Systems Validation Centre shows Benefits of Formal Methods

by Henk Eertink, Wan Fokkink, Holger Hermanns and Izak van Langevelde

Embedded systems and network protocols have been formally verified by the Dutch Systems Validation Centre (SVC), using state-of-the-art techniques developed at international research institutes. This has led to substantial improvements in their design.

SVC was founded September 1998 as a cooperative effort of the Telematica Instituut, the Embedded Systems Group at CWI, and the Formal Methods and Tools Group at the University of Twente. Industrial support was provided by companies like CMG, IBM, KPN and Lucent. The central aim of SVC is to apply the fruits of fundamental research and tool development concerning system verification at CWI and the University of Twente to industrial cases handled by the Telematica Instituut. Thus, SVC contributes to building bridges between theory and practice, tearing down the walls of misconception about the applicability of formal methods.

This unique project builds on a strong foundation of theoretical research. On the one hand, µCRL, developed at CWI, is a language for specifying and verifying distributed embedded systems in an algebraic fashion. It is based on the classic theories of process algebra and abstract data types. On the other hand, the theory of interactive Markov chains (IMC), a conservative extension of stochastic models and, again, process algebra, forms the basis of a clean language to specify performance related properties of distributed embedded systems.

Directly resting on these theories is the development of tools. The µCRL tool set supports the analysis and manipulation of µCRL specifications. These specifications are automatically converted into a symbolic format, where a range of tools is available for optimisation, theorem proving, state space generation and model checking. Some of these tools belong to the CADP toolset developed at an ERCIM partner site at INRIA Rhone-Alpes. The same format is also supported by a novel method to specify stochastic models in terms of IMC. Dedicated analysers for performance and dependability have been developed.

In the context of SVC, the use of these tools and techniques in the development of complex embedded systems and state-of-the-art telematics standards was assessed in a number of real-world case studies. The results of these were reflected back into foundational research and tool development, by posing new theoretical questions and further challenging the developers of automated tools.

One successful case is the verification of the IEEE P1394.1 Draft Standard for High-Performance Serial Bus Bridges, which aims at the standardisation of hot-pluggable ‘bus bridges’ as a flexible means to connect FireWire serial buses. The net update fragment of this standard, which ensures the unhampered continuation of network functionality throughout addition or removal of bridges, has grown towards a protocol which is too complex to be understood by mere human wit. This research project, in cooperation with researchers from Eindhoven University of Technology, already led to the detection of and solutions to many flaws in this standard. This project continues, side by side with the IEEE standardisation body.

SVC puzzles over the IEEE P1394.1 standard for high-performance serial bus bridges. (Illustration: I.A. van Langevelde, CWI)

Another case is the verification of an Erlang optimisation of the Transaction Capabilities Procedures of the Signalling System No. 7, a protocol for intelligent network services, in close cooperation with Ericsson. Both the original and the optimised version of the protocol were formally specified, in order to verify that the latter is a correct optimisation of the former. This effort revealed a number of bugs in the optimisation, the most noticeable of which resulted in a memory leak which would have been hard to localise by more conventional means.

Together with Lucent Technologies, the stability and control of an SDH data communication network was analysed. The performance of an experimental network at Lucent was measured. Moreover, this network was formally modelled and analysed using both simulation and numerical methods. Although the main focus was on performance issues, the measurements revealed system traces that did not adhere to the specification of the intended network behaviour.

The experience gained within SVC demonstrates how formal methods have grown mature. The theoretical foundation has been proven a solid base for the construction of tool sets, the applicability of which is wide enough to span the gap between the theory of formal specification and model checking and the practice of modern embedded systems and telematics standards. SVC continues until January 2003, and has in the meanwhile stimulated various dedicated successor projects, including projects on formal testing, on performance and dependability analysis, and on improving the quality of embedded systems and of real-time distributed shared data spaces.

Links:
http://fmt.cs.utwente.nl/svc/
http://www.cwi.nl/sen2
http://www.inrialpes.fr/vasy
http://svc.telin.nl/

Please contact:
Wan Fokkink, CWI
Tel: +31 20 592 4104
E-mail: wan@cwi.nl

Henk Eertink, Telematica Instituut, The Netherlands
E-mail: Henk.Eertink@telin.nl

Holger Hermanns, University of Twente, The Netherlands
E-mail: hermanns@cs.utwente.nl