Computer Science – Logic in Computer Science
Scientific paper
2010-09-22
EPTCS 36, 2010, pp. 137-157
Computer Science
Logic in Computer Science
In Proceedings RTRTS 2010, arXiv:1009.3982
Scientific paper
10.4204/EPTCS.36.8
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.
Meseguer Jose
Ölveczky Peter Csaba
No associations
LandOfFree
Specification and Verification of Distributed Embedded Systems: A Traffic Intersection Product Family does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Specification and Verification of Distributed Embedded Systems: A Traffic Intersection Product Family, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Specification and Verification of Distributed Embedded Systems: A Traffic Intersection Product Family will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-637555