Specifying real-time properties with metric temporal logic

1990 ◽  
Vol 2 (4) ◽  
pp. 255-299 ◽  
Author(s):  
Ron Koymans
Keyword(s):  
Real Time ◽  
Temporal Logic ◽  
Metric Temporal Logic

SPECIFYING INDUSTRIAL REAL-TIME SYSTEMS WITH A TEMPORAL LOGIC FRAMEWORK

1996 ◽  
Vol 06 (01) ◽  
pp. 21-61
Author(s):  
EMANUELE CIAPESSONI ◽  
EDOARDO CORSETTI ◽  
MANLIO MIGLIORATI ◽  
ELENA RATTO ◽  
ERNANI CRIVELLI
Keyword(s):  
Real Time ◽  
Temporal Logic ◽  
Formal Method ◽  
Object Oriented ◽  
Logical Framework ◽  
Real Time Systems ◽  
Temporal Constraint ◽  
Real Time System ◽  
Metric Temporal Logic ◽  
Time Systems

This paper presents the TRIO logical framework to specify industrial real-time systems. Typical specification requirements for this kind of system are discussed and related to corresponding features of the framework. In particular, the methodological expressiveness, the validation and the temporal constraint proof capabilities are highlighted. The former is mainly dealt with by the Object Oriented paradigm, while the latter is dealt with by a formal method specification derived from Metric Temporal Logic languages. Further, this Metric Temporal Logic is extended with the ability to treat different granularities. In order to show the capabilities of the TRIO logical framework, the specification of a complex real-time system is proposed.

Extending Linear Temporal Logic with Clocks to Object-Z

2014 ◽  
Vol 513-517 ◽  
pp. 927-930
Author(s):  
Zhi Cheng Wen ◽  
Zhi Gang Chen
Keyword(s):  
Real Time ◽  
Temporal Logic ◽  
Formal Specification ◽  
Large Scale ◽  
Linear Temporal Logic ◽  
Specification Language ◽  
Continuous Variables ◽  
Real Time System ◽  
Software Specification ◽  
Formal Specification Language

Object-Z, an extension to formal specification language Z, is good for describing large scale Object-Oriented software specification. While Object-Z has found application in a number of areas, its utility is limited by its inability to specify continuous variables and real-time constraints. Linear temporal logic can describe real-time system, but it can not deal with time variables well and also can not describe formal specification modularly. This paper extends linear temporal logic with clocks (LTLC) and presents an approach to adding linear temporal logic with clocks to Object-Z. Extended Object-Z with LTLC, a modular formal specification language, is a minimum extension of the syntax and semantics of Object-Z. The main advantage of this extension lies in that it is convenient to describe and verify the complex real-time software specification.

Real-time refinement in Manna and Pnueli's temporal logic

1996 ◽  
Vol 8 (4) ◽  
pp. 408-427 ◽  
Author(s):  
David Scholefield
Keyword(s):  
Real Time ◽  
Temporal Logic
Sign in / Sign up

Export Citation Format

Share Document