基于探针和模态μ演算的实时观察者验证自动化
计算机科学中的逻辑
2015-09-23 v1
摘要
一种用于模型检测时间属性（例如使用时态逻辑的定时扩展表达的那些属性）的经典方法是依赖观察者的使用。在这种情况下，一个主要问题是证明观察者的正确性。本质上，这归结为证明：(1) 任何与属性矛盾的轨迹都能被观察者检测到；而且(2) 观察者是无害的，意味着它不能干扰被观察的系统。在本文中，我们描述了一种自动测试实时观察者正确性的方法。该方法通过自动化一种常被称为可视化验证的方法获得，其中系统的正确性通过检查其状态空间的图形表示来执行。我们的方法已在工具Tina（一个用于时间Petri网的模型检测工具箱）上实现。
引用
@article{arxiv.1509.06507,
title = {Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus},
author = {Silvano Dal Zilio and Bernard Berthomieu},
journal= {arXiv preprint arXiv:1509.06507},
year = {2015}
}
备注
This work was presented at TTCS 2015, the First IFIP International Conference on Topics in Theoretical Computer Science, August 26-28,2015. Institute for Research in Fundamental Sciences (IPM), Tehran, Iran