Cobleigh, Assume-guarantee Verification of Source Code with Design-level Assumptions

Model checking is an automated technique that can be used to determine whether a system satisfies certain re-quired properties. To address the “state explosion ” prob-lem associated with this technique, we propose to integrate assume-guarantee verification at different phases of system development. During design, developers build abstract be-havioral models of the system components and use them to establish key properties of the system. To increase the scala-bility of model checking at this level, we have previously de-veloped techniques that automatically decompose the veri-fication task by generating component assumptions for the properties to hold. The design artifacts are subsequently used to guide the implementation of the system, but also to enable more efficient reasoning of the source code. In par-ticular, we propose to use assumptions generated for the de-sign to similarly decompose the verification of the actual system implementation. We demonstrate our approach on a significant NASA application, where design models were used to identify and correct a safety property violation, and the generated assumptions allowed us to check successfully that the property was preserved by the implementation