loading...
Specifying Urgency in Timed I/O Automata
Koblenz, Germany September 07-September 09
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.42Third IEEE International Conference o ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Biniam Gebremichael, Radboud University Nijmegen, The Netherlands
Frits Vaandrager, Radboud University Nijmegen, The Netherlands
Tools and techniques based on timed automata (such as Uppaal and the timed I/O automata framework) have proven to be extremely useful for the analysis of protocols and control software for real-time systems. However, a significant limitation of these approaches is that, due to the expressiveness of the modeling languages, timelocks - degenerate states in which time is unable to pass - can freely arise and cannot, in the general case, be detected. As a remedy to this problem Sifakis et al. advocate the use of deadline predicates for the specification of progress properties of Alur-Dill style timed automata. In this article, we extend these ideas to a more general setting, which may serve as a basis for deductive verification techniques. More specifically, we extend the TIOA framework of Lynch et al with urgency predicates. We identify a suitable language to describe the resulting timed I/O automata with urgency and show that for this language time reactivity holds by construction. We also establish that the class of timed I/O automata with urgency is closed under composition. The use of urgency predicates is compared with three alternative approaches to specifying progress properties that have been advocated in the literature: invariants, stopping conditions and deadline predicates. We argue that in practice the use of urgency predicates leads to shorter and more natural specifications than any of the other approaches. Some preliminary results on proving invariant properties of timed (I/O) automata with urgency are presented.
Citation:
Biniam Gebremichael, Frits Vaandrager, "Specifying Urgency in Timed I/O Automata," sefm, pp.64-74, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.