The careful definition of aims and scope of the formal model, the right choice of formalism and tools, and the systematic, incremental construction of the model are key factors to the success of a formal assurance project.
The following process ensures the success of a formal assurance project.
While any project profits from a clear understanding of the aims and scope right from the start, it is essential to have a clear focus right from the beginning of a formal modeling project. Only a good understanding of the aims allow one to find the right level of abstraction and to scope the formal model appropriately.
On the basis of this understanding, one can choose a formalism and analysis approach that is adequate to target the desired abstraction and scales to the size and complexity of the desired analysis. An inadequate choice of methods or tools is a serious risk to project success.
The formal model must cover the relevant system functionality. Additionally, constraints and usage patterns imposed by the environment of the system must be formalized as well, as they may be just as important to adequately reflect the workings of the system.
Formal assertions express the critical requirements of the system, whose fulfillment (or not) is to be verified in the formal assurance process. Failing to verify an assertion can point to design flaws and thus provide valuable feedback to the system developers.
Dr.-Ing. Thomas Santen, Diplom-Informatiker
Independent IT consultant
contact@formalassurance.com