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...

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Peter Csaba Ölveczky, José Meseguer
• Keywords: ENTCS 2007, Real-Time Maude, Real-Time Maude Peter, Real-time Systems