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模型及其实现中的错误。本文还展示了铁路领域的一个案例研究。