Leveraging Horn clause solving for compositional verification of PLC software

DOI10.1007/S10626-019-00296-8MaRDI QIDQ2177778zbMATH OpenOpenAlexWikidataFDO

Authors Dimitri Bohlender, Stefan Kowalewski

Publication date 6 May 2020

Published in Discrete Event Dynamic Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10626-019-00296-8

zbMATH Keywords

constrained Horn clausesformal verificationindustry automationpredicate abstractionprogrammable logic controllerssoftware safety

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Automated systems (robots, etc.) in control theory (93C85)

Recommendations

• scientific article; zbMATH DE number 1836374
• Component-based formal modeling of PLC systems
• scientific article; zbMATH DE number 5718039
• Verification of programmable logic controller code using model checking and static analysis
• Temporal Logic for Programmable Logic Controllers

Cites work

• An axiomatic basis for computer programming
• Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
• Efficient CTL verification via Horn constraints solving
• Generalized property directed reachability
• Horn clause solvers for program verification
• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 4055578 (Why is no real title available?)
• Temporal verification of reactive systems: response

Cited in

(3)

• Component-based formal modeling of PLC systems
• scientific article; zbMATH DE number 1223543 (Why is no real title available?)
• On the application of the calculus of positively constructed formulas for the study of controlled discrete-event systems

Describes a project that uses

Uses Software

• nuXmv
• VeriMAP
• z3
• SMACK

This page was built for publication: Leveraging Horn clause solving for compositional verification of PLC software

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2177778)