Formal Validation of Downtimeless System Evolution in Embedded Automation Controllers
ACM Transactions on Embedded Computer Systems (TECS), pp. 17:1-17:17
January 2013 · doi: 10.1145/2406336.2406353
abstract
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.