Model Generation for Temporal Properties of Reactive Components

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.