分布式嵌入式系统的描述与验证：一个交通交叉口产品族
Specification and Verification of Distributed Embedded Systems: A Traffic Intersection Product Family
摘要：
分布式嵌入式系统（DES）不再是例外;它们是许多应用领域的规则，如航空电子，汽车工业，交通系统，传感器网络和医疗设备。由于状态空间爆炸和实时特性的需要，形式化的DES规范和验证具有挑战性。本文报告了一个广泛的基于行业的案例研究，涉及DES产品系列的行人和汽车4路交通路口，其中自主设备通过异步消息传递进行通信，而无需集中控制器。已使用实时Maude及其模型检验功能正式验证了需求文档中非正式规定的所有安全需求和活性需求。
英文摘要：
Distributed embedded systems (DESs) are no longer the exception; they are the rule in many application areas such as avionics, the automotive industry, traffic systems, sensor networks, and medical devices. Formal DES specification and verification is challenging due to state space explosion and the need to support real-time features. This paper reports on an extensive industry-based case study involving a DES product family for a pedestrian and car 4-way traffic intersection in which autonomous devices communicate by asynchronous message passing without a centralized controller. All the safety requirements and a liveness requirement informally specified in the requirements document have been formally verified using Real-Time Maude and its model checking features.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
