Articles Standards
Why safety standards ask for formal methods
Formal methods are not a new sales pitch. IEC 61508 and DO-178C both name them once the safety integrity level rises. This is why.
The first time an equipment engineer hears the words “formal methods”, the reaction is nearly always the same.
“That’s a maths thing. Nothing to do with us.”
That is fair enough. Symbols line up, the word proof appears, and it looks like something far from the daily life of people who make machines run. The kind of thing presented at conferences, with no point of contact with the machine you are commissioning on Monday morning. That is the natural reading.
There is one thing that snags, though. That “nothing to do with us” subject is named explicitly by the safety standards sitting on your own shelf.
The standards already say so
Sector by sector, it looks like this.
| Standard | Domain | Where formal methods sit |
|---|---|---|
| IEC 61508 | Functional safety (general) | Formal methods highly recommended at the top safety integrity level, SIL 4 |
| EN 50128 | Railway | Highly recommended at SIL 3 and 4 |
| ISO 26262 | Automotive | Recommended |
| DO-178C | Aerospace | A separate supplement, DO-333, sets out how to apply formal methods |
Read one line at a time, it looks like a list of recommendations. Read together, something else comes into view.
The general functional safety standard, railway, automotive, aerospace — built independently of one another, written by different committees carrying different histories of accidents. All four reach for the same technique.
The DO-178C row in particular is worth stopping on. Aerospace did not merely mention formal methods. It wrote a separate volume on how to apply them — that is DO-333.
Nobody writes a supplementary document for something nobody uses. Application guidance is needed because people actually apply it, and because the way they apply it decides whether certification passes or fails. There is a distance between a mention and a separate volume.
Why independently written standards arrived at the same conclusion
The reason is the same sentence this series has been writing throughout.
The earlier you find it, the more sharply the cost of the later stages falls.
The standards ended up at formal methods not because the theory is beautiful. It is because finding a safety-related error late simply does not pay. Found on site: rework. Found in volume production: a recall. Found after certification has passed: resubmission.
And one more thing. Past a certain level of hazard, testing alone can no longer assert that the error is absent.
This is not the standards authors being difficult. The more things move at once, the more the possible orderings grow combinatorially. Past a certain level, claiming you tried them all becomes physically impossible. SIL 4 means you have arrived there.
What certification asks about is not the number of bugs
I think this is the most important part.
What you do in certification and in a quality audit is not only to fix errors. It is to make a claim to an assessor. You say this machine is safe, and you show the grounds. What the other side is looking at is the quality of those grounds.
Put two sentences side by side.
“We tested, and the event did not occur.”
“We showed that the state is structurally unreachable.”
As sentences, they are similar. What is inside them is a different thing entirely. The first shows that something was not observed. The second shows that something does not exist.
“It did not occur” is the absence of an observation; “it cannot be reached” is the absence of the event. No number of trials closes the gap between them.
Assessors can tell the difference. So can a customer’s quality audit. When you are being asked “how many times did you test it?”, what is actually being asked is “which of the two claims are you making?”
The hard half is already done
Hearing “formal methods” makes it sound as though new work is being added from zero. That is a misunderstanding.
Your company already does risk assessment. You run HAZOP, enumerate the hazardous events, put them in a list. You carry them down into a safety requirements specification. For certification, you must already be doing this.
Look at that list again.
- Two axes enter the hazardous zone at the same time
- The transfer moves while the door is open
- A state remains from which there is no way to recover after an emergency stop
This is not paperwork for the sake of paperwork. It is exactly what formal verification eats as input. Every one of those hazard scenarios converts directly into the question “is this state reachable?”. And showing that it is unreachable is what formal methods do.
In other words, the hard half is already done. What knows the hazards is neither the standard nor the tool. It is the people who build that machine. What is missing is the means to turn that list from “it did not happen” into “it cannot happen”.
Let me put this honestly
If you have read this far and thought “we had better hurry”, stop for a moment.
Your machine is probably not SIL 4. It is not under DO-178C either. If you build ordinary factory automation equipment, there is no standard today that makes formal methods mandatory. This article was not written to make an obligation that does not exist look as though it does.
So what was the point of talking about standards?
Standards are worth reading not as orders to obey but as a signal of where the difficulty lies. The fact that four standards independently reached for the same place is information about the technique. Whether it is mandatory for you is separate information.
The industries that were not permitted to get it wrong — railways, aerospace, automotive safety mechanisms — reached for this knowing the cost. Not because they were timid. It is simply that in their world the price of finding things late was exposed first. That price is not cheaper in the equipment industry. The invoice just arrives differently.
One more practical observation. Certification pressure usually arrives from customers and export destinations before it arrives from regulators. One day a safety integrity level appears in the specification attached to an enquiry. You go to ship into a particular country and the required level is different. Wait for the regulation to change and, by the time it does, you tend to find the order of events has already left you late.
It is not mandatory now — that is correct. It will never be relevant — that is a different claim.
What to read next
So the standards recommend it. Then who actually uses it — Who actually uses this lays out the published cases alongside how far adoption has not progressed.
And what the difference between “we tested” and “we showed” amounts to as a technique is covered in What is the difference between testing and formal methods?.