RealTime-DEVS 中定量时序性质的验证
软件工程
2025-04-09 v3
摘要
Real-Time DEVS (RT-DEVS) 能够对具有定量时序要求的系统进行建模。为了确保此类模型满足该类时序性质，需要采用仿真之外的手段。在本工作中，我们使用模型检验工具 Uppaal 来验证 RT-DEVS 模型中出现的一类循环定量时序性质，尽管 Uppaal 通常无法处理此类性质。为了克服这些限制，我们使用了被称为自动机观测器的技术。其次，通过向定量时序性质中引入变异，我们能够发现 RT-DEVS 模型及其实现中的错误。本文给出了一个来自铁路领域的案例研究。
引用
@article{arxiv.2409.18732,
title = {Verification of Quantitative Temporal Properties in RealTime-DEVS},
author = {Ariel González and Maximiliano Cristiá and Carlos Luna},
journal= {arXiv preprint arXiv:2409.18732},
year = {2025}
}