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.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Formal Specification and Verification of Hybrid Programs for Urban Air Mobility

    J. Tanner Slagel / Cesar Munoz / Swee Balachandran et al. | NTRS


    Integrating Abstraction Techniques for Formal Verification of Analog Designs

    Zaki, Mohamed H. / Denman, William / Tahar, Sofiène et al. | AIAA | 2009


    Formal Verification at System Level

    Mazzini, S. / Puri, S. / Mari, F. et al. | British Library Conference Proceedings | 2009



    Formal verification and legacy redesign

    Young, F.C.D. / Houston, J.A. | Tema Archiv | 1998