Compositional verification of real-time systems with Explicit Clock Temporal Logic

1996 ◽  
Vol 8 (3) ◽  
pp. 294-323 ◽  
Author(s):  
Ping Zhou ◽  
Jozef Hooman ◽  
Ruurd Kuiper
Keyword(s):  
Real Time ◽  
Temporal Logic ◽  
Compositional Verification ◽  
Real Time Systems ◽  
Time Systems

Temporal logic for real-time systems

Automatica ◽  
1992 ◽  
Vol 28 (6) ◽  
pp. 1288-1289
Author(s):  
L. Motus
Keyword(s):  
Real Time ◽  
Temporal Logic ◽  
Real Time Systems ◽  
Time Systems

scholarly journals Compositional verification of real-time systems using Ecdar

2012 ◽  
Vol 14 (6) ◽  
pp. 703-720 ◽  
Author(s):  
Alexandre David ◽  
Kim. G. Larsen ◽  
Axel Legay ◽  
Mikael H. Møller ◽  
Ulrik Nyman ◽  
...  
Keyword(s):  
Real Time ◽  
Compositional Verification ◽  
Real Time Systems ◽  
Time Systems

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

2016 ◽  
Vol 643 ◽  
pp. 38-64 ◽  
Author(s):  
Matteo Rossi ◽  
Dino Mandrioli ◽  
Angelo Morzenti ◽  
Luca Ferrucci
Keyword(s):  
Real Time ◽  
Temporal Logic ◽  
Real Time Systems ◽  
Time Systems

AN EVENT-BASED REAL-TIME LOGIC FOR THE SPECIFICATION AND ANALYSIS OF REAL-TIME SYSTEMS

1993 ◽  
Vol 02 (01) ◽  
pp. 71-91 ◽  
Author(s):  
HORNG-YUAN CHEN ◽  
JEFFREY J.P. TSAI ◽  
YAODONG BI
Keyword(s):  
Real Time ◽  
Temporal Logic ◽  
Programming Language ◽  
Target System ◽  
Real Time Systems ◽  
Testing And Debugging ◽  
Time Logic ◽  
Prolog Programming ◽  
Event Based ◽  
Time Systems

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.

Sign in / Sign up

Export Citation Format

Share Document