A dense-time temporal logic with nice compositionality properties
A dense temporal logic specification method for the development of reactive systems is introduced. The two development constructs of this method are refinement and composition. A reactive system is specified by a pair consisting of a machine and a condition on the computations of this machine. In order to compose such systems compositionally, each machine step contains additional information such as, “this is a system step”, or “this is an environment step” or “this is a communication step”. Compositionality enables us to break refinement between complex systems into refinement between small and simple systems. The latter can then be verified by existing proof rules for refinement which are reformulated in our formalism.
Citation : Cau, Antonio and Roever, W.-P. de, A dense-time temporal logic with nice compositionality properties. In: Computer aided systems theory, EUROCAST '97: a selection of papers from the 6th International Workshop on Computer Aided Systems Theory, Las Palmas de Gran Canaria, Spain, February 1997. Editors: Franz Pichler and Roberto Moreno Diaz, Berlin: New York: Springer, 1997, Lecture notes in computer science, vol 1333. pp. 123-145.
ISSN : 0302-9743
Research Group : Software Technology Research Laboratory (STRL)