The application of Programmable Logic Controllers (PLCs) in safety critical systems demands a failure free behaviour considering all possible scenarios. Due to the cost of software development a user program is often in use on different types of PLCs. But one open question is: Behaves the user program equivalent on all PLCs? A framework is proposed suitable to prove the equivalence of a user program regarding different types of PLCs. The semantic behaviour of the hardware is embedded and the equivalence against a high level reference model is proved. Formal Equivalence Checking (EC) using Boolean satisfiability (SAT) is applied and the framework is evaluated in a case study.
Verification of PLC programs using formal proof techniques
Verifizierung von PLC-Programmen durch formale Verifikation
2008
8 Seiten, 7 Bilder, 6 Tabellen, 19 Quellen
Aufsatz (Konferenz)
Englisch
Anwenderprogramm , Äquivalenz , Boole-Algebra , eingebettete Elektronik , Eisenbahnsignaltechnik , experimentelles Ergebnis , Fallstudie , formale Sprache , formale Verifikation , Framework (Programmierung) , IEC-Norm , integrierte Sicherheitsstufe , Komplexität , Logiksimulation , Modellbildung , Programmentwicklung , programmierbarer Logikregler , Programmiersprache , Programmprüfung , Referenzwert , Schaltungslogik , sicherheitskritisches Software-Design , Software-Engineering , Verriegelung
Formal Verification at System Level
British Library Conference Proceedings | 2009
|Articles - Formal Verification & Legacy Redesign
Online Contents | 1999
|Formal verification and legacy redesign
Tema Archiv | 1998
|