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.


    Access

    Access via TIB

    Check availability in my library


    Export, share and cite



    Title :

    Logic Model Checking of Time-Periodic Real-Time Systems


    Contributors:

    Conference:

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


    Publication date :

    2012-06-19


    Type of media :

    Conference paper


    Type of material :

    No indication


    Language :

    English




    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


    Model Checking Multitask Applications for OSEK Compliant Real-Time Operating Systems

    McKelvin, Mark L., Jr. / Gamble, Edward / Holzmann, Gerard | NTRS | 2011