• DocumentCode
    3572010
  • Title

    Arcade.PLC: a verification platform for programmable logic controllers

  • Author

    Biallas, Sebastian ; Brauer, J. ; Kowalewski, Stefan

  • Author_Institution
    Embedded Software Lab., RWTH Aachen Univ., Aachen, Germany
  • fYear
    2012
  • Firstpage
    338
  • Lastpage
    341
  • Abstract
    This paper introduces Arcade.PLC, a verification platform for programmable logic controllers (PLCs). The tool supports static analysis as well as ACTL and past-time LTL model checking using counterexample-guided abstraction refinement for different programming languages used in industry. In the underlying principles of the framework, knowledge about the hardware platform is exploited so as to provide efficient techniques. The effectiveness of the approach is evaluated on programs implemented using a combination of programming languages.
  • Keywords
    control engineering computing; formal verification; programmable controllers; programming languages; ACTL model checking; Arcade.PLC platform; PLC; counterexample-guided abstraction refinement; past-time LTL model checking; programmable logic controllers; programming language; static analysis; verification platform; PLC; model checking; static analysis;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Automated Software Engineering (ASE), 2012 Proceedings of the 27th IEEE/ACM International Conference on
  • Print_ISBN
    978-1-4503-1204-2
  • Type

    conf

  • DOI
    10.1145/2351676.2351741
  • Filename
    6494950