Development of consistent formal models

Abstract

Formal models can be used in the system design process to find design errors as soon as possible and to reduce the time-to-market and the development costs. Several methods for the verification of such models have been proposed in the past. However, developing such a formal model usually requires several iterations in a so-called refinement process. Between each of these steps, the consistency of the models' behavior has to be ensured as new errors can be introduced. Additionally, coverage metrics are necessary to determine if the model can be implemented yet or requires further consideration. The major contributions of this thesis are (1) a formally sound approach for the verification of model refinements, (2) a technique to retrieve correct and formal relations between the iterations of the refinement, and (3) a coverage metric for formal models.