Re: New Book: CONCURRENCY

[Bryan Scattergood <bryan@xxxxxxxx>]

On Wed, 21 Apr 1999, Denis A Nicole wrote:
> > On Tue, 20 Apr 1999, Oyvind Teig wrote:
> > WHY CAN'T I INPUT IN OCCAM?
> > It MUST be better to model check and code in the same language, eh?
> 
> That's not uncontroversial.  I think so, but others would have you design,
> prove and (maybe) check in an unexecutable specification language and
> then refine (with automated checking of the refinement) into an
> implementation language.

Okay, I'll bite. We don't have a version of FDR which accepts occam as
input because of the size of the state-space. On current PCs we
regularly check systems with around 10^8 states. Throwing time, disk
and memory at the problem might get you another order of magnitude.
That still isn't enough to explicitly check a system with one INT32,
let alone a real-world system.

You can simply ignore the state, and the paper I presented at Como in
1994 discussed doing just that. Unfortunately that throws away so much
that we never went beyond a prototype implementation.

Another approach is to use less explicit techniques (BDDs, compression
or data-independence). Those tend to require fine-tuning by
sophisticated users or are still in development.

I'll agree that ideally you would be able to check your final
implementation, but that is rarely possible with the current state of
the art. In the meantime, the best we can do is to check some
abstraction of the system. The aim of specification languages is to
make it easier to produce suitable abstractions, whether during the
design phase or after implementation.

	  Bryan

[I'm not speaking officially for Formal Systems. I just work here.]