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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    An extendable architecture for model checking hardware-specific automotive microcontroller code


    Additional title:

    Eine erweiterbare Architektur für die Modellprüfung hardware-spezifischer Automobile-Mikrocontroller-Programme


    Contributors:


    Publication date :

    2007


    Size :

    11 Seiten, 3 Bilder, 15 Quellen



    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English




    Applying model checking to an automotive microcontroller application

    Schlich, B. / Salewski, F. / Kowalewski, S. | Tema Archive | 2007


    Microcontroller fuer sicherheitskritische Automotive-Systeme

    Freescale,DE / STMicroelectronics,DE | Automotive engineering | 2010


    High performance code generation for Audo, an automotive microcontroller from Infineon Technologies

    Amato,G. / Koester,L. / Infineon Technologies,DE et al. | Automotive engineering | 2000



    Integration of hardware specific features of microcontroller into the AUTOSAR standard

    Wang,G. / Infineon Technologies,DE | Automotive engineering | 2009