Interfaces and Model Checking for Software

Model checking has become a successful verification technology for hardware, because it permits the fully automatic analysis of designs. For software verification, model checkers must be applied to finite abstractions of code. This requires suitable abstractions: if the abstraction is too coarse, the model checker fails to prove the desired property; if it is too fine, the model checker fails to terminate. To address these issues, we have developed the paradigm of lazy abstraction, which automatically refines an initial Boolean abstraction locally and on demand, as long as necessary to achieve a sufficient degree of precision to pass the model checker. We have implemented our algorithm in the Berkeley Lazy Abstraction Software verification Toolkit BLAST, and we have used BLAST successfully to uncover errors in Linux and NT device drivers.
This project has three goals. First, we will apply BLAST to the NASA MDS testbed. Second, we will investigate the effectiveness of our interface formalisms for capturing the design requirements of MDS, and evolve the formalisms as necessary. Third, and most importantly, we will develop novel compositional approaches to software verification,
where model-checking is used to analyze single components and relate them to their specifications, and interfaces are used to specify and verify the interaction of the components in a design. To achieve this, we will extend BLAST to the automatic checking of component code with respect to interface specifications, which can then be checked for compatibility across components. We will also connect interfaces to the architecture of the system, enabling the compliance checking of code against an architectural or programming pattern. For instance, by relating interfaces with the class hierarchy, we can specify common behavioral constraints for subclasses such as resource access protocols, which can be then statically checked. Finally, we will extend BLAST to the automatic derivation of interfaces, which can then be propagated and verified in the system. All the techniques developed will be applied to the MDS testbed, which will benefit from the
verification effort.