Database of Case Studies Achieved Using CADP

Testing of a Distributed Leader Election Algorithm.

Organisation: University Otto-von-Guericke Magdeburg and BTU Cottbus (Germany)

Method: LOTOS
Petri nets

Tools used: CADP (Construction and Analysis of Distributed Processes)
PEP (Programming Environment based on Petri nets)

Domain: Protocol Testing.

Period: 1998.

Size: approx 50 lines of LOTOS (680,000 states in the model)

Description: This work addresses the problem of test suite derivation from a formal specification of a distributed concurrent software system by defining a concurrency model, called behaviour machine (BM), and its construction algorithm from a collection of labelled transition systems (LTSs). Test derivation can be performed on the BM model in order to produce test suites that still exhibit concurrency between test events.

The construction algorithm takes a collection of LTSs and maps them into a single Petri net representing the system. This Petri net is futher used to construct its unfolding, i.e. another Petri net with a simpler structure. Then, the BM is constructed from the finite prefix of the Petri net unfolding. Finally, the test derivation approach is extended, by applying appropriate algorithms, such as to deal with the BM model.

A prototype toolset using this approach and supporting LOTOS specifications has been developed. This toolset uses the CAESAR compiler to generate a global Petri net of the specification that is subsequently used as input for the construction of the complete finite prefix of the net using the PEP tool. Finally, the behaviour machine is constructed from the prefix using the proposed algorithm. The prototype toolset has been applied for test derivation of a distributed leader election algorithm in unidirectional ring networks. The experimental results show that, as the degree of parallelism in the system increases, the BM is much smaller than the corresponding interleaved LTS model.

Conclusion: A behaviour machine model is defined and used to support test derivation for concurrent systems. The model has the advantages of being a finite description of a concurrent system that still exhibits concurrency between actions. The approach has been automated by integrating the CADP and PEP toolsets in the behaviour machine construction process, thus obtaining an efficient framework supporting test derivation for LOTOS specifications.

Publications: [Ulrich-Konig-97] Andreas Ulrich and Hartmut Konig. "Specification-based Testing of Concurrent Systems". In: Proceedings of the IFIP Joint International Conference on Formal Description Techniques and Protocol Specification, Testing, and Verification {FORTE/PSTV}'97 (Osaka, Japan), November 1997.

[Ulrich-97] Andreas Ulrich. "A description model to support test suite derivation for concurrent systems". In: M. Zitterbart (ed.), Kommunikation in Verteilten Systemen, GI/ITG-Fachtagung KiVS'97 (Braunschweig, Germany), 1997.
Available on-line from our FTP site in PDF or PostScript
Andreas Ulrich
Siemens AG
Corporate Technology, ZT SE 1
81730 Munchen
Tel: +49-(0)89-636-47018
Fax: +49-(0)89-636-40898

Further remarks: This application, amongst others, is described on the CADP Web site:

Last modified: Fri Feb 19 09:12:04 2016.

Back to the CADP case studies page