Refining interval temporal logic specifications

Simple item page
dc.contributor.authorCau, A. (Antonio)
dc.contributor.authorZedan, Hussein
dc.date.accessioned2005-09-05T18:47:06Z
dc.date.available2005-09-05T18:47:06Z
dc.date.issued1997
dc.description.abstractInterval 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.sponsorshipFunded by EPSRC Research Grant GR/K25922: A compositional approach to the specification of systems using ITL and Tempura.en
dc.format.extent184910 bytes
dc.format.extent390283 bytes
dc.format.mimetypeapplication/pdf
dc.format.mimetypeapplication/postscript
dc.identifier.citationCau, 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-94en
dc.identifier.doihttps://doi.org/10.1007/3-540-63010-4_6
dc.identifier.isbn3540630104
dc.identifier.issn0302-9743
dc.identifier.otherIR/2005/17
dc.identifier.urihttp://hdl.handle.net/2086/40
dc.language.isoenen
dc.publisherSpringeren
dc.relation.ispartofseriesSTRLen
dc.relation.ispartofseries1997-2en
dc.researchgroupSoftware Technology Research Laboratory (STRL)
dc.subjectEPSRC
dc.titleRefining interval temporal logic specificationsen
dc.typeBook chapteren

Files

Original bundle
Now showing 1 - 2 of 2
Thumbnail Image
Name:
itlextension.pdf
Size:
180.58 KB
Format:
Adobe Portable Document Format
Description:
Main article text
Download
No Thumbnail Available
Name:
itlextension.ps
Size:
381.14 KB
Format:
Postscript Files
Description:
Main article in postscript
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.78 KB
Format:
Item-specific license agreed upon to submission
Description:
Download

Collections

School of Computer Science and Informatics