Real-Time DEVS (RT-DEVS) can model systems with quantitative temporal requirements. Ensuring that such models verify some 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. 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.

翻译：实时DEVS（RT-DEVS）能够对具有定量时序需求的系统进行建模。为确保此类模型满足特定时序属性，需要采用超越仿真的验证手段。本研究利用模型检测工具Uppaal对RT-DEVS模型中一类周期性定量时序属性进行验证。其次，通过对定量时序属性引入变异，我们能够发现RT-DEVS模型及其实现中的潜在错误。本文还展示了铁路领域的案例研究。