Abstract
Formal verification has become a recommended practice in the safety-critical application areas. However, due to the complexity of practical control and safety systems, the state space explosion often prevents the use of formal analysis. In this paper we extend our former verification methodology with effective property preserving reduction techniques. For this purpose we developed general rule-based reductions and a customized version of the Cone of Influence (COI) reduction. Using these methods, the verification of complex requirements formalised with temporal logics (e.g. CTL, LTL) can be orders of magnitude faster. We use the NuSMV model checker on a real-life PLC program from CERN to demonstrate the performance of our reduction techniques. © 2014 IFIP International Federation for Information Processing.
Author supplied keywords
Cite
CITATION STYLE
Darvas, D., Fernández Adiego, B., Vörös, A., Bartha, T., Blanco Viñuela, E., & González Suárez, V. M. (2014). Formal verification of complex properties on PLC programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8461 LNCS, pp. 284–299). Springer Verlag. https://doi.org/10.1007/978-3-662-43613-4_18
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
