面向对象实时 Maude 规约的度量 LTL 属性类的模型检验
计算机科学中的逻辑
2010-09-23 v1
摘要
本文提出了一种变换方法，用于对非层次化面向对象实时 Maude 规约的两类重要度量时序逻辑（MTL）属性（即有界响应和最小间隔）进行模型检验。我们证明了该模型检验算法的正确性，当可达状态空间有限时，在合理的非齐诺假设下算法可终止。这些新的模型检验功能已被集成到实时 Maude 中，并用于分析医疗设备网络和四路交通路口系统。
引用
@article{arxiv.1009.4264,
title = {Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications},
author = {Daniela Lepri and Peter Csaba Ölveczky and Erika Ábrahám},
journal= {arXiv preprint arXiv:1009.4264},
year = {2010}
}
备注
In Proceedings RTRTS 2010, arXiv:1009.3982