Synthesis of Reactive Protocols for Vehicle-to-Vehicle Communication

TL;DR

This paper introduces a synthesis method for creating reliable vehicle-to-vehicle communication protocols that meet formal safety and quality standards, demonstrated through a traffic scenario example.

Contribution

It presents a novel synthesis approach for distributed communication protocols tailored for automotive safety, including a new specification language and execution model.

Findings

Successfully synthesized a protocol for a traffic red light scenario.

Demonstrated the method's viability in real-world traffic safety applications.

Ensured protocols meet formal quality of service specifications.

Abstract

We present a synthesis method for communication protocols for active safety applications that satisfy certain formal specifications on quality of service requirements. The protocols are developed to provide reliable communication services for automobile active safety applications. The synthesis method transforms a specification into a distributed implementation of senders and receivers that together satisfy the quality of service requirements by transmitting messages over an unreliable medium. We develop a specification language and an execution model for the implementations, and demonstrate the viability of our method by developing a protocol for a traffic scenario in which a car runs a red light at a busy intersection.