[e2e] Re: Protocol Verification Techniques (fwd)

[helmy]

Martin,
	You can look at the STRESS project at USC
	some of the pointers are on the project web page:
	catarina.usc.edu/stress

	a more up-to-date information and related publications are
included on my web page:
	ceng.usc.edu/~helmy under the STRESS and VINT projects under
selected publications section.

	We have studied PIM-SM, PIM-DM, MARS, timer suppression mechanisms
(e.g., SRM), and multicast congestion control (e.g., pgmcc), among others.
	The algorithms we have looked at were forward search techniques
for reachability analysis, with state space reduction using equivalences.
More interesting and efficient algorithms we have developed include
fault-oriented test generation (FOTG) and variants of it for correctness
and performance systematic testing.

	Note that this body of work addresses the question 'does a
designed protocol meet the deign requirements? and what are scenarios
under which it enters an erroneous state or has the worst-case behavior?'
	This is a bit different than saying 'does a specific
implementation of the protocol meet the design specification?' which is
often termed conformance testing.

Regards,
-Ahmed
-------

Ahmed Helmy
Assistant Professor
Electrical Engineering Department
University of Southern California
http://ceng.usc.edu/~helmy

---------- Forwarded message ----------
Date: Tue, 30 Jul 2002 15:59:39 +0100
From: Martin Koyabe <koyabe at erg.abdn.ac.uk>
To: end2end-interest at postel.org
Subject: [e2e] Re: Protocol Verification Techniques

Hi ALL,

I am writing up some research on Multicast Protocol verification techniques
(i.e. Proof that a designed protocol does what the specification says).
Does anyone have further pointers in terms of literature where I can refer
to.

Regards,

-- Martin