Assume,guarantee or repair: a regular framework for non regular properties |
| |
Authors: | Frenkel Hadar Grumberg Orna Păsăreanu Corina S. Sheinvald Sarai |
| |
Affiliation: | 1.CISPA Helmholtz Center for Information Security, Saarbrücken, Germany ;2.Department of Computer Science, The Technion, Haifa, Israel ;3.Carnegie Mellon University, Pittsburgh, USA ;4.NASA Ames Research Center, Mountain View, CA, USA ;5.Department of Software Engineering, ORT Braude College, Karmiel, Israel ; |
| |
Abstract: | We present Assume-Guarantee-Repair (AGR)—a novel framework which verifies that a program satisfies a set of properties and also repairs the program in case the verification fails. We consider communicating programs—these are simple C-like programs, extended with synchronous actions over communication channels. Our method, which consists of a learning-based approach to assume–guarantee reasoning, performs verification and repair simultaneously: in every iteration, AGR either makes another step towards proving that the (current) system satisfies the required properties, or alters the system in a way that brings it closer to satisfying the properties. To handle infinite-state systems we build finite abstractions, for which we check the satisfaction of complex properties that contain first-order constraints, using both syntactic and semantic-aware methods. We implemented AGR and evaluated it on various communication protocols. Our experiments present compact proofs of correctness and quick repairs. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|