Formal Validation of Downtimeless System Evolution in Embedded Automation Controllers

Christoph Sünder , Valeriy Vyatkin and Alois Zoitl

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.

url: http://doi.acm.org/10.1145/2406336.2406353

URL DOI BibTeX Back