Arcade.µC

Arcade.µC is a framework for the verification of binary code for microcontroller. Its development started in 2005 under the name [mc]square and has been widely improved since.

The goal of Arcade.µC is to enable software developers to analyze, debug, and verify their code on a daily basis. This is why we provide a graphical user interface based on the Eclipse Rich Client framework, that grants comforts most academic tools lack. Since we hide much of the complexity of formal methods from the user, a four to eight hour workshop is all a software developer needs to get started using Arcade. As input, Arcade takes the compiled binary code eliminating the need for error-prone and time-consuming manual modelling. Should you also be able to provide the C source code and a binary containing debug information, Arcade will link these inputs automatically. In that case, specifications can use C labels as well as variable names and counterexamples are displayed in the C source code as well.

Arcade.µC consists of a simulator for different microcontrollers, a set of model-checkers, and a static analysis interface.

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

• ATMEL ATmega16, ATmega128
• Renesas R8C/23
• several discontinued microcontrollers

In the past, a computer science student who had no prior knowledge of Aracde or the target hardware implemented basic support for the Infineon XC167 microcontroller as part of his diploma thesis.

• CTL model checking (including three-valued atomics)
• Past time LTL model checking
• Safety Automata

The major advantage of static analyses in Arcade is that they enable powerful abstraction techniques to reduce the size of the state space by several orders of magnitude without losing relevant information. However, we also present the results to the user directly:

• Live Variable Analysis
• Reachable Definitions Analysis
• Maximum Stack Size Analysis
• and many more

We provided our industrial partner, a SME in the automotive sector, with Arcade and basic training. The software developers were able to create formal specifications in CTL and as safety automata. Using these specifications, Arcade uncovered a number of previously undetected errors in their code:

• A possible division by zero was unconsidered.
• Due to code reuse, interrupts were prematurely activated globally during initialization.
• After a compiler update, an old file produced variable initialization code that did not initialize a single variable.

This picture shows the simulator view of Arcade.µC. The developer can step through the code instruction by instruction (C and assembly, forth and back) and inspect all memory locations of our internal hardware model. In this picture a similar view is used to present a counterexample to the user. On the right, Arcade shows in which state the safety automaton used for specification currently is. On the left, the developer can step through the counterexample (forth and back). This helps the developer in understanding the cause of the counterexample and locating the error.