Sciweavers

Share
ENTCS
2007

Abstraction and Completeness for Real-Time Maude

8 years 3 months ago
Abstraction and Completeness for Real-Time Maude
ion and Completeness for Real-Time Maude Peter Csaba ¨Olveczky a,b and Jos´e Meseguer b a Department of Informatics, University of Oslo b Department of Computer Science, University of Illinois at Urbana-Champaign This paper presents criteria that guarantee completeness of Real-Time Maude search and temporal logic model checking analyses, under the maximal time sampling strategy, for a large class of real-time systems. As a special case, we characterize simple conditions for such completeness for object-oriented real-time systems, and show that these conditions can often be easily proved even for large and complex systems, such as advanced wireless sensor network algorithms and active network multicast protocols. Our results provide completeness and decidability of timebounded search and model checking for a large and useful class of dense-time nonZeno real-time systems far beyond the class of automaton-based real-time systems for which well known decision procedures exist. For discr...
Peter Csaba Ölveczky, José Meseguer
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Where ENTCS
Authors Peter Csaba Ölveczky, José Meseguer
Comments (0)
books