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
- Standort
-
Deutsche Nationalbibliothek Frankfurt am Main
- Umfang
-
Online-Ressource
- Sprache
-
Englisch
- Klassifikation
-
Informatik
- Ereignis
-
Veröffentlichung
- (wo)
-
Freiburg
- (wer)
-
Universität
- (wann)
-
2016
- Urheber
- Beteiligte Personen und Organisationen
- DOI
-
10.6094/UNIFR/10636
- URN
-
urn:nbn:de:bsz:25-freidok-106362
- Rechteinformation
-
Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Letzte Aktualisierung
-
14.08.2025, 10:54 MESZ
Datenpartner
Dieses Objekt wird bereitgestellt von:
Deutsche Nationalbibliothek. Bei Fragen zum Objekt wenden Sie sich bitte an den Datenpartner.
Deutsche Nationalbibliothek. Bei Fragen zum Objekt wenden Sie sich bitte an den Datenpartner.
Beteiligte
- Bohlender, Dimitri
- Simon, Hendrik
- Kowalewski, Stefan
- Wimmer, Ralf
- Universität
Entstanden
- 2016
Ähnliche Objekte (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
Configurable verification of timed automata with discrete variables
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
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
Configurable verification of timed automata with discrete variables
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
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
Configurable verification of timed automata with discrete variables
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