Specification decomposition for synthesis from libraries of LTL Assume/Guarantee contracts

Antonio Iannopollo, Stavros Tripakis, Alberto Sangiovanni-Vincentelli

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

1 Citation (Scopus)

Abstract

Contract-Based Design is a methodology that allows for compositional design of complex systems. Given a contract representing a specification, it is possible to formally satisfy it by composing a number of simpler contracts. When these simpler contracts are chosen from a library of existing solutions, we talk about synthesis from contract libraries. There are techniques to automate the synthesis process, but they are computationally intensive, especially for complex specifications. In this paper, we describe an efficient technique to partition a specification, i.e., an LTL-based Assume/Guarantee contract, in a number of simpler sub-specifications which can be satisfied independently. Once all these smaller problems are solved, it is possible to safely merge their solutions to satisfy the original specification. We show the effectiveness of our technique in an industrial case study.

Original languageEnglish
Title of host publicationProceedings of the 2018 Design, Automation and Test in Europe Conference and Exhibition, DATE 2018
PublisherIEEE
Pages1574-1579
Number of pages6
ISBN (Electronic)9783981926316
DOIs
Publication statusPublished - 19 Apr 2018
MoE publication typeA4 Article in a conference publication
EventDesign, Automation and Test in Europe Conference and Exhibition - Dresden, Germany
Duration: 19 Mar 201823 Mar 2018

Conference

ConferenceDesign, Automation and Test in Europe Conference and Exhibition
Abbreviated titleDATE
CountryGermany
CityDresden
Period19/03/201823/03/2018

Fingerprint Dive into the research topics of 'Specification decomposition for synthesis from libraries of LTL Assume/Guarantee contracts'. Together they form a unique fingerprint.

Cite this