Refining interval temporal logic specifications

De Montfort University Open Research Archive

Show simple item record

dc.contributor.author Cau, A. (Antonio)
dc.contributor.author Zedan, Hussein
dc.date.accessioned 2005-09-05T18:47:06Z
dc.date.available 2005-09-05T18:47:06Z
dc.date.issued 1997
dc.identifier.citation Cau, Antonio and Zedan, Hussein, Refining interval temporal logic specifications. In: Transformation-based reactive systems development: 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software, ARTS'97, Palma, Mallorca, Spain, May 21-23, 1997: proceedings, Editors: Miquel Bertran and Teodor Rus, Berlin: London: Springer, 1997, Lecture notes in computer science, vol.1231, pp 79-94 en
dc.identifier.isbn 3540630104
dc.identifier.issn Transformation-based reactive systems development: 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software, ARTS'97, Palma, Mallorca, Spain, May 21-23, 1997: proceedings, Editors: Miquel Bertran and Teodor Rus, Berlin: London: Springer, 1997, Lecture notes in computer science vol.1231 pp79-94
dc.identifier.issn 0302-9743
dc.identifier.other IR/2005/17
dc.identifier.uri http://hdl.handle.net/2086/40
dc.description.abstract Interval Temporal Logic (ITL) was designed as a tool for the specification and verification of systems. The development of an executable subset of ITL, namely Tempura, was an important step in the use of temporal logic as it enables the developer to check, debug and simulate the design. However, a design methodology is missing that transforms an abstract ITL specification to an executable (concrete) Tempura program. The paper describes a development technique for ITL based on refinement calculus. The technique allows the development to proceed from high level “abstract” system specification to low level “concrete” implementation via a series of correctness preserving refinement steps. It also permits a mixture of abstract specification and concrete implementation at any development step. To allow the development of such a technique, ITL is extended to include modularity, resources and explicit communication. This allows synchronous, asynchronous and shared variable concurrency to be explicitly expressed. These constructs also help in solving the problems, like lack of expressing modularity, timing and communication, discovered during the use of ITL and Tempura for a large-scale application. en
dc.description.sponsorship Funded by EPSRC Research Grant GR/K25922: A compositional approach to the specification of systems using ITL and Tempura. en
dc.format.extent 184910 bytes
dc.format.extent 390283 bytes
dc.format.mimetype application/pdf
dc.format.mimetype application/postscript
dc.language.iso en en
dc.publisher Springer en
dc.relation.ispartofseries STRL en
dc.relation.ispartofseries 1997-2 en
dc.subject EPSRC
dc.title Refining interval temporal logic specifications en
dc.type Book chapter en
dc.researchgroup Software Technology Research Laboratory (STRL)


Files in this item

This item appears in the following Collection(s)

Show simple item record