Arcade

Arcade is a framework for the verification of programs for programmable logic controllers. Its development started in 2011 as a reincarnation of the [mc]square framework, tailored for the support of PLC semantics and specific features.

The expressed aim of Arcade is to aid PLC developers in finding bugs and verifying functional (safety) properties without requiring deep knowledge of formal methods. This is provided by offering direct support of different PLC programming languages and easy access to different analysis functions.

Arcade consists of a static analysis engine for PLC languages.

• IEC 61131 “Structured Text”
• IEC 61131 “Sequential Function Chart”

Arcade can be used in two ways. An interactive command line REPL allows for command-based use of Arcade.

Arcade can also be used like a normal command line tool. Results of the bug-finding analysis are printed directly on the command line…

…while the detailed results of e.g. value set analysis are written into a html-file that can be viewed with any web browser