loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Second International Workshop on Real-Time Computing Systems and Applications (RTCSA'95)
Verification system for real-time specification based on extended real-time logic
Tokyo, Japan
October 25-October 27
ISBN: 0-8186-7106-8
S. Yamane, Dept. of Comput. Sci., Shimane Univ., Matsue, Japan
A real-time system consists of many concurrent processes and behaves on strict timing conditions. It is important to verify the timing conditions of a real-time system. In this paper, we propose extended TCTL (Timed CTL) and effective real-time model checking as follows. (1) The timing description of extended TCTL consists of both freeze quantification and bounded temporal operator. For this extension, extended TCTL admits timing constraints between distant contexts. (2) Real time model checking consists of both labelling algorithm and geometric region method. For this method we can avoid the state explosion problem. We have develop the verification system, and show our method to be effective.
Index Terms:
real-time systems; formal specification; temporal logic; formal verification; real-time specification; extended real-time logic; Timed CTL; verification system; bounded temporal operator; freeze quantification
Citation:
S. Yamane, "Verification system for real-time specification based on extended real-time logic," rtcsa, pp.192, Second International Workshop on Real-Time Computing Systems and Applications (RTCSA'95), 1995
Usage of this product signifies your acceptance of the Terms of Use.