Computing worst-case response times in real-time avionics applications

The work in this paper builds upon our prior work to analyze properties of applications running on top of the Deos real-time operating system. We describe how a control application's worst-case response time to an event can be "computed" using the model checker SPIN. We lay out the steps involved in reusing our existing models for this analysis, and our 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.