A dense-time temporal logic with nice compositionality properties

De Montfort University Open Research Archive

Show simple item record

dc.contributor.author Cau, A. (Antonio)
dc.contributor.author de Roever, W. P.
dc.date.accessioned 2005-09-05T17:59:17Z
dc.date.available 2005-09-05T17:59:17Z
dc.date.issued 1997-02
dc.identifier.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. en
dc.identifier.issn 0302-9743
dc.identifier.uri http://hdl.handle.net/2086/37
dc.description.abstract 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. en
dc.format.extent 399220 bytes
dc.format.extent 704337 bytes
dc.format.mimetype application/pdf
dc.format.mimetype application/postscript
dc.language.iso en en
dc.relation.ispartofseries STRL en
dc.relation.ispartofseries 1997-1 en
dc.title A dense-time temporal logic with nice compositionality properties en
dc.type Article en
dc.identifier.doi https://doi.org/10.1007/bfb0025039
dc.researchgroup Software Technology Research Laboratory (STRL)

Files in this item

This item appears in the following Collection(s)

Show simple item record