分布式嵌入式系统的规约与验证：交通路口产品线
计算机科学中的逻辑
2010-09-23 v1
摘要
分布式嵌入式系统（DES）已不再是特例；在航空电子、汽车工业、交通系统、传感器网络和医疗设备等许多应用领域中，它们已成为常态。由于状态空间爆炸以及需要支持实时特性，DES的形式化规约与验证极具挑战性。本文报告了一项广泛的基于工业的案例研究，涉及一个用于行人与汽车四路交通路口的DES产品线，其中自主设备通过异步消息传递进行通信，而没有集中式控制器。需求文档中非形式化规约的所有安全性需求和活性需求，均已使用实时 Maude 及其模型检验功能进行了形式化验证。
引用
@article{arxiv.1009.4265,
title = {Specification and Verification of Distributed Embedded Systems: A Traffic Intersection Product Family},
author = {Peter Csaba Ölveczky and José Meseguer},
journal= {arXiv preprint arXiv:1009.4265},
year = {2010}
}
备注
In Proceedings RTRTS 2010, arXiv:1009.3982