One domain for which automotive companies are expressing interest in formal analysis is microcontroller code containing hard-to-find defects in the low-level execution. The authors developed a model checker called [mc]square for the verification of such microcontroller specific code. The paper presents the extendable architecture of [mc]square which is required to adapt this approach to further microcontrollers and different model checking algorithms. The tool features and the architecture are explained and with the help of a realistic example it is illustrated how the tool can be used to analyse a program.
An extendable architecture for model checking hardware-specific automotive microcontroller code
Eine erweiterbare Architektur für die Modellprüfung hardware-spezifischer Automobile-Mikrocontroller-Programme
2007
11 Seiten, 3 Bilder, 15 Quellen
Aufsatz (Konferenz)
Englisch
Applying model checking to an automotive microcontroller application
Tema Archiv | 2007
|Microcontroller fuer sicherheitskritische Automotive-Systeme
Kraftfahrwesen | 2010
|Integration of hardware specific features of microcontroller into the AUTOSAR standard
Kraftfahrwesen | 2009
|