Next: Task T3.3: Dissemination and
Up: Task T3.2: Assessment and
Previous: Construction of validation tools
Several encouraging results have been obtained during the first year.
One part of the results concern verifying systems beyond
the capabilities of previously existing methods such as
parametrized networks of processes, parametrized versions
of the Bounded Retransmission Protocol, IEEE root contention protocol, etc.
The second part consists of case studies showing that our
methods scale up to protocols with substantial sizes,
e.g., the protocol MASCARA.
A new specification of the PGM protocol has been produced
using the new version of IF (extended with the feature of dynamic
creation of processes), and some preliminary experimentation
has been carried out.
We have also performed some work on the modeling and verification
of the SIP protocol.
We shall not pursue the study of SIP further in the project since Ericsson
have dropped their interest in the protocol.
On the other hand, Ericsson will provide new case studies
of interest for the project.