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
Conference paper
English
Applying model checking to an automotive microcontroller application
Tema Archive | 2007
|Microcontroller fuer sicherheitskritische Automotive-Systeme
Automotive engineering | 2010
|High performance code generation for Audo, an automotive microcontroller from Infineon Technologies
Automotive engineering | 2000
|Integration of Hardware Specific Features of Microcontroller into the AUTOSAR Standard
SAE Technical Papers | 2009
|Integration of hardware specific features of microcontroller into the AUTOSAR standard
Automotive engineering | 2009
|