Verification of Quantitative Temporal Properties in RealTime-DEVS
Ariel González, Maximiliano Cristiá, Carlos Luna
TL;DR
The paper tackles the challenge of verifying quantitative temporal properties in Real-Time DEVS models, which go beyond what standard simulation can guarantee. It proposes a workflow that translates RT-DEVS models to Timed Automata and uses Uppaal with automata observers to verify a class of recurrent quantitative temporal properties expressed as patterns, without requiring full MTL support. The approach is augmented by mutation-based techniques to reveal timing-interpretation errors and to generate test cases for implementations, demonstrated on a Railway Control System case study with patterns such as Time-Bounded Response, Time-Restricted Precedence, and Conditional Security. While effective on the case study, the method acknowledges potential state-explosion and manual translation steps, and outlines future work toward automation, broader pattern support, and tool integration. Collectively, the work provides a practical pathway to combine model checking with RT-DEVS for rigorous timing verification and debugging in real-time systems.
Abstract
Real-Time DEVS (RT-DEVS) can model systems with quantitative temporal requirements. Ensuring that such models verify that kind of temporal properties requires to use something beyond simulation. In this work we use the model checker Uppaal to verify a class of recurrent quantitative temporal properties appearing in RT-DEVS models, even though Uppaal cannot deal in general with this kind of properties. In order to overcome these limitations we use the technique known as automata observer. Secondly, by introducing mutations to quantitative temporal properties we are able to find errors in RT-DEVS models and their implementations. A case study from the railway domain is presented.