A temporal logic for micro- and macro-step-based real-time systems: Foundations and applications

Research on real-time systems now focuses on formal approaches to specify and analyze the behavior of real-time systems. Temporal logic is a natural candidate for this since it can specify properties of event and state sequences. However, “pure” temporal logic cannot specify “quantitative” aspect of time. The concepts of eventuality, fairness, etc. are essentially “qualitative” treatment of time. The pure temporal logic makes no reference to absolute time. For real-time systems, the pure qualitative specification and analysis of time are inadequate. In this paper, we present a modification of temporal logic—Event-based Real-time Logic (ERL), based on our event-based conceptual model. The ERL provides a high-level framework for specifying timing properties of real-time systems, and it can be implemented using Prolog programming language. In our approach to testing and debugging of real-time systems, the ERL is used to specify both expected behavior (specification) and actual behavior (execution traces) of the target system and to verify that the target system achieves the specification. In this paper, a method is presented to implement the ERL using Prolog programming language for testing and debugging real-time systems.

Download Full-text

An interval point duration temporal logic for the modeling of real time systems

First International Symposium on Control, Communications and Signal Processing, 2004. ◽

10.1109/isccsp.2004.1296210 ◽

2004 ◽

Author(s):

L.J. Ben Ayed ◽

J. Jaray

Keyword(s):

Real Time ◽

Temporal Logic ◽

Real Time Systems ◽

Time Systems

Download Full-text

Explicit clock temporal logic in constraint checking for real-time systems

Annual Review in Automatic Programming ◽

10.1016/0066-4138(91)90009-z ◽

1991 ◽

Vol 16 ◽

pp. 47-58 ◽

Cited By ~ 1

Author(s):

S Ramanna ◽

J.F Peters

Keyword(s):

Real Time ◽

Temporal Logic ◽

Real Time Systems ◽

Constraint Checking ◽

Time Systems

Download Full-text

Specification and Validation of Real Time Systems

Reconfigurable Embedded Control Systems ◽

10.4018/978-1-60960-086-0.ch017 ◽

2011 ◽

pp. 444-475

Author(s):

Olfa Mosbahi

Keyword(s):

Real Time ◽

Formal Methods ◽

Temporal Logic ◽

Formal Method ◽

The Other ◽

Real Time Systems ◽

Critical Systems ◽

Temporal Properties ◽

Integration Approach ◽

Time Systems

The chapter presents a specification technique borrowing features from two classes of specification methods, formal and semi-formal ones. Each of the above methods have been proved to be useful in the development of real-time and critical systems and widely reported in different papers (Bruel, 1996; Clarke & Wing, 1996; Cohen, 1994; Fitzgerald & Larsen, 1994; Ghezzi, Mandrioli & Morzenti, 1990). Formal methods are based on mathematical notations and axiomatic which induce verification and validation. Semi-formal methods are, in the other hand, graphic, structural and uer-friendly. Each method is applied on a suitable case study, that we regret some missing features we could find in the other class. This remark has motivated our work. We are interested in the integration of formal and semi-formal methods in order to lay out a specification approach which combines the advantages of theses two classes of methods. The proposed technique is based on the integration of the semi-formal method STATEMATE (Harel, 1997; Harel, 1987) and the temporal logic FNLOG (Sowmya & Ramesh, 1997). This choice is justified by the fact that FNLOG is formal, deals with quantitative temporal properties and that these two approaches have a compatibility which simplifies their integration (Sowmya & Ramesh, 1997). The proposed integration approach uses the notations of STATEMATE and FNLOG, defines various transformation rules of a STATEMATE specification towards FNLOG and extends the axiomatics of the temporal logic FNLOG by new lemmas to deal with duration properties. The chapter presents the various steps of our integration approach, the proposed extentions and illustrates it over a case of critical real-time systems: the gas burner system (Ravn, Rishel & Hansen, 1993).

Download Full-text