The technical contribution of this paper is a particular way of adding model-checking to the repertoire of more familiar techniques (such as rate monotonic analysis) for analyzing real-time behavior. Model-checking comprises automated methods of search and reasoning that apply, in principle, to any system representable as a finite state machine. It can be used to verify not only that deadlines are met but other system properties as well. The methods we propose are general, but are applied in the context of a specific solution to the problem of safety-critical runtime support. The Ravenscar subset of Ada tasking is designed to support pre-emptive scheduling while requiring minimal runtime support. The Ravenscar profile is supported by the RAVEN/sup TM/ runtime, developed at Aonix to be FAA certifiable. Our immediate goal is to verify Ravenscar programs running on RAVEN/sup TM/.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Analysis of real-time code by model checking


    Beteiligte:
    Guaspari, D. (Autor:in) / Naydich, D. (Autor:in)


    Erscheinungsdatum :

    01.01.2000


    Format / Umfang :

    678415 byte




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Analysis of Real-Time Code by Model Checking

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


    Logic Model Checking of Time-Periodic Real-Time Systems

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


    Logic Model Checking of Time-Periodic Real-Time Systems

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



    Verification of Real-Time Systems using Statistical Model Checking

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