/sys/doc/ Documentation archive

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

re: sophisticated dev/debug tools

Promela and Spin are discussed at great length in the book:
	Design and Validation of Computer Protocols
	Gerard Holzmann
	published by Prentice-Hall, 1991, ISBN 0-13-539834-7

`protocols' should be understood in the most general sense of
interactions between processes; its use is not confined to network protocols
such as TCP/IP.  there might be an updated version that takes account
of changes to the language and verifier since that edition of the book was
published; i don't know.  the changes are documented in the Spin (Spin2)
distribution, which is on the net.  i haven't got the http: or ftp references
to hand, but if you go to plan9.bell-labs.com, and select Formal Verification
(something like that) or Holzmann's entry in the picture gallery, you should
come to information about Spin fairly quickly.
(the Spin distribution is nearby.)

Acme is a splendid environment available in Plan 9 (itself available from
booksellers by special order -- amazon.com knew about it last time i checked).
Acme streamlines the interface and mouse handling in Wirth's Oberon's system,
and takes it into a networked, concurrent, multi-language world.  i haven't
actually extended it in any way to support Limbo/Inferno programming, but
it would be a straightforward environment in which to do that.  you can find
a paper about Acme in the plan9 document section on plan9.bell-labs.com/plan9/

Some of the other Plan 9 papers are well worth reading to see the background
and get a feel for how the infrastructure provided by Inferno might be applied.
the Inferno/Limbo combination offers some fascinating new possibilities;
i'd go into more detail there, but i'm still coming to grips with the thing
myself!

wm/deb is the Debugger provided in the Inferno wm/logon environment.

by the way, to judge from various conference proceedings at the Spin site,
there is significant use of Promela/Spin in industry.
it's well worth a look, anyhow.