https://murray.cds.caltech.edu/index.php?action=history&feed=atom&title=Formal_Verification_of_an_Autonomous_Vehicle_System 2026-05-24T20:00:49Z Revision history for this page on the wiki MediaWiki 1.44.2 https://murray.cds.caltech.edu/index.php?title=Formal_Verification_of_an_Autonomous_Vehicle_System&diff=19810&oldid=prev 2016-05-15T06:16:56Z

<p>htdb2wiki: creating page for 2008h_wm08-cdc.html</p> <p><b>New page</b></p><div>{{HTDB paper<br /> | authors = Tichakorn Wongpiromsarn, Richard M Murray<br /> | title = Formal Verification of an Autonomous Vehicle System<br /> | source = Conference on Decision and Control, 2008 (submitted)<br /> | year = 2008<br /> | type = Preprint<br /> | funding = <br /> | url = http://www.cds.caltech.edu/~murray/preprints/wm08-cdc_s.pdf<br /> | abstract = 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. <br /> | flags = <br /> | tag = wm08-cdc<br /> | id = 2008h<br /> }}</div>

Murray