What is the difference between testing and formal methods?

The pre-shipment tests all passed. Not one item on the checklist failed. The machine ran for two weeks in the factory without trouble.

Then, on site, it stopped on the third day.

You fly out and run through the same procedure dozens of times. It does not stop. The log holds only what happened immediately before and after. You take it home and try to reproduce it. Nothing. And you still have to write the corrective action report.

This bug did not escape because the testing was poor. It lives somewhere that testing, as a method, structurally cannot reach.

The range you tried, and everything that can occur

Let us clear up the most easily misunderstood point first.

Formal methods do not replace testing.

What formal methods check is the design, not the assembled machine. Whether the wiring matches the drawing, whether the motor stops within the commanded time, whether the sensor trips at the threshold in the specification — only testing can tell you that. Everything the model threw away in abstraction belongs to testing.

The two answer different questions. Testing checks whether this machine works. Formal methods check whether this design can be broken. Neither is ever sufficient on its own.

With that said, the difference fits in one line.

Testing checks the range you tried. Formal methods check every state that can occur.

That difference only matters when the bug is outside the range. And in equipment software, the most expensive bugs are usually outside the range.

Two axes and one interlock

Here is a textbook example.

There is a transfer axis and a lift axis, and their ranges of motion partly overlap. Call the overlapping part the shared zone. There is one safety condition.

Only one of the two may ever be in the shared zone.

The design goes like this. Before entering, each axis reads the state of the zone. If it is free, the axis enters; an occupancy sensor detects the entry, and the occupancy flag is raised. The other axis sees that flag and waits.

Read it, and it looks correct. And in fact it works correctly almost all of the time.

The problem is this ordering.

1. Transfer axis: reads the state of the shared zone → free
2. Lift axis:     reads the state of the shared zone → free   ← the transfer axis has not entered yet
3. Transfer axis: begins entry → occupancy sensor trips → occupancy flag = occupied
4. Lift axis:     read "free" at step 2, so it begins entry regardless
5. Both axes are inside the shared zone

The window sits between steps 1 and 3: from reading the state to the occupancy flag being raised. On the design drawing this looked like a single action — check, then enter. In reality, the check and the confirmation of occupancy are separate events, and the other axis’s check can slip in between them.

More testing does not converge on this

This design passes its tests. It passes them every time.

As long as you run it according to the procedure, the two checks will essentially never land in the same window. The window is a few control cycles wide, and during testing the commands are issued in sequence, by a script or by an operator. Unless you set out to hit it deliberately, you will not hit it.

This is the crucial point. Running a test that cannot hit it a thousand times just gives you a thousand consecutive misses.

A low probability of occurrence does not mean “run it enough times and you will eventually hit it”. Whether you hit it depends on whether the test environment is capable of opening that window at all. The supervisory cycle time changes on site. A message is delayed once. A retry occurs. A changeover shifts the spacing between commands. Only then does the window open, and the two checks fall into the same gap.

It does not appear during testing; it appears on site. And on site it does not reproduce either. This property does not come from a shortage of test hours. It comes from a structural fact: in a design where several axes, sensors and controllers move at once, there are states that appear only under a particular interleaving, and testing has no means of selecting that interleaving.

Race conditions, deadlocks and timing-dependent faults are all members of this same family.

”We tried it and it did not happen” versus “it cannot happen”

Test cases are written by humans.

So what testing checks is the cases the designer thought of. A coverage figure measures how much of what you wrote was exercised. The cases you did not write are not in the denominator. The boundary of your imagination is the boundary of your coverage.

There is an asymmetry here. A failing test carries a lot of information: something is definitely wrong. But all a passing test tells you is that it did not happen along this one path. About the ordering you never wrote, it says nothing. It says nothing, and it looks green.

Model checking does this mechanically. You write the design as states and transitions, and you write the property you want to hold. From there it examines, one after another, every state reachable from the initial state. To the question “is a state in which both axes are inside the shared zone reachable?”, it answers by examining the whole of the reachable state space. Nobody has to think of an ordering like steps 1 to 5 above. Nobody thinks of it, and if it is reachable it is found anyway.

That is the difference between “we tried it and it did not happen” and “it cannot happen”. The first is a report about the range you tried. The second is a conclusion about the whole of the range examined.

What comes back when it fails

There is one more difference, a practical one.

When a test fails, what you get is an assertion failure. You know which condition was violated. Why execution got there is something you have to trace yourself.

When a verification fails, what comes back is a sequence of events that reproduces the violation. Steps 1 to 5 above come out exactly as they stand. This is called a counterexample. Read it, and you can see which gap it went through. What a counterexample is covers this in detail.

The limits, stated honestly

If this has started to sound too good, the limits deserve to be written at the same density. There are three.

One. It checks the design and nothing else. When verification says “cannot happen”, it is saying so about the design. It says nothing about whether the implementation follows that design, whether the wiring is right, or whether the motor on the physical machine stops within the expected time. Testing does not shrink. What shrinks is one family of bugs — the ones you meant to catch in test and did not.

Two. State explosion is real. To examine every state, the state space has to fit within a size that can be examined. Add axes, add state variables, make the time granularity finer, and the combinations grow exponentially. That is why a model is an abstraction. Choosing what to throw away is the skill, and it is the limit. Throw away too much and you get counterexamples that do not exist on the physical machine. Throw away too little and the verification never finishes. There is no magic here.

Three. A proof answers only the question you asked. If you checked that both axes never enter the shared zone at the same time, then that is all that was checked. Nothing about a third axis, nothing about recovery from emergency stop. Writing the safety properties correctly is a human job. Ask the wrong question and you will get a confident answer to the wrong question. If someone tells you they “proved everything”, ask them what they proved.

With all that said, what remains, remains. Whether a design permits a particular ordering can be settled mechanically — without the physical machine, and without anyone having to think of it. That is all it does. And that one thing is what testing cannot do.

What to read next

How to read and use the sequence of events that comes back when a verification fails is covered in What a counterexample is.

Why this method is a requirement in the standards rather than a hobbyist’s concern is in Why safety standards ask for formal methods.