Formal Validation of Downtimeless System Evolution in Embedded Automation Controllers

Christoph Sünder, Valeriy Vyatkin und Alois Zoitl

ACM Transactions on Embedded Computer Systems (TECS), pp. 17:1-17:17

Januar 2013 · DOI: 10.1145/2406336.2406353


This article presents a new formal approach to validation of on-the-fly modification of control software in automation systems. The concept of downtimeless system evolution (DSE) is introduced. The DSE is essentially based on the use of IEC 61499 system architecture and formal modeling and verification of the hardware and software of an automation device. The validation is performed by means of two complimentary techniques: analytic calculations and formal verification by model-checking.