CaltechTHESIS
  A Caltech Library Service

Contract-Based Design: Theories and Applications

Citation

Phan-Minh, Tung (2021) Contract-Based Design: Theories and Applications. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/8vp7-kd82. https://resolver.caltech.edu/CaltechTHESIS:01132021-065636010

Abstract

Most things we know only exist in relation to one another. Their states are strongly coupled due to dependencies that arise from such relations. For a system designer, acknowledging the presence of these dependencies is as crucial to guaranteeing performance as studying them. As the roles played by technology in fields such as transportation, healthcare, and finance continue to be more profound and diverse, modern engineering systems have grown to be more reliant on the integration of technologies across multiple disciplines and their requirements. The need to ensure proper division of labor, integration of system modules, and attribution of legal responsibility calls for a more methodological look into co-design considerations. Originally conceived in computer programming, contract-based reasoning is a design approach whose promise of a formal compositional paradigm is receiving attention from a broader engineering community. Our work is dedicated to narrowing the gap between the theory and application of this yet nascent framework.

In the first half of this dissertation, we introduce a model interface contract theory for input/output automata with guards and a formalization of the directive-response architecture using assume-guarantee contracts and show how these may be used to guide the formal design of a traffic intersection and an automated valet parking system respectively. Next, we address a major drawback of assume-guarantee contracts, i.e., the problem of a void contract due to antecedent failure. Our proposed solution is a reactive version of assume-guarantee contracts that enables direct specification at the assumption and guarantee level along with a novel synthesis algorithm that exposes the effects of failures on the contract structure. This is then used to help optimize, adapt, and robustify our design against an uncertain environment.

In light of ongoing development of autonomous driving technologies and its potential impact on the safety of future transportation, the second half of this work is dedicated to the application of the design-by-contract framework to the distributed control of autonomous vehicles. We start by defining and proving properties of "assume-guarantee profiles," our proposed approach to transparent distributed multi-agent decision making and behavior prediction. Next, we provide a local conflict resolution algorithm in the context of a quasi-simultaneous game which guarantees safety and liveness to the composition of autonomous vehicle systems in this game. Finally, to facilitate the extension of these frameworks to real-life urban driving settings, we also supply an effective method to predict agent behavior that utilizes recent advances in machine learning research.

Item Type:Thesis (Dissertation (Ph.D.))
Subject Keywords:Formal Methods; Design by Contracts; Control Theory; Systems Engineering; Autonomy
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Mechanical Engineering
Minor Option:Computer Science
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Murray, Richard M.
Thesis Committee:
  • Burdick, Joel Wakeman (chair)
  • Doyle, John Comstock
  • Chandy, K. Mani
  • Murray, Richard M.
Defense Date:18 December 2020
Funders:
Funding AgencyGrant Number
Jack Kent Cooke FoundationUNSPECIFIED
Denso CorporationUNSPECIFIED
NSFUNSPECIFIED
Record Number:CaltechTHESIS:01132021-065636010
Persistent URL:https://resolver.caltech.edu/CaltechTHESIS:01132021-065636010
DOI:10.7907/8vp7-kd82
Related URLs:
URLURL TypeDescription
https://doi.org/10.23919/ACC.2019.8814789DOIArticle adapted for Chapter 3.
https://doi.org/10.1109/CDC40024.2019.9030068DOIArticle adapted for Chapter 6.
https://arxiv.org/abs/2011.14148arXivArticle adapted for Chapter 7.
https://doi.org/10.1109/CVPR42600.2020.01408DOIArticle adapted for Chapter 8.
ORCID:
AuthorORCID
Phan-Minh, Tung000-0002-1403-5197
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:14052
Collection:CaltechTHESIS
Deposited By: Tung Phan
Deposited On:19 Jan 2021 20:47
Last Modified:23 Feb 2021 22:49

Thesis Files

[img] PDF (Complete thesis) - Final Version
See Usage Policy.

7MB

Repository Staff Only: item control page