CaltechTHESIS
  A Caltech Library Service

Decomposing Formal Specifications Into Assume-Guarantee Contracts for Hierarchical System Design

Citation

Filippidis, Ioannis (2019) Decomposing Formal Specifications Into Assume-Guarantee Contracts for Hierarchical System Design. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/Z9Q52MTD. https://resolver.caltech.edu/CaltechTHESIS:07202018-115217471

Abstract

Specifications for complex engineering systems are typically decomposed into specifications for individual subsystems in a way that ensures they are implementable and simpler to develop further. We describe a method to algorithmically construct specifications for components that should implement a given specification when assembled. By eliminating variables that are irrelevant to realizability of each component, we simplify the specifications and reduce the amount of information necessary for operation. To identify these variables, we parametrize the information flow between components.

The specifications are written in the Temporal Logic of Actions, TLA+, with liveness properties restricted to an implication of conjoined recurrence properties, known as GR(1). We study whether GR(1) contracts exist in the presence of full information, and prove that memoryless GR(1) contracts that preserve safety do not always exist, whereas contracts in GR(1) with history-determined variables added do exist. We observe that timed stutter-invariant specifications of open-systems in general require GR(2) liveness properties for expressing them.

We formalize a definition of realizability in TLA+, and define an operator for forming open-systems from closed-systems, based on a variant of the while-plus operator. The resulting open-system properties are realizable when expected to be. We compare stepwise implication operators from the literature, and establish relations between them, and examine the arity required for expressing these operators. We examine which symmetric combinations of stepwise implication and implementation kind avoid circular dependence, and show that only Moore components specified by strictly causal stepwise implication avoid circular dependence.

The proposed approach relies on symbolic algorithms for computing specifications. To convert the generated specifications from binary decision diagrams to readable formulas over integer variables, we symbolically solve a minimal covering problem. We implemented an algorithm for minimal covering over lattices originally proposed for two-level logic minimization. We formalized the computation of essential elements and cyclic core that is part of this algorithm, and machine-checked the proofs of safety properties using a proof assistant. Proofs supporting the thesis are organized as TLA+ modules in appendices.

Item Type:Thesis (Dissertation (Ph.D.))
Subject Keywords:Assume-guarantee contracts, System specification, Open systems, Formal languages, Realizability, Temporal logic, Temporal Logic of Actions, TLA+, Algorithmic game theory, Symbolic algorithms, Binary decision diagrams, Reactive synthesis, Logic minimization, Minimal covering, Stepwise implication, Parametric analysis
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major 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:30 November 2017
Non-Caltech Author Email:jfilippidis (AT) gmail.com
Funders:
Funding AgencyGrant Number
Microelectronics Advanced Research Corporation (MARCO)UNSPECIFIED
Defense Advanced Research Projects Agency (DARPA)UNSPECIFIED
Record Number:CaltechTHESIS:07202018-115217471
Persistent URL:https://resolver.caltech.edu/CaltechTHESIS:07202018-115217471
DOI:10.7907/Z9Q52MTD
Related URLs:
URLURL TypeDescription
https://github.com/tulip-control/omegaRelated ItemPython package: Specify and synthesize systems using symbolic algorithms
https://github.com/tulip-control/ddRelated ItemPython package: Binary Decision Diagrams (BDDs) in pure Python and Cython wrappers of CUDD, Sylvan, and BuDDy
http://dx.doi.org/10.1109/ACC.2016.7525009DOISymbolic construction of GR(1) contracts for systems with full information
https://arxiv.org/abs/1508.02705arXivSymbolic construction of GR(1) contracts for synchronous systems with full information
https://authors.library.caltech.edu/73165/Related DocumentFormalizing synthesis in TLA+
http://dx.doi.org/10.4204/EPTCS.202.6DOIA multi-paradigm language for reactive synthesis
http://dx.doi.org/10.1109/CCA.2016.7587949DOIControl design for hybrid systems with TuLiP: The Temporal Logic Planning toolbox
ORCID:
AuthorORCID
Filippidis, Ioannis0000-0003-4704-3334
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:11129
Collection:CaltechTHESIS
Deposited By: Ioannis Filippidis
Deposited On:23 Jul 2018 20:31
Last Modified:04 Oct 2019 00:22

Thesis Files

[img]
Preview
PDF (PhD dissertation) - Final Version
See Usage Policy.

700kB
[img]
Preview
PDF (Cyclic core computation specification and proofs) - Supplemental Material
See Usage Policy.

1MB
[img]
Preview
PDF (Stepwise implication operators in temporal logic) - Supplemental Material
See Usage Policy.

1MB
[img] Archive (ZIP) (TLA+ modules relevant to cyclic core computation) - Supplemental Material
See Usage Policy.

58kB
[img] Archive (ZIP) (TLA+ modules relevant to stepwise implication operators) - Supplemental Material
See Usage Policy.

57kB
[img]
Preview
PDF (Proofs on expressing nested GR(1) properties in GR(1)) - Supplemental Material
See Usage Policy.

101kB

Repository Staff Only: item control page