FWD: Looking for comments: Verify telecommunications system

------- Forwarded Message

From: dv@srv2.med.ed.ac.uk (Duncan Verrall)
Date: Thu, 23 Feb 1995 11:59:59 GMT
Subject: Looking for comments
Newsgroups: comp.specification
Reply-To: dv@festival.ed.ac.uk

I'm looking for some comments and opinions on a project I'm about to
start on.  The aims of the project are to try to verify a telecommunications
system (looking for feature interaction problems) and, if any are found,
suggest ways of solving them.  The idea is to specify the protocols in Larch
(algebraic specification language, similar to ACT ONE) and use the Larch
theorem prover to verify some desired properties and detect interactions.

Can anybody give me an opinion on this approach?  Or any pointers to similar



------- End of Forwarded Message