//
Home Blog Tech Safe by Design: Examples of Formal Methods in Software Engineering

Safe by Design: Examples of Formal Methods in Software Engineering

The software development industry plays a significant role in the development of modern technology as well as economic growth. This position also reverberates throughout the commercial and the scientific fields.

It is extremely vital for the end-users, hence software makers, so that the developed products work reliably and efficiently. This is because, in some instances, the systems lay the foundation for business administration and process automation.

We all think about the consequences of running a program under a variety of different scenarios. We also wonder how the program will integrate with other systems or whether this will satisfy the end-user when we write the next line of code. Did we ever have to think someone’s life depends on it? In this post, I will attempt to emphasise the existing tools for designing safety-critical systems for the implementation of clean, concise and reliable code.

Formal Methods in Software Development Life-Cycle

Formal methods are techniques used by software engineers to design safety-critical systems and their components. In software engineering, they are techniques that involve mathematical expressions to model “abstract representation” of the system.

Long story short – it uses mathematical rigour to describe/specify systems before they get implemented.

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.

//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
    • cardiac pacemaker – a device used to help control the heartbeat
    • body fluid analysis tool for treatment monitoring
  • Transportation
    • automated railway systems – Paris, France / São Paulo, Brasil
  • Aviation
    • Unmanned Aircraft Systems – NASA
    • Air traffic control – International Civil Aviation Organization (ICAO), Federal Aviation Administration (FAA), and the National Aeronautics and Space Administration (NASA)
    • Aeroplane autopilot mode (NASA)
  • Military
    • Cybersecurity – DARPA Clean-slate design of Resilient, Adaptive, Secure Hosts

Read more stories like this in our Tech category

Spread the word ...

Share on facebook
Facebook
Share on twitter
Twitter
Share on linkedin
LinkedIn
Java Developer passionate about clean and concise coding. He has professional experience in software development for range of technologies (Java, Scala, .NET, Android) and domains (publishing, pharmaceutical, chemical, leisure, travel). Graduated BSc in Computer Science and MSc in Software Engineering in Oxford Brookes University with Award for “Outstanding Achievements” for best dissertation.