[Prev][Next][Index]
larch prover and protocols
------- 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
work?
Thanks.
Duncan.
------- End of Forwarded Message
We made an experiment with the larch prover and protocols, which consists in a formal proof of a protocol for communication over faulty channels u
You can find the corresponding research report RR_2476 at:
ftp://ftp.inria.fr/INRIA/publication/RR
(see also RR_2475)
for more information, you can contact me.
Boutheina
==================^^^=====^^^=================================
CRIN & INRIA-Lorraine E-mail : chetali@loria.fr
Campus scientifique - Bureau : A-220
615 rue du jardin botanique - BP 101 Tel : (33) 83 59 30 19
54602 VILLERS LES NANCY CEDEX
FRANCE
==============================================================