Safe by Design: Examples of Formal Methods in Software Engineering

Such models are subject to proof-check (Formal Specification) with regards to stability, cohesion and reliability. Proving validation is a core process for evaluating models using automatic theorem proofs. This is based on a set of mathematical formulas to be proven called proof obligations (Formal Verification). This allows identification of potential flaws earlier in the design stage, to prevent from “bricking” expensive systems later when placed into exploitation. Standard development techniques revolve around the following phases:

1. Requirements engineering
2. Architecture design
3. Implementation
4. Testing
5. Maintenance
6. Evolution

Some may argue that all these steps usually take place, but they must, to some extent for at least usable software with longer perspectives for exploitation. Some of the earlier steps – particularly design stages – may bring a sense of uncertainty in terms of unforeseen problems later in the process. The reasons could be:

1. Lack of grasp of the problem as a whole
2. Dispersed engineering teams have different perceptions of the end-product
3. Lack of domain knowledge
4. Inconsistent requirements
5. Yet-to-be discovered areas of expertise

These are just some avoidable factors in the completion of complex projects. Safety-critical systems, in particular, have a significant need for earlier fault detection. It is crucial to validate software faultlessness where agile incremental analysis and development bring about quality assurance concerns. Thus, that is where the implementation of such techniques finds its highest demand.

There are notable differences between standard and formal software development methods. Formal methods are somewhat supporting tools. Here, the reliability of mathematics improves software production quality at any stage. They are not necessarily there to implement data processing. Choice of programming language is irrelevant. Instead, it creates a ‘bridge’ between modelled concepts and the environment towards final software implementation: “What shall we do?” over “How shall we do this?”.

Examples of Formal Method Techniques

B method

B is an example of formal method techniques that covers the whole development life-cycle. It divides software onto separated components that further represent as Abstract Machines.

B methods represent system models in the form of mathematical expressions as an Abstract Notation Machine (AMN). These are further subject to stepwise refinement and proof obligation evaluation. This consists of verification of invariant preservation and refinement correctness.

The B method is a widely-cited technique in scientific publications concerning formal method implementation. Notably, it is used in the specification for transport automation systems in Paris and Sao Paulo, by Siemens Transportation Systems.

B Method code example: less safety-critical

This model represents the CRM software (Customer Relationship Management) to keep track of the current state of relationships. Its task is to improve user enrolment, user satisfaction rate and member retention.

1
2
3
4
5
6
7
8
9
10
11
12
13
//Data structures in use SETS PERSON; REGISTER; ACCEPTANCE
                              = {true, false} CONSTANTS max_member PROPERTIES max_member : NAT1 VARIABLES casual,
                              prospect, member, pers_data, membership, assessment //System state - must always be true
                              during proof-check execution INVARIANT casual <: PERSON & pers_data <: REGISTER
                              & membership <: PRODUCT & prospect : casual >+> pers_data & !dd.(dd:
                              dom(prospect) => dd : casual)& member : dom(prospect) <-> membership &
                              assessment : ran(prospect) --> ACCEPTANCE & !aa.(aa: dom(assessment) => aa :
                              ran(prospect))& !cc.(cc: dom(member) => cc : dom(prospect) & prospect(cc)
                              |-> true:assessment)& card(dom(member)) <= max_member Data needed for
                              proof-checking INITIALISATION casual, prospect, member, pers_data, membership, assessment
                              := {},{},{},{},{},{} END //Methods OPERATIONS add_casual(cc)= PRE cc: PERSON & cc /:
                              ran(casualr) THEN casualr := casualr ^ [cc] END; add_persdata(pd) = PRE pd: REGISTER &
                              pd /: ran(pers_datar) THEN pers_datar:= pers_datar ^[pd] END;

Z notation

Z notation is a model-based, abstract formal specification technique most compatible with object-oriented programming. Z defines system models in the form of states where each state consists of variables, values and operations that change from one state to another.

As opposed to the usability of B, which is involved in full development life-cycle, Z formalises a specification of the system at the design level.

Event-B

Event-B is an advanced implementation of the B method. Using this approach, formal software specification is the process of creating a discrete model that represents a specific state of the system. The state is an abstract representation of constants, variables and transitions (events). Part of an event is the guard that determines the condition for the transition to another other state to take place. Constructed models (blueprints) are a further subject of refinement, proof obligation and decomposition for the correctness of verification.

Evaluation

Before deciding on the use of formal methods, each architect must list the pros and cons against resources available, as well as the system’s needs.

Benefits

1. Significantly improves reliability at the design level decreasing the cost of testing
2. Improves system cohesion, reliability, and safety-critical components by fault detection on early phases in the development cycle
3. Validated models present deterministic system behaviour

Criticisms

1. Requires qualified professionals competent in either mathematics (mathematical expressions, set theory and predicate logic) or software engineering. Systems once modelled may be difficult to implement by unaccustomed programmers. “People are quite reluctant to use such methods mostly because it necessitates modifying the development process in a significant fashion.”, author of B-Methods, Abrial, once said.
2. Design proof-validation may introduce additional effort/cost to overall project estimation.

Case studies

Formal methods find use in some real-life-saving systems. Below are some examples of software and hardware products:

Medical

Transportation

Aviation

Military