| dc.description.abstract | Over the past decades, society has become increasingly dependent on
computer technology, which makes it more and more important to ensure
that computer systems function correctly. Most larger computer systems
are distributed systems, which are very hard to understand and to program. During the design process, it is difficult to foresee every consequence of the design choices being made, and although extensive testing and simulation can uncover many faults, it is often not enough to guarantee that the system is free of errors. To complement other techniques for constructing reliable systems, developers can use formal methods --- mathematically-based techniques for specification and verification. Formal methods provide
a wide range of techniques for reasoning about computer systems.
This thesis gives an example of the use of formal methods in modelling
and analysing a communication protocol under development: I formally
specify the NORM multicast protocol in the specification language
Real-Time Maude, and analyse the resulting specification with the
Real-Time Maude analysis tool. In addition to presenting an analysis
of a specific protocol, the thesis investigates the usefulness of formal methods as part of the design process of distributed systems, and evaluates the applicability of the Real-Time Maude specification
formalism and tool in analysing communication protocols.
The NORM protocol, which is being developed by a working group of the
Internet Engineering Task Force (IETF), provides multicast
transport of large amounts of data using IP multicast services.
The Real-Time Maude language is a flexible and intuitive high-level formalism for specifying real-time systems, e.g. communication protocols. Real-Time Maude supports an object-oriented specification style, which is convenient for modelling distributed real-time systems. Real-Time Maude specifications are executable, and can be executed to simulate one possible behaviour of a system. Furthermore, the Real-Time Maude tool lets the user analyse every behaviour of a specification w.r.t. an initial state using timed search and model checking techniques.
Specifying (parts of) the NORM protocol in Real-Time Maude results in a high-level executable formal specification, which I analyse with the Real-Time Maude tool. The specification process uncovers some inconsistencies and ambiguities in the original informal specification, and shows that some of its procedures are not fully specified. The subsequent analysis also reveals a case where a procedure is not completely described in the
informal specification. The specification and analysis work demonstrates how formal methods, in particular the process of formalising an informal specification, can contribute to the understanding of a complex distributed system, and be of help in finding flaws and errors at an early stage in
the development process. Real-Time Maude supports a very intuitive and
natural specification style for communication protocols, and its tool
is powerful and easy to use. | nor |