From Code to Models

One of the corner stones of formal methods is the notion that abstract models enable analysis. By the construction of a formal model we can trade implementation detail for analytical power. The intent of a model is to preserve selected characteristics of real-world artifact, while suppressing others. Unfortunately, practitioners are less likely to use a modeling tool if it cannot real-world artifacts in their native format. The requirement to build a model to enable analysis is often seen as a verdict to design a system twice: once in a verification language and once in an implementation language. Because the implementation phase cannot be skipped, verification is often sacrificed. In this paper we will consider a way to avoid this problem by automating the extraction of verification models from implementation level code. The user now provides only model extraction rules, or abstractions, rather than full-scale models.