Using interface refinement to integrate formal verification into the design cycle

Abstract

We present a practical compositional interface refinement methodology which helps to integrate formal verification with the design process. One of the main verification challenges is to keep up with the changes to the specifications as the design evolves, and in particular, the transformations to the interfaces between the components. Interface changes are usually incremental, and therefore, the verification efforts after each change should also be incremental in order to be scalable. This paper presents a compositional interface refinement methodology which addresses all of these issues. We have applied this methodology in the design process of a network controller that will be used in the Smart Memory project at Stanford. The design is split into modules which are modeled as transition systems, and the properties of their interfaces are described in the First-Order LTL. We perform interface refinement by compositional reasoning with the help of an additional interface converter module. Unlike in previous approaches, the inverse converter does not need to be constructed, thus, making the verification of the refinement step simpler. © Springer-Verlag Berlin Heidelberg 2004.