A Caltech Library Service

Formal Methods for Design and Verification of Embedded Control Systems: Application to an Autonomous Vehicle


Wongpiromsarn, Tichakorn (2010) Formal Methods for Design and Verification of Embedded Control Systems: Application to an Autonomous Vehicle. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/XZ3X-7V51.


The design of reliable embedded control systems inherits the difficulties involved in designing both control systems and distributed (concurrent) computing systems. Design bugs in these systems may arise from the unforeseen interactions among the computing, communication and control subsystems. Motivated by the difficulties of finding this type of design bugs, this thesis develops mathematical frameworks, based on formal methods, to facilitate the design and analysis of such embedded systems. An expressive specification language of linear temporal logic (LTL) is used to specify the desired system properties. The practicality of the proposed frameworks is demonstrated through autonomous vehicle case studies and autonomous urban driving problems.

Our approach incorporates methodology from computer science and control, including model checking, theorem proving, synthesis of digital designs, reachability analysis, Lyapunov-type methods and receding horizon control. This thesis consists of two complementary parts, namely, verification and design. First, we introduce Periodically Controlled Hybrid Automata (PCHA), a subclass of hybrid automata that abstractly captures a common design pattern in embedded control systems. New sufficient conditions that exploit the structure of PCHAs in order to simplify their invariant verification are presented.

Although the aforementioned technique simplifies an invariant verification of PCHAs, finding a proper invariant remains a challenging problem. To complement the verification efforts, in the second part of the thesis, we present a methodology for automatic synthesis of embedded control software that provides a formal guarantee of system correctness, with respect to its desired properties expressed in linear temporal logic. The correctness of the system is guaranteed even in the presence of an adversary (typically arising from changes in the environments), disturbances and modeling errors. A receding horizon framework is proposed to alleviate the associated computational complexity of LTL synthesis. The effectiveness of this framework is demonstrated through the autonomous urban driving problems.

Item Type:Thesis (Dissertation (Ph.D.))
Subject Keywords:autonomous systems, control architecture, embedded systems, hybrid automata, invariants, linear temporal logic, model checking, receding horizon control
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Mechanical Engineering
Minor Option:Control and Dynamical Systems
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Murray, Richard M.
Thesis Committee:
  • Murray, Richard M. (chair)
  • Burdick, Joel Wakeman
  • Chandy, K. Mani
  • Holzmann, Gerard J.
Defense Date:27 May 2010
Funding AgencyGrant Number
Projects:Specification, Design and Verification of Distributed Embedded Systems, Model-Based Design and Qualification of Complex Systems
Record Number:CaltechTHESIS:05272010-153304667
Persistent URL:
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:5864
Deposited By: Tichakorn Wongpiromsarn
Deposited On:04 Jun 2010 17:19
Last Modified:08 Nov 2019 18:10

Thesis Files

PDF - Final Version
See Usage Policy.


Repository Staff Only: item control page