loading...
Verifying Linear Real-Time Logic Specifications
Tucson, Arizona, USA December 03-December 06
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/RTSS.2007.1428th IEEE International Real-Time Sys ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formal specification and verification are critical to the development of safe real-time and embedded systems, which have become increasingly complex. Real-Time Logic (RTL) has been used to describe the specification and safety asser- tion of real-time systems. However, the satisfiability prob- lem for RTL, as well as other first-order logics, is unde- cidable. There exist already non-trivial fragments of RTL, like path RTL and extended path RTL, for which the veri- fication can be done efficiently. The key idea used by these RTL fragments was the so-called constraint graph. The con- straint graph can express dependencies between two events, but cannot describe dependencies between three or more events. This paper presents a larger class than existing frag- ments of RTL for which the verification problem can also be solved efficiently. Our new class is called Linear Real- Time Logic (LRTL) and includes the existing decidable RTL fragments like path RTL and extended path RTL. The LRTL class is able to express any linear timing constraint with an arbitrary number of events variables (e.g., between three or more events). The main ingredient of the LRTL class is the use of matrices instead of the constraint graph, as a more powerful data structure capable of performing the conver- sion from RTL to a propositional formula. The unsatisfi- ability of the propositional formula will ensure the safety and feasibility of the given real-time system. Experimental results show that the execution times for LRTL are better than the systems expressed in extended path RTL, and com- parable with those expressed in path RTL.
Citation:
Stefan Andrei, Albert M. K. Cheng, "Verifying Linear Real-Time Logic Specifications," rtss, pp.333-342, 28th IEEE International Real-Time Systems Symposium (RTSS 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.