The work in this paper builds upon prior work to analyze properties of applications running on top of the Deos real-time operating system. The authors describe how a control application's worst-case response time to an event can be 'computed' using the model checker SPIN. The authors lay out the steps involved in reusing their existing models for this analysis, and their solution to reducing the memory required to perform the analysis. This work highlights the benefit of expanding the use of formal models, and the necessity of changing existing abstractions (such as the timer model in this work) to reflect changed verification goals.
Computing worst-case response times in real-time avionics applications
Berechnung der ungünstigsten Antwortzeiten in Echtzeit-Avionik-Anwendungen
2008
14 Seiten, 14 Bilder, 9 Quellen
Aufsatz (Konferenz)
Englisch
Object-oriented real-time computing for reusable avionics software
Tema Archiv | 2001
|Real Time Aspects of Manned Space Flight Avionics Computing
Springer Verlag | 1994
|Real-time avionics optimization
Tema Archiv | 2011
|