Browse wiki

From MurrayWiki
Jump to: navigation, search
Formal Verification of an Autonomous Vehicle System
Abstract Model checking is a widely used technique …
Model checking is a widely used technique for formal verification of distributed systems. It works by effectively examining the complete reachable state space of a model in order to determine whether the system satisfies its requirements or desired properties. The complexity of an autonomous vehicle system, however, renders model checking of the entire system infeasible due to the state explosion problem. In this paper, we illustrate how to exploit the structure of the system to systematically decompose the overall system-level requirements into a set of component-level requirements. Each of the components can then be model checked separately. A case study is presented where we formally verify the state consistency between different software modules of Alice, an autonomous vehicle developed by the California Institute of Technology for the 2007 DARPA Urban Challenge.
nology for the 2007 DARPA Urban Challenge.  +
Authors Tichakorn Wongpiromsarn, Richard M Murray  +
ID 2008h  +
Source Conference on Decision and Control, 2008 (submitted)  +
Tag wm08-cdc  +
Title Formal Verification of an Autonomous Vehicle System +
Type Preprint  +
Categories Papers
Modification date
This property is a special property in this wiki.
15 May 2016 06:16:56  +
URL
This property is a special property in this wiki.
http://www.cds.caltech.edu/~murray/preprints/wm08-cdc_s.pdf  +
show properties that link here 

 

Enter the name of the page to start browsing from.