Arcade.PLC

Arcade.PLC 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.PLC 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 a graphical user interface based on the Eclipse Rich Client framework, direct support of different PLC programming languages and easy access to different model checking and static analysis functions.

Arcade.PLC consists of a simulator for different PLC languages, a model-checker and a static analysis interface.

It features a graphical user interface (see below) under a varity of operating systems.

• IEC 61131 “Structured Text”
• IEC 61131 “Instruction List”
• Siemens S7 AWL

• CTL model checking
• Past time LTL model checking
• Safety Automata

The first screenshot shows the build-in simulator which can be used to debug and analyze the PLC Code. This screenshot also highlights the value-set analysis which automatically determines possible ranges from the program variables.

In the second screenshot the model checker interface is shown. Different formulae (in different logics) can be checked in parallel.

If there is a counterexample or witness for a formula, possible PLC inputs which yield a path violating the specification are shown graphically.