Assume-Guarantee Verification of Source Code with Design-Level Assumptions

摘要

Model checking is an automated technique that can beused to determine whether a system satisfies certain requiredproperties. To address the "state explosion" problemassociated with this technique, we propose to integrateassume-guarantee verification at different phases of systemdevelopment. During design, developers build abstract behavioralmodels of the system components and use them toestablish key properties of the system. To increase the scalabilityof model checking at this level, we have previously developedtechniques that automatically decompose the verification task by generating component assumptions for the properties to hold. The design artifacts are subsequentlyused to guide the implementation of the system, but also toenable more efficient reasoning of the source code. In particular,we propose to use assumptions generated for the designto similarly decompose the verification of the actualsystem implementation. We demonstrate our approach ona significant NASA application, where design models wereused to identify and correct a safety property violation, andthe generated assumptions allowed us to check successfullythat the property was preserved by the implementation.