[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: New Book: CONCURRENCY
On Wed, 21 Apr 1999, Bryan Scattergood wrote:
> 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.
I agree, you don't model-check a whole program.
> 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.
It seems to me that the program validation tool we are reaching for
integrates several technologies:
1. User input, to indicate which state can be discarded in
2. User input of "intended" assertions about the program. At its
crudest, say, loop invariants, but expressed as programming
3. Automatic proof of "regular" and unbounded parts of the
behaviour, based on 1 and 2.
4. Model checking of irregular parts.
> 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.
The specification languages do at least three things:
1. Provide a more regular semantics than most programming
languages, so reducing the technical complexity of proofs.
2. Provide mathematical structures (say sets, bags) that encourage
suitable levels of abstraction.
3. Provide a common notation for assertions and for abstract
Unfortunately they also:
1. Generate a syntactic and semantic gap between abstract designs
2. Most importantly, intimidate programmers without a mathematical
background. I believe that "real" computer scientists completely
fail to understand the limitations of ordinary programmers writing
ordinary mission-critical applications in, say, Visual BASIC.
Programming needs to be like car driving; a mass activity with
socially acceptable loss of life. It's already a mass activity;
how do we reduce the carnage?
Denis A Nicole WWW: http://www.hpcc.ecs.soton.ac.uk/~dan
High Performance Computing Centre Email: dan@xxxxxxxxxxxxxxx
University of Southampton Phone: +44 1703 592703
UK. Fax: +44 1703 593903