Title :
Arcade.PLC: a verification platform for programmable logic controllers
Author :
Biallas, Sebastian ; Brauer, J. ; Kowalewski, Stefan
Author_Institution :
Embedded Software Lab., RWTH Aachen Univ., Aachen, Germany
Abstract :
This paper introduces Arcade.PLC, a verification platform for programmable logic controllers (PLCs). The tool supports static analysis as well as ACTL and past-time LTL model checking using counterexample-guided abstraction refinement for different programming languages used in industry. In the underlying principles of the framework, knowledge about the hardware platform is exploited so as to provide efficient techniques. The effectiveness of the approach is evaluated on programs implemented using a combination of programming languages.
Keywords :
control engineering computing; formal verification; programmable controllers; programming languages; ACTL model checking; Arcade.PLC platform; PLC; counterexample-guided abstraction refinement; past-time LTL model checking; programmable logic controllers; programming language; static analysis; verification platform; PLC; model checking; static analysis;
Conference_Titel :
Automated Software Engineering (ASE), 2012 Proceedings of the 27th IEEE/ACM International Conference on
Print_ISBN :
978-1-4503-1204-2
DOI :
10.1145/2351676.2351741
