In this paper we report on the work we performed to extend the logic model checker SPIN with built-in support for the verification of periodic, real-time embedded software systems, as commonly used in aircraft, automobiles, and spacecraft. We first extended the SPIN verification algorithms to model priority based scheduling policies. Next, we added a library to support the modeling of periodic tasks. This library was used in a recent application of the SPIN model checker to verify the engine control software of an automobile, to study the feasibility of software triggers for unintended acceleration events.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen


    Exportieren, teilen und zitieren



    Titel :

    Logic Model Checking of Time-Periodic Real-Time Systems


    Beteiligte:
    Florian, Mihai (Autor:in) / Gamble, Ed (Autor:in) / Holzmann, Gerard (Autor:in)

    Kongress:

    AIAA Infotech @ Aerospace 2012 Conference ; 2012 ; Garden Grove, CA, United States


    Erscheinungsdatum :

    19.06.2012


    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Keine Angabe


    Sprache :

    Englisch




    Logic Model Checking of Time-Periodic Real-Time Systems

    Florian, Mihai / Gamble, Ed / Holzmann, Gerard | AIAA | 2012


    2012-2607 Logic Model Checking of Time-Periodic Real-Time Systems

    Florian, M. / Gamble, E. / Holzmann, G. et al. | British Library Conference Proceedings | 2012


    Verification of Real-Time Systems using Statistical Model Checking

    Hansen, Jeffery P. / Wrage, Lutz | AIAA | 2015


    Analysis of real-time code by model checking

    Guaspari, D. / Naydich, D. | IEEE | 2000


    Analysis of Real-Time Code by Model Checking

    Guaspari, D. / IEEE / AIAA | British Library Conference Proceedings | 2000