CaltechAUTHORS
  A Caltech Library Service

Layering Assume-Guarantee Contracts for Hierarchical System Design

Filippidis, Ioannis and Murray, Richard M. (2018) Layering Assume-Guarantee Contracts for Hierarchical System Design. Proceedings of the IEEE, 106 (9). pp. 1616-1654. ISSN 0018-9219. https://resolver.caltech.edu/CaltechAUTHORS:20180920-104049492

[img] PDF - Accepted Version
See Usage Policy.

2969Kb

Use this Persistent URL to link to this item: https://resolver.caltech.edu/CaltechAUTHORS:20180920-104049492

Abstract

Specifications for complex engineering systems are typically decomposed into specifications for individual subsystems in a manner that ensures they are implementable and simpler to develop further. We describe a method to algorithmically construct component specifications that 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. We parametrize the information flow between components by introducing parameters that select whether each variable is visible to a component. The decomposition algorithm identifies which variables can be hidden while preserving realizability and ensuring correct composition, and these are eliminated from component specifications by quantification and conversion of binary decision diagrams to formulas. The resulting specifications describe component viewpoints with full information with respect to the remaining variables, which is essential for tractable algorithmic synthesis of implementations. The specifications are written in TLA + , with liveness properties restricted to an implication of conjoined recurrence properties, known as GR(1). We define an operator for forming open systems from closed systems, based on a variant of the “while-plus” operator. This operator simplifies the writing of specifications that are realizable without being vacuous. To convert the generated specifications from binary decision diagrams to readable formulas over integer variables, we symbolically solve a minimal covering problem. We show with examples how the method can be applied to obtain contracts that formalize the hierarchical structure of system design.


Item Type:Article
Related URLs:
URLURL TypeDescription
https://doi.org/10.1109/JPROC.2018.2834926DOIArticle
ORCID:
AuthorORCID
Filippidis, Ioannis0000-0003-4704-3334
Murray, Richard M.0000-0002-5785-7481
Additional Information:© 2018 IEEE. Manuscript received July 5, 2017; revised March 20, 2018; accepted May 1, 2018. Date of current version September 14, 2018. This work was supported in part by the TerraSwarm Research Center, one of six centers supported by the STARnet phase of the Focus Center Research Program (FCRP), a Semiconductor Research Corporation program sponsored by MARCO and DARPA.
Funders:
Funding AgencyGrant Number
TerraSwarm Research CenterUNSPECIFIED
Semiconductor Research CorporationUNSPECIFIED
Microelectronics Advanced Research Corporation (MARCO)UNSPECIFIED
Defense Advanced Research Projects Agency (DARPA)UNSPECIFIED
Issue or Number:9
Record Number:CaltechAUTHORS:20180920-104049492
Persistent URL:https://resolver.caltech.edu/CaltechAUTHORS:20180920-104049492
Official Citation:I. Filippidis and R. M. Murray, "Layering Assume-Guarantee Contracts for Hierarchical System Design," in Proceedings of the IEEE, vol. 106, no. 9, pp. 1616-1654, Sept. 2018. doi: 10.1109/JPROC.2018.2834926
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:89781
Collection:CaltechAUTHORS
Deposited By: Tony Diaz
Deposited On:20 Sep 2018 18:24
Last Modified:30 Jan 2020 23:12

Repository Staff Only: item control page