CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Application of Formal Verification to the Lane Change Module of an Autonomous Vehicle

Anton Zita (Institutionen för signaler och system) ; Sahar Mohajerani (Institutionen för signaler och system, Automation) ; Martin Fabian (Institutionen för signaler och system, Automation)
13th IEEE Conference on Automation Science and Engineering August 20-23,Xi'an, China, 2017 (2017)
[Konferensbidrag, refereegranskat]

For autonomous vehicles, correct behavior is of the utmost importance, as unexpected incorrect behavior can have catastrophic outcomes. However, as with any large-scale software development, it is not easy to get the system correct. As the system is made up of multiple sub-modules that interact with each other, unexpected behavior can arise from incorrect interactions when one module may have unfulfilled expectations on the other. This paper describes how formal verification was applied to the lane change module of the decision and control software (under development) for an autonomous vehicle. The module was manually modeled as an extended finite-state machine, as were some of the requirements. When applying the Supremica software to perform the formal verification, some bugs were discovered in the model. Setting up additional unit tests triggering the incorrect behavior showed that this behavior was also present in the actual code. For some of the errors, applied corrections resulted in the absence of the particular error, thus demonstrating the power of true formal verification.



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2017-09-05. Senast ändrad 2017-09-14.
CPL Pubid: 251650

 

Läs direkt!

Lokal fulltext (fritt tillgänglig)


Institutioner (Chalmers)

Institutionen för signaler och system (1900-2017)
Institutionen för signaler och system, Automation (2005-2017)

Ämnesområden

Informations- och kommunikationsteknik
Datalogi
Datorsystem
Inbäddad systemteknik

Chalmers infrastruktur