Re: New Book: CONCURRENCY

[Denis A Nicole <dan@xxxxxxxxxxxxxxx>]

On Tue, 20 Apr 1999, Oyvind Teig wrote:

> Ian Robert East wrote:
> > Somewhere (don't press me for reference) I have seen 
> > published surveys that support the claim of little tangible benefit.
> 
> Does OO Sync with How We Think?
> Les Hatton, IEEE Software May/June 1998
> 
> Judith Bishop wrote:
> > This year we used the analyser and animator tool, LTSA from day 
> > one, and Wow, what a difference. 
> 
> In that context, I'm a student as well, after 24 years in the 
> business. Occam, written with a folding editor is semi-graphical! 
> The LTSA analyzer is what I've been waiting for for 8 1/2 years!
> (Not any high-end expensive tool.) Or at least what this community 
> have been telling me I should wait for.. But why did I have to 
> input FSP to it? What's wrong with occam? (WHILE loops? Variables?) 
> 
> Someone in this community was working an an occam->SMV compiler,
> I think. How did it go? 

It's me.  The occam->SMV depends on the flattening in occam->PIC which is
almost complete.    

> 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.

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