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.

• Formal Assurance Process

  1. Define the aims of the project.
  2. Determine an adequate level of abstraction and scope to cover the relevant aspects of the system that the model should cover.
  3. Choose formal methods and supporting tools matching the abstraction and scope of the model and scaling to the prospective size of the modeling and verification effort.
  4. Develop a initial model, comprising
     1. core system functionality,
     2. environment constraints and usage patterns,
     3. assertions reflecting critical requirements.
  5. Grow the model, successively addressing more features and requirements.

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.