Alloy is a lightweight formal modeling tool that generates instances of a software specification to check properties of the design. This work demonstrates the use of Alloy for the rapid development of autonomous vehicle driving protocols. We contribute two driving protocols: a Normal protocol that represents the unpredictable yet safe driving behavior of typical human drivers, and a Connected protocol that employs connected technology for cooperative autonomous driving. Using five properties that define safe and productive driving actions, we analyze the performance of our protocols in mixed traffic. Lightweight formal modeling is a valuable way to reason about driving protocols early in the development process because it can automate the checking of safety and productivity properties and prevent costly design flaws.

Creator

• VanValkenburg, MaryAnn E.

Contributors

• Dougherty, Daniel J.

Degree

• MS

Unit

• Computer Science

Publisher

• Worcester Polytechnic Institute

Identifier

• etd-3956

Keyword

• Formal verification
• Alloy
• Formal modeling
• Cooperative autonomous driving (CAD)

Advisor

• Dougherty, Daniel J.

Defense date

• 2020-04-02

Year

• 2020

Date created

• 2020-05-18

Resource type

• Thesis

Rights statement

• In Copyright