It’s quite impressive how safe cars, planes and trains are today.  Looking at this, it seems that we understand really well how to build reliable systems. This is in part due to safety standards.  When they are not followed, as it seems to have been the case with Toyota, things can go wrong.  Safety standards evolve, for two reasons: They evolve as we learn more about safety, and they evolve, as they need to adapt to the complexity found in today’s systems.  That’s why they started to recommend the use of formal methods.

Before we look into formal methods, and how they relate to requirements, let’s get an overview of safety standards.  The following figure has been taken from the Deploy Wiki, which provides quite a bit of analysis.

Of particular interest is IEC 61508, as it serves as the basis for domain-specific standards, like ISO 26262.  For instance, it introduces the concept of Safety Integrity Levels (SIL), a relative level of risk-reduction provided by a safety function.  In other words, the SIL level prescribes how reliable a function must be from SIL 1 (low) to SIL 4 (high).

The standards recognize that the use of formal methods is expensive, but they also recognize what formal methods are capable of.  It’s no wonder that the standards therefore focus on SIL 4, with respect to formal methods.  As the result, in IEC 61508, formal methods are “highly recommended” for SIL 4 functions.  EN 50128 (rail) even “recommends” them for SIL 1 and 2, and “highly recommends” them for SIL 3 and 4.  In fact, the rail industry is a leader in the adoption of formal methods.

An interesting exception is ISO 26262, which “recommends” formal methods, but “highly recommends” semi-formal methods.  According to the above source, this was due to lobbing by the automotive industry, being concerned about the cost overhead.

What about formal requirements?

When we talk about formal methods, we typically mean that the system description – the specification – has been formalized.  Requirements make up a significant part of the system description.  In practice, there are two approaches: Either the requirements are formalized as well, or a traceability between non-formal requirements and formal specification exists.

While formalizing requirements is possible, acceptance is low.  Rarely are stakeholders putting up with learning the formalism, so that they can understand the requirements.  Nevertheless, it is important to recognize that reading formal models is much easier than writing them.  In safety-critical domains, it can be possible to convince the customer to invest in training the stakeholders to read the formal specs.  Writing can be limited to a small circle of experts.

The opposite approach is to keep the requirements informal, but to establish a traceability to the formal model.  This is often preferred by the stakeholders, but requires discipline in keeping the traceability up to date, especially in the light of change management.  The desire to do this is reflected in the success of SysML, a dialect of UML that embraces the concepts of requirements and requirements traceability.

Seamless traceability

Rather than surrender to the static traceability model of SysML, it is worth while exploring alternative traceability models.  We at Formal Mind developed an approach that leaves sufficient room for stakeholders to express their requirements in natural language, while providing a structure that makes traceability in a formal model (Event-B, in this case), systematic and scalable.  There are countless other approaches, of course, and the challenge is to find the right approach for the project at hand (and taking the existing processes into account).

An important requisite for scalability is tool support, and Eclipse provides a powerful platform for integrating various tools for seamless traceability, as we have shown before.  These solutions have been realized using open source tools, and of course, there are plenty of commercial solutions for traceability around (like reqtify or agosense, to name just two).  Nevertheless, Eclipse contains some industry-strength components, like RMF/ProR, that are used in production environments. Alternatively, Eclipse makes it possible to quickly build prototypes at low cost, to explore different approaches.

More Information

We regularly publish our knowledge and present it at public events, like recently at TdSE (organized by the German chapter of INCOSE), and hopefully next year at ReConf 2014.  We also provide in-house trainings and workshops, covering topics like functional safety, safety standards, requirements traceability or formal modeling.  Please contact us to find out how we can make you more productive.

Image courtesy of tungphoto / FreeDigitalPhotos.net