home > modelling and abstraction > formal methods and Z

Formal methods and Z

To err is human; to really foul things up you need a computer.

-- trad.

 

Some exciting new 'opportunities' possible with computers in general, and agent systems in particular, are described in 'Things that Go Bump in the Net'.

 

But even once we've specified software so that it is correct, how can we make it robust?

 

perfection is attained not when there is nothing more to add, but when there is nothing more to take away

-- Antoine de Saint Exupery

If you think that the way most software gets written today is fine, try reading the Usenet Risks Digest newsgroup for a while (also archived).

'Formal methods' is the fancy name given to good old mathematical modelling, as applied to computer systems specification and design. When used well, a formal method should yield specifications that have significant advantages over natural language documents: they are unambiguous, they can be checked mechanically, and they are open to proof.

A formal method can benefit any stage of the development lifecycle. The rigour and clarity required for its effective use open the way for any of: more effective requirements capture and analysis, cleaner and more robust architectures and designs, provably correct software, better documentation, enhanced maintainability.

Using formality isn't an 'all-or-nothing' method. It can be used selectively at any point in the development lifecycle where its benefits can be clearly justified. For example, a critical system development might require fully formal proofs at every stage, whereas a less critical application might benefit most from just a formal requirements model, followed by a more conventional software development process.

[Z]My favorite formal method is Z (pronounced 'Zed')