Symbolic verification of PLC safety-applications based on PCLopen automata
Zusammenfassung: This paper presents a technique for verifying a PLC program’s compliance with respect to the automaton-based specifications used by the PLCopen. While related approaches only support a subset of expressible PLCopen automata and struggle with the state explosion problem, our technique both enables the logical characterisation of any PLCopen automaton and facilitates the verification of programs previously entailing exhaustive state space exploration and time outs. To enable fully symbolic reasoning we utilise the Property Directed Reachability capabilities of the Z3 SMT solver
- Location
-
Deutsche Nationalbibliothek Frankfurt am Main
- Extent
-
Online-Ressource
- Language
-
Englisch
- Classification
-
Informatik
- Event
-
Veröffentlichung
- (where)
-
Freiburg
- (who)
-
Universität
- (when)
-
2016
- Creator
- Contributor
- DOI
-
10.6094/UNIFR/10636
- URN
-
urn:nbn:de:bsz:25-freidok-106362
- Rights
-
Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Last update
-
25.03.2025, 1:42 PM CET
Data provider
This object is provided by:
Deutsche Nationalbibliothek. If you have any questions about the object, please contact the data provider.
Deutsche Nationalbibliothek. If you have any questions about the object, please contact the data provider.
Associated
- Bohlender, Dimitri
- Simon, Hendrik
- Kowalewski, Stefan
- Wimmer, Ralf
- Universität
Time of origin
- 2016
Other Objects (12)
Verification of automata with storage mechanisms
Verification of Automata with Storage Mechanisms
Integrating Symbolic Execution, Debugging and Verification
Applications of automata learning in verification and synthesis
Applications of automata learning in verification and synthesis
symQV : Automated Symbolic Verification of Quantum Programs
Interactive Verification of Concurrent Systems using Symbolic Execution
Formal verification of infinite-state systems : one-counter machines, register automata, and timed automata
Formal Verification of Algorithms for Automata and Model Checking
Improving Live Sequence Chart to Automata Transformation for Verification
New results on probabilistic verification : automata, logic and satisfiability
An Automata-Theoretic Approach to Open Actor System Verification
Verification of automata with storage mechanisms
Verification of Automata with Storage Mechanisms
Integrating Symbolic Execution, Debugging and Verification
Applications of automata learning in verification and synthesis
Applications of automata learning in verification and synthesis
symQV : Automated Symbolic Verification of Quantum Programs
Interactive Verification of Concurrent Systems using Symbolic Execution
Formal verification of infinite-state systems : one-counter machines, register automata, and timed automata
Formal Verification of Algorithms for Automata and Model Checking
Improving Live Sequence Chart to Automata Transformation for Verification
New results on probabilistic verification : automata, logic and satisfiability
An Automata-Theoretic Approach to Open Actor System Verification
Verification of automata with storage mechanisms
Verification of Automata with Storage Mechanisms
Integrating Symbolic Execution, Debugging and Verification
Applications of automata learning in verification and synthesis
Applications of automata learning in verification and synthesis
symQV : Automated Symbolic Verification of Quantum Programs
Interactive Verification of Concurrent Systems using Symbolic Execution
Formal verification of infinite-state systems : one-counter machines, register automata, and timed automata
Formal Verification of Algorithms for Automata and Model Checking
Improving Live Sequence Chart to Automata Transformation for Verification
New results on probabilistic verification : automata, logic and satisfiability