Compositional Verification of PLC Software using Horn Clauses and Mode Abstraction. Issue 7 (2018)

• Record Type: Journal Article
• Authors: Bohlender, Dimitri; Kowalewski, Stefan
• Is Part Of: IFAC-PapersOnLine. Volume 51:Issue 7(2018)
• Page Start: 428
• Page End: 433
• Publication Date: 2018
• Subjects: Formal verification -- Programmable logic controllers -- Industry automation -- Software tools -- Software safety; Automatic control -- Periodicals; 629.805
• DOI: 10.1016/j.ifacol.2018.06.336
• Languages: English
• ISSNs: 2405-8963

Abstract

Abstract: Real-world PLC software is modular and composed of many different function blocks. Due to its cyclic execution, an engineer's mental model of a single function block often exhibits state machine semantics – partitioning a block's behaviours into different modes of operation. We propose a technique called mode abstraction for automatic computation of such high-level models from program semantics and investigate its impact on the overall model checking performance. To this end, we use constrained horn clauses to characterise the program semantics, mode transitions and safety goals in a compositional way. The resulting verification conditions are discharged using an SMT solver. Evaluation of our prototypical implementation on examples from the PLCopen Safety library shows the effectiveness of both the chosen formalism and mode abstraction.