MIRELA系统中的无限等待检测
软件工程
2015-06-12 v1 计算机科学中的逻辑
摘要
MIRELA是一种专用于虚拟与数字对象共存于同一环境并实时交互的系统的高级语言与快速原型框架。其语义以时间自动机网络的形式给出，可使用符号化方法进行检验。本文展示了如何检测此类系统各组件中的各类无限等待。该方法使用PRISM模型检测器进行了实验。
引用
@article{arxiv.1506.03553,
title = {Indefinite waitings in MIRELA systems},
author = {Johan Arcile and Jean-Yves Didier and Hanna Klaudel and Raymond Devillers and Artur Rataj},
journal= {arXiv preprint arXiv:1506.03553},
year = {2015}
}
备注
In Proceedings ESSS 2015, arXiv:1506.03250