[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: New Book: CONCURRENCY
- To: java-threads@xxxxxxxxx, occam-com@xxxxxxxxx
- Subject: Re: New Book: CONCURRENCY
- From: Oyvind Teig <Oyvind.Teig@xxxxxxxxxxxx>
- Date: Thu, 22 Apr 1999 08:45:55 +0200
- Alternate-recipient: Allowed
- X400-mts-identifier: [/PRMD=autronica/ADMD=TELEMAX/C=NO/;8776 99/04/22 08:45]
- X400-originator: Oyvind.Teig@xxxxxxxxxxxx
- X400-received: by mta mail.autronica.no in /PRMD=autronica/ADMD=TELEMAX/C=NO/; Relayed; Thu, 22 Apr 1999 08:45:55 +0200
- X400-recipients: non-disclosure:;
Jeremy Martin and S.A.Jassim did a state-implosion(?) in their
"A Tool for Proving Deadlock Freedom" at WoTUG-20. Jeremy mentioned
at the presentation that it might be done on occam, or a subset
of it. What's the state?
The psychology that Denis mentioned is important. I'm SO POSITIVE
to these things, but I am a real programmer in the worst sense,
and can't find a place to start filling up the semantics/syntactic
gap. I WANT ONE LANGUAGE FOR MODELING AND IMPLEMENTATION no matter
if things are 10exp8. I don't hear what your're saying.
The SPoC occam->smv, what state is it in?
Could I download (like) the free The SMV Model Checker from
and start off with occam NOW?
Will it accept my 20000 lines of occam, or will I have to write
Could this community make an occam->FSP translation (FSP is the
language they have defined in the CONCURRENCY book) - or is that
a waste if we have occam->smv?
Where does SPIN come into this picture? (Extract from my html
Reliable design of concurrent software, Holzmann,
Dr.Dobb's Journal, October 1997, SPIN, XSPIN and
PROLEMA,Chan-of-protocol metalanguage for analyzing
deadlocks etc. http://netlib.bell-labs.com/netlib/spin/.
| Oyvind Teig | oyvind.teig@xxxxxxxxxxxx |
| Navia Maritime AS, division Autronica | oyvind.teig@xxxxxxxxxxxx |
| 7005 Trondhem | http://www.navia.no | Tel:+47 73 58 12 68 |
| Norway |http://www.autronica.no | Fax:+47 73 91 93 20 |