Microcontrollers in automotive applications perform more and more safety critical functions. The reliability of these systems is of great importance and model checking is seen as a promising future tool for the analysis of the corresponding software. For this purpose an explicit, on-the-fly CTL model checker for assembly code called (mc)square was developed at our institute. This paper describes a case study that was conducted using (mc) square. The aim of this case study was to model check programs that solve an automotive problem, namely a four channel speed measurement with CAN bus interface. The programs were written by students in a lab course without the application of model checking in mind. Hence, these programs contain all features which can be found in real world software. This case study showed that small or medium sized microcontroller programs can be verified without respectively with minor modifications. Additional potentials for future improvements to handle more complex programs have been identified.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Applying model checking to an automotive microcontroller application


    Contributors:
    Schlich, B. (author) / Salewski, F. (author) / Kowalewski, S. (author)


    Publication date :

    2007


    Size :

    8 Seiten, 19 Quellen




    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English





    Timer validation of automotive microcontroller using motor application

    Vaishnav, Saujal / Murarishetty, Chethan / Jayakrishna, Guddeti | IEEE | 2017


    Microcontroller fuer sicherheitskritische Automotive-Systeme

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


    Method of checking the functionality of a vehicle microcontroller

    GANESH SANKAR / AISHIK MAZUMDER | European Patent Office | 2023

    Free access

    Cost Effective LIN Bus Automotive Networking Microcontroller

    Bender, Michael | SAE Technical Papers | 2004