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

TL;DR

This paper presents a formal specification and verification approach for a distributed embedded traffic intersection system, addressing challenges like state space explosion and real-time features, validated through an industry case study.

Contribution

It introduces a formal verification method for a distributed traffic intersection system using Real-Time Maude, demonstrating its effectiveness in a real-world industry case.

Findings

Successful formal verification of safety and liveness requirements

Effective handling of asynchronous message passing in distributed systems

Validation of the approach through an industry case study

Abstract

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.