Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability
arXiv (Cornell University)(2016)
摘要
The realizability problem in requirements engineering is to determine the existence of an implementation that meets the given formal requirements. A step forward after realizability is proven, is to construct such an implementation automatically, and thus solve the problem of program synthesis. In this paper, we propose a novel approach to pro- gram synthesis guided by k-inductive proofs of realizability of assume- guarantee contracts constructed from safety properties. The proof of re- alizability is performed over a set of forall-exists formulas, and synthesis is per- formed by extracting Skolem functions witnessing the existential quan- tification. These Skolem functions can then be combined into an imple- mentation. Our approach is implemented in the JSyn tool which con- structs Skolem functions from a contract written in a variant of the Lus- tre programming language and then compiles the Skolem functions into a C language implementation. For a variety of benchmark models that already contained hand-written implementations, we are able to identify the usability and effectiveness of the synthesized counterparts, assuming a component-based verification framework.
更多查看译文
关键词
skolemized proofs,contracts,synthesis,assume-guarantee
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要