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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    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


    Verification of System Architectures Using Modal Logics and Formal Model Checking Techniques

    Zaidi, A. K. / Levis, A. H. | British Library Conference Proceedings | 2006


    Formal Verification at System Level

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