Modelling in the contexts of verification and design/01. Introduction: The pragmatic view
We believe that formal methods can contribute to quality improvement of it systems, if they are applied in a pragmatic way. In our perspective pragmatism comes in two aspects:
- the application of formal methods should be efficient, and,
- after validation/verification it should be clear what the contribution to the overall quality is, or not is.
The Rationality Square shows the entities we consider and their relations. In the end, the question we are interested in is whether an artefact exhibits a certain behaviour (that typically has an informal meaning). Both, artefact and its desired behaviour are part of the physical world, the reality. Application of formal methods is always based on a verification model, i.e. a formal description (of a fragment) of the artefact. The properties that are verified are expressed formally, e.g. in some logic or as another model. Verification model and formal properties are part of the mathematical world. In this context pragmatism aspect 2) above translates to the question: to what extent is a verification of a verification model meaningful for the system in the real world?
From a minimalistic point of view verification is not more than debugging: having found a fault in the verification model that can be traced back to a fault in the real system then a real fault has been detected. However, from the absence of faults in the verification model we cannot conclude the absence of faults in the real system.
We share the minimalistic point of view in the aspect that verification of a verification model can only increase our trust that the real system exhibits the desired properties, but cannot prove its correctness. However, we belive that we can deduce more information from verification than described in the minimalistic view. The key here is the quality of the model: a good model increases our trust more than a bad one.
This immediately raises the question what the quality criteria for a good verification model are. We have identified the following ones:
q1) The verification model should mimic the relevant behaviour/structure of the real system.
q2) The verification model should be small enough to be analysed with a tool on a computer.
q3) The model should be understandable.
Before we illuminate these quality criteria in detail we want to discuss the
modelling process in itself. Modelling bridges between an object in the real
world and a formal object. Therefore, modelling cannot be a formal process
inherently. Modelling typically contains formal aspects (e.g., when we model
software automatically), and informal aspects (e.g., the choice of
abstractions, or identification of structure). This inherent informality makes
modelling a kind of ``fishy business, and many people with background in
logics or formal methods prefer to avoid this unsafe area. However, we are
convinced that modelling is a crucial element in the verification process and
we investigate to what extent we can deal with informal aspects.
The main hypothesis of our approach is that with a systematic way of modelling, where informal decisions are stated and discussed clearly, supported by checklists, schemata and standard solutions, we can derive verification models that satisfy the quality criteria and contribute to a more meaningful application of formal methods. With such a method we want to opposite the wide-spread approach of model-hacking.
