Towards Synthesis from Assume-Guarantee Contracts involving Infinite Theories: A Preliminary Report
Loading...
View/Download File
Persistent link to this item
Statistics
View StatisticsJournal Title
Journal ISSN
Volume Title
Title
Towards Synthesis from Assume-Guarantee Contracts involving Infinite Theories: A Preliminary Report
Published Date
2016
Publisher
ACM
Type
Report
Abstract
In previous work, we have introduced a contract-based {em realizability checking} algorithm for assume-guarantee contracts involving infinite theories, such as linear integer/real arithmetic and uninterpreted functions over infinite domains. This algorithm can determine whether or not it is possible to construct a realization (i.e. an implementation) of an assume-guarantee contract. The algorithm is similar to k-induction model checking, but involves the use of quantifiers to determine implementability.
While our work on realizability is inherently useful for virtual integration in determining whether it is possible for suppliers to build software that meets a contract, it also provides the foundations to solving the more challenging problem of component synthesis. In this paper, we provide an initial synthesis algorithm for assume-guarantee contracts involving infinite theories. To do so, we take advantage of our realizability checking procedure and a skolemization solver for forall/exists-formulas, called AE-VAL. We show that it is possible to immediately adapt our existing algorithm towards synthesis by using this solver, using a demonstration example. We then discuss challenges towards creating a more robust synthesis algorithm.
Keywords
Description
Associated research group: Critical Systems Research Group
Related to
Replaces
License
Series/Report Number
Funding information
Isbn identifier
Doi identifier
Previously Published Citation
Appeared in the 4th FME Workshop on Formal Methods in Software Engineering, Austin, TX, May 15, 2016.
Suggested citation
Katis, Andreas; Whalen, Michael; Gacek, Andrew. (2016). Towards Synthesis from Assume-Guarantee Contracts involving Infinite Theories: A Preliminary Report. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/217447.
Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.