Formal Modeling Can Improve Smart Transportation Algorithm Development
| dc.contributor.author | Wathugala, Wathugala Gamage Dulan Manujinda | |
| dc.date.accessioned | 2017-08-31T22:57:47Z | |
| dc.date.available | 2017-08-31T22:57:47Z | |
| dc.date.issued | 2017-06 | |
| dc.description | 201 pages | en_US |
| dc.description.abstract | 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. | en_US |
| dc.identifier.uri | https://hdl.handle.net/1794/22608 | |
| dc.language.iso | en | en_US |
| dc.publisher | University of Oregon | en_US |
| dc.rights | Creative Commons BY-NC-ND 4.0-US | en_US |
| dc.subject | Autonomous vehicles | en_US |
| dc.subject | Distributed Mutual Exclusion Algorithm for Intersection Traffic Control | en_US |
| dc.subject | Labelled Transition System Analyser | en_US |
| dc.subject | LTSA-O | en_US |
| dc.subject | Manulator | en_US |
| dc.subject | Modeling and simulation | en_US |
| dc.title | Formal Modeling Can Improve Smart Transportation Algorithm Development | en_US |
| dc.type | Thesis / Dissertation | en_US |