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:
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:
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 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.
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 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.
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.
Formal methods find use in some real-life-saving systems. Below are some examples of software and hardware products:
- Cardiac pacemaker – a device used to help control the heartbeat
- Body fluid analysis tool for treatment monitoring
- Automated railway systems – Paris, France / São Paulo, Brasil
- 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)
- Cybersecurity – DARPA Clean-slate design of Resilient, Adaptive, Secure Hosts