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

TL;DR

This paper introduces a new method for model checking specific classes of metric temporal logic properties in object-oriented Real-Time Maude specifications, with proven correctness and practical applications in medical device networks and traffic systems.

Contribution

It presents a transformational approach for verifying bounded response and minimum separation properties, including correctness proofs and integration into Real-Time Maude.

Findings

Successfully verified properties of medical device networks

Analyzed traffic intersection system for temporal properties

Model checking algorithms terminate under certain conditions

Abstract

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.