Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications

Daniela Lepri
Peter Csaba Ölveczky
Erika Ábrahám

This paper presents a transformational approach for model checking two important classes of metric temporal logic (MTL) properties, namely, bounded response and minimum separation, for nonhierarchical object-oriented Real-Time Maude specifications. We prove the correctness of our model checking algorithms, which terminate under reasonable non-Zeno-ness assumptions when the reachable state space is finite. These new model checking features have been integrated into Real-Time Maude, and are used to analyze a network of medical devices and a 4-way traffic intersection system.

In Peter Csaba Ölveczky: Proceedings First International Workshop on Rewriting Techniques for Real-Time Systems (RTRTS 2010), Longyearbyen, April 6-9, 2010, Electronic Proceedings in Theoretical Computer Science 36, pp. 117–136.
Published: 21st September 2010.

ArXived at: bibtex PDF

Comments and questions to:
For website issues: