Model Generation for Temporal Properties of Reactive Components

A Moss, HL Muller

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)


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.
Translated title of the contributionModel Generation for Temporal Properties of Reactive Components
Original languageEnglish
Title of host publicationUnknown
EditorsMauricio Varea
PublisherUniversity of Southampton
Pages12 - 19
Number of pages7
Publication statusPublished - Aug 2004

Bibliographical note

Conference Proceedings/Title of Journal: 1st International Workshop on Software Analysis and Development for Pervasive Systems


Dive into the research topics of 'Model Generation for Temporal Properties of Reactive Components'. Together they form a unique fingerprint.

Cite this