期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2010
卷号：36
页码：137-157
DOI：10.4204/EPTCS.36.8
出版社：Open Publishing Association
摘要：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.
