×

zbMATH — the first resource for mathematics

Leveraging Horn clause solving for compositional verification of PLC software. (English) Zbl 1435.68190
Summary: Real-world PLC software is modular and composed of many different function blocks. Nevertheless, common approaches to PLC software verification do not leverage this but resort to inlining, or analyse instances of the same function block type independently. With the advent of constrained Horn clauses as the basis for automated program verification, many state-of-the-art verification procedures build upon them. We illustrate how this formalism allows for a uniform characterisation of PLC program semantics and safety goals, derived from reactive systems safety foundations. Furthermore, we give a natural extension of the resulting encoding which enables compositional reasoning about modular software. Due to the cyclic execution of PLCs, an engineer’s mental model of a single function block often exhibits state machine semantics – partitioning a block’s behaviour into different modes of operation. We illustrate how such a mode space, and similar high-level knowledge, can be integrated with our compositional characterisation. We investigate the impact of each technique on the model checking performance by characterising PLC software verification problems, both in a non-compositional and a compositional way that may incorporate mode transitions, and solving them with an SMT solver. Evaluation of our prototypical implementation on examples from the PLCopen Safety library shows the effectiveness of both the chosen formalism and using high-level summaries.
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing
93C85 Automated systems (robots, etc.) in control theory
Software:
nuXmv; SMACK; VeriMAP; z3
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Apel S, Beyer D, Friedberger K, Raimondi F, von Rhein A (2013) Domain types: Abstract-domain selection based on variable usage. In: Hardware and Software: Verification and Testing - 9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5-7, 2013, Proceedings, pp 262-278
[2] Beckert B, Ulbrich M, Vogel-Heuser B, Weigl A (2015) Regression verification for programmable logic controller software. In: Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings, pp 234-251
[3] Beyene, Tewodros A.; Popeea, Corneliu; Rybalchenko, Andrey, Efficient CTL Verification via Horn Constraints Solving, Electronic Proceedings in Theoretical Computer Science, 219, 1-14 (2016)
[4] Beyer D (2015) Software verification and verifiable witnesses - (report on SV-COMP 2015). In: Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, pp 401-416
[5] Beyer, Dirk, Automatic Verification of C and Java Programs: SV-COMP 2019, Tools and Algorithms for the Construction and Analysis of Systems, 133-155 (2019), Cham: Springer International Publishing, Cham
[6] Beyer, D.; Stahlbauer, A., Bdd-based software verification, Int J Softw Tools Technol Transfer, 16, 5, 507-518 (2014)
[7] Beyer D, Henzinger TA, Théoduloz G (2007) Configurable software verification: Concretizing the convergence of model checking and program analysis. In: Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, pp 504-518 · Zbl 1135.68466
[8] Beyer D, Cimatti A, Griggio A, Keremoglu ME, Sebastiani R (2009) Software model checking via large-block encoding. In: Proceedings of 9Th International Conference on Formal Methods in Computer-aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA, pp 25-32
[9] Biallas S, Brauer J, Kowalewski S (2012) Arcade.plc: a verification platform for programmable logic controllers. In: IEEE/ACM International Conference on Automated Software Engineering, ASE’12, Essen, Germany, September, 3-7, 2012, pp 338-341
[10] Biallas S, Giacobbe M, Kowalewski S (2013) Predicate abstraction for programmable logic controllers. In: Formal Methods for Industrial Critical Systems - 18th International Workshop, FMICS 2013, Madrid, Spain, September 23-24, 2013. Proceedings, pp 123-138
[11] Bjørner, Nikolaj; Gurfinkel, Arie; Mcmillan, Ken; Rybalchenko, Andrey, Horn Clause Solvers for Program Verification, Fields of Logic and Computation II, 24-51 (2015), Cham: Springer International Publishing, Cham · Zbl 06484064
[12] Blass, A.; Gurevich, Y., Existential Fixed-point Logic, 20-36 (1987), Berlin: Springer, Berlin · Zbl 0647.03018
[13] Bohlender, D.; Kowalewski, S., Compositional verification of plc software using horn clauses and mode abstraction, IFAC-PapersOnLine, 51, 7, 428-433 (2018)
[14] Bohlender D, Kowalewski S (2018b) Design and verification of restart-robust industrial control software. In: Integrated Formal Methods - 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings, pp 47-68
[15] Bohlender D, Simon H, Kowalewski S (2016) Symbolic verification of PLC safety-applications based on plcopen automata. In: 19th GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, MBMV 2016, Freiburg im Breisgau, Germany, March 1-2, 2016., pp 33-45
[16] Bohlender D, Hamm D, Kowalewski S (2018) Cycle-bounded model checking of PLC software via dynamic large-block encoding. In: Proceedings of the 33rd Annual ACM Symposium on Applied Computing, SAC 2018, Pau, France, April 09-13, 2018, pp 1891-1898
[17] Carter M, He S, Whitaker J, Rakamaric Z, Emmi M (2016) SMACK software verification toolchain. In: Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, Austin, TX, USA, May 14-22, 2016 - Companion Volume, pp 589-592
[18] Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S (2014) The nuxmv symbolic model checker. In: Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, pp 334-342
[19] Clarke, Em; Klieber, W.; Nováček, M.; Zuliani, P., Model checking and the state explosion problem, 1-30 (2012), Berlin: Springer, Berlin
[20] Darvas D, Fernandez Adiego B, Blanco E (2013) Transforming PLC Programs into Formal Models for Verification Purposes. Tech rep., EN-ICE-PLC, CERN
[21] Darvas D, Majzik I, Viñuela EB (2016) Formal verification of safety PLC based control software. In: Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings, pp 508-522
[22] De Angelis E, Fioravanti F, Pettorossi A, Proietti M (2014) Verimap: A tool for verifying programs through transformations. In: Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, pp 568-574
[23] Dijkstra, Ew; Schölten, Cs, The Strongest Postcondition, 209-215 (1990), New York: Springer, New York
[24] Eén N, Mishchenko A, Brayton RK (2011) Efficient implementation of property directed reachability. In: International conference on formal methods in computer-aided design, FMCAD ’11, austin, TX, USA, October 30 - November 02, 2011, pp 125-134
[25] Frey G, Drath R, Schlich B, Eschbach R (2012) “safety automata” - A new specification language for the development of PLC safety applications. In: Proceedings of 2012 IEEE 17th International Conference on Emerging Technologies & Factory Automation, ETFA 2012, Krakow, Poland, September 17-21, 2012, pp 1-8
[26] Graf S, Saïdi H (1997) Construction of abstract state graphs with PVS. In: Computer Aided Verification, 9th International Conference, CAV ’97, Haifa, Israel, June 22-25, 1997, Proceedings, pp 72-83
[27] Hoare, C. A. R., An axiomatic basis for computer programming, Communications of the ACM, 12, 10, 576-580 (1969) · Zbl 0179.23105
[28] Hoder K, Bjørner N (2012) Generalized property directed reachability. In: Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, pp 157-171 · Zbl 1273.68229
[29] Komuravelli A, Bjørner N, Gurfinkel A, McMillan KL (2015) Compositional verification of procedural programs using horn clauses over integers and arrays. In: Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, September 27-30, 2015., pp 89-96
[30] Lange T, Neuhäußer MR, Noll T (2013) Speeding up the safety verification of programmable logic controller code. In: Hardware and Software: Verification and Testing - 9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5-7, 2013, Proceedings, pp 44-60
[31] Ljungkrantz, O.; Åkesson, K.; Fabian, M.; Yuan, C., Formal specification and verification of industrial control logic components, IEEE Trans Automation Science and Engineering, 7, 3, 538-548 (2010)
[32] Manna Z, Pnueli A (1995) Temporal verification of reactive systems - safety. Springer · Zbl 1288.68169
[33] McMillan KL (1993) Symbolic model checking. Kluwer · Zbl 0784.68004
[34] Moon, I., Modeling programmable logic controllers for logic verification, IEEE Control Syst Mag, 14, 2, 53-59 (1994)
[35] de Moura LM, Bjørner N (2008) Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, pp 337-340
[36] Ovatman, T.; Aral, A.; Polat, D.; Ünver, Ao, An overview of model checking practices on verification of PLC software, Software and System Modeling, 15, 4, 937-960 (2016)
[37] PLCopen TC5 (2006) Safety Software, Technical Specification, Part 1: Concepts and Function Blocks. PLCopen
[38] PLCopen TC5 (2008) Safety Software, Technical Specification, Part 2: User Examples. PLCopen
[39] Quinton S, Graf S (2008) Contract-based verification of hierarchical systems of components. In: Sixth IEEE International Conference on Software Engineering and Formal Methods, SEFM 2008, Cape Town, South Africa, 10-14 november 2008, pp 377-381
[40] Simon H, Kowalewski S (2018) Mode-aware concolic testing for PLC software. In: Integrated Formal Methods - 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings, pp 367-376
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.