Unifying proof methodologies of duration calculus and timed linear temporal logic
Liu Z.1; Ravn A.P.4; Li X.5
Source PublicationFormal Aspects of Computing
AbstractLinear temporal logic (LTL) has been widely used for specification and verification of reactive systems. Its standard model is sequences of states (or state transitions), and formulas describe sequencing of state transitions. When LTL is used to model real-time systems, a state is extended with a time stamp to record when a state transition takes place. Duration calculus (DC) is another well studied approach for real-time systems development. DC models behaviours of a system by functions from the domain of reals representing time to the system states. This paper extends this time domain to the Cartesian product of the real and the natural numbers. With the extended time domain, we provide the chop modality with a non-overlapping interpretation. This allows some linear temporal operators explicitly dealing with the discrete dimension of time to be derivable from the chop modality in essentially the same way that their continuous-time counterparts are in the classical DC. This provides a nice embedding of some timed LTL (TLTL) modalities into DC to unify the methods from DC and LTL for real-time systems development: Requirements and high level design decisions are interval properties and are therefore specified and reasoned about in DC, while properties of an implementation, as well as the refinement relation between two implementations, are specified and verified compositionally and inductively in LTL. Implementation properties are related to requirement and design properties by rules for lifting LTL formulas to DC formulas. BCS © 2004.
KeywordDesign Real-time Refinement Specification Verification
URLView the original
Fulltext Access
Citation statistics
Cited Times [WOS]:3   [WOS Record]     [Related Records in WOS]
Document TypeConference paper
Affiliation1.United Nations University
2.United Nations University
3.University of Leicester
4.Aalborg Universitet
5.Universidade de Macau
Recommended Citation
GB/T 7714
Liu Z.,Ravn A.P.,Li X.. Unifying proof methodologies of duration calculus and timed linear temporal logic[C],2004:140-154.
APA Liu Z.,Ravn A.P.,&Li X..(2004).Unifying proof methodologies of duration calculus and timed linear temporal logic.Formal Aspects of Computing,16(2),140-154.
Files in This Item:
There are no files associated with this item.
Related Services
Recommend this item
Usage statistics
Export to Endnote
Google Scholar
Similar articles in Google Scholar
[Liu Z.]'s Articles
[Ravn A.P.]'s Articles
[Li X.]'s Articles
Baidu academic
Similar articles in Baidu academic
[Liu Z.]'s Articles
[Ravn A.P.]'s Articles
[Li X.]'s Articles
Bing Scholar
Similar articles in Bing Scholar
[Liu Z.]'s Articles
[Ravn A.P.]'s Articles
[Li X.]'s Articles
Terms of Use
No data!
Social Bookmark/Share
All comments (0)
No comment.

Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.