期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2010
卷号：36
页码：117-136
DOI：10.4204/EPTCS.36.7
出版社：Open Publishing Association
摘要：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.
