Formal Model Checking

FormalModelChecking is commonly called ModelChecking? by its proponents. It is a new SPIN-off from the idea of ProofOfCorrectness.

Why not just call it ModelChecking? Is there some InformalModelChecking that is used in practice?

Unlike most FormalMethods it makes computer programs do the heavy lifting. One of these tools is called SPIN and has been used on NASA and Lucent software as an experiment.

It targets nasty real time race hazards and bugs that happen when very rare sequence of events occur. Rather than testing to see if a particular scenario causes a problem (like a UnitTest for example) a model check is given some requirement and then goes to hunt for a scenario that breaks it. They are capable of predicting that no scenario can possibly break a requirement.

In both reported tests of model checking some bad things were uncovered that nobody knew were there.

The model in model checking is a finite state abstraction of the software. The requirements are expressed in some kind of logic.

Expenses: deriving the model demands some understanding of state machines as well as code. Expressing the requirements in logic is also a specialized skill -- even if some specification patterns have been documented plus the kinds of well formed formulae needed to express them.

Catch: The code may not implement the model. The formula that expresses the requirements will almost certainly be incomplete and need tuning.

-- DickBotting (in haste,.... back later) (Several months later -- waiting 20041029)

CategoryFormalMethods