Specification and Verification of Distributed Embedded Systems: A Traffic Intersection Product Family

Peter Csaba Ölveczky
(University of Oslo)
José Meseguer
(University of Illinois at Urbana-Champaign)

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.

In Peter Csaba Ölveczky: Proceedings First International Workshop on Rewriting Techniques for Real-Time Systems (RTRTS 2010), Longyearbyen, April 6-9, 2010, Electronic Proceedings in Theoretical Computer Science 36, pp. 137–157.
Published: 21st September 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.36.8 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org