[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
re: sophisticated dev/debug tools
- To: email@example.com
- Subject: re: sophisticated dev/debug tools
- From: firstname.lastname@example.org
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.