Model Generation for Temporal Properties of Reactive ComponentsAndrew Moss, Henk Muller, Model Generation for Temporal Properties of Reactive Components. 1st International Workshop on Software Analysis and Development for Pervasive Systems. Mauricio Varea, (eds.), pp. 12–19. August 2004. PDF, 108 Kbytes.
We present a new static analysis that generates a model of the temporal behaviour of a reactive component. The component is specified in machine code - this makes the analysis applicable to the legacy code and the output of any compiler. Our analysis is an abstract interpretation of the program that computes the possible periodicities of instructions within a nonterminating program. The machine code is transformed into an abstract instruction set that retains only the timing characteristics of each instruction. We show how a simple abstraction of the timing state allows an abstract interpretation to construct a finite model of the components temporal behaviour. This model is useful for manual verification of a simple component or can be used to construct an automatic verification through model-checking. The abstraction of time uses a relative measure of time; time is measured since the flow of control passed certain nominated positions.