Arcade

Arcade - Aachen Rigorous Code Analysis and Debugging Environment - is a framework for the verification and analysis of embedded software. It is designed for daily use in industry. The key idea is to utilize the (compiled) software as is without need for further manual modelling or preprocessing. It offers various formal methods from static analysis to model checking. Currently, Arcade supports multiple microcontrollers as well as programmable logic controllers.

As an example, confere to the figure below which shows the model checking process of Arcade. The user supplies a program in its unprocessed form and a specification. Arcade automatically generated a model using a build-in hardware simulator; this model is used by different on-the-fly model checking algorithms. In order to prevent state explosion, static analyses are performed automatically beforehand enabling advances abstraction techniques to minimize the state space. Partially symbolic data structures allow for a compact representation of sets of states. If the specification is violated, Arcade presents a counterexample that can be used to track down the source of the violation.

We provide two versions of Arcade tailored to microcontrollers and programmable logic controllers respectively. Have a look at the corresponding pages for more information about them.

• Arcade.PLC
• Arcade.µC

In 2005, Bastian Schlich of the Embedded Software Laboratory started the development of [mc]square - Model Checking Micro Controller. The tool soon was able to perform explicit model checking on binary microcontroller code for academic examples. Due to is strong modular nature, it was possible to quickly add support for multiple microcontrollers and programmable logic controllers as well as complex abstraction and analysis techniques. In 2011, [mc]square was reincarnated as Arcade featuring a graphical user interface based on the Eclipse Rich Client formwork.

Contact us if you are interested in this verification tool and want more information.