Over the past decades, society has become increasingly dependent oncomputer technology, which makes it more and more important to ensurethat computer systems function correctly. Most larger computer systemsare 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 providea wide range of techniques for reasoning about computer systems.
This thesis gives an example of the use of formal methods in modellingand analysing a communication protocol under development: I formallyspecify the NORM multicast protocol in the specification languageReal-Time Maude, and analyse the resulting specification with theReal-Time Maude analysis tool. In addition to presenting an analysisof 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 specificationformalism and tool in analysing communication protocols.
The NORM protocol, which is being developed by a working group of theInternet 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 theinformal 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 andnatural specification style for communication protocols, and its toolis powerful and easy to use.