Organisation: 
University OttovonGuericke 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: 
[UlrichKonig97]
Andreas Ulrich and Hartmut Konig.
"Specificationbased 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.
[Ulrich97] Andreas Ulrich. "A description model to support test suite derivation for concurrent systems". In: M. Zitterbart (ed.), Kommunikation in Verteilten Systemen, GI/ITGFachtagung KiVS'97 (Braunschweig, Germany), 1997. Available online from the CADP Web site in PDF or PostScript 
Contact:  Andreas Ulrich Siemens AG Corporate Technology, ZT SE 1 81730 Munchen GERMANY Tel: +49(0)8963647018 Fax: +49(0)8963640898 Email: andreas.ulrich@mchp.siemens.de 
Further remarks:  This application, amongst others, is described on the CADP Web site: http://cadp.inria.fr/casestudies 