Return to search

Formal Modeling Can Improve Smart Transportation Algorithm Development

201 pages / Ensuring algorithms work accurately is crucial, especially when they drive
safety critical systems like self-driving cars.
We formally model a published distributed algorithm for autonomous
vehicles to collaborate and pass thorough an intersection. Models are built and
validated using the “Labelled Transition System Analyser” (LTSA). Our models
reveal situations leading to deadlocks and crashes in the algorithm.
We demonstrate two approaches to gain insight about a large and complex
system without modeling the entire system: Modeling a sub system - If the sub
system has issues, the super system too. Modeling a fast-forwarded state - Reveals
problems that can arise later in a process.
Some productivity tools developed for distributed system development
are also presented. Manulator, our distributed system simulator, enables quick
prototyping and debugging on a single workstation. LTSA-O, extension to LTSA,
listens to messages exchanged in an execution of a distributed system and validates
it against a model.

Identiferoai:union.ndltd.org:uoregon.edu/oai:scholarsbank.uoregon.edu:1794/22608
Date06 1900
CreatorsWathugala, Wathugala Gamage Dulan Manujinda
PublisherUniversity of Oregon
Source SetsUniversity of Oregon
LanguageEnglish
Detected LanguageEnglish
TypeThesis / Dissertation
RightsCreative Commons BY-NC-ND 4.0-US

Page generated in 0.0022 seconds