CWI (The Netherlands)
CADP (Construction and Analysis of Distributed Processes)
360 lines of LOTOS
The study centers around a LOTOS description of two telephone services
Abbreviated Dialling (ABD) and Originating Call Screening (OCS). Bouma
and Zuidweg (Dutch PTT) formalised a simple example of feature
interaction between these two services: if a dialled number is expanded
too late, it might not be recognised as belonging to the list of
numbers to be screened.
Bouma & Zuidweg's work has been extended by the use of the CADP
The verification was done by observing the graphs generated from the specification, and features were checked with testers. A tester is a simple LOTOS description which encodes a property to be checked and runs in parallel with the original specification. As soon as the property to be tested is violated, the tester fires a special error transition. These testers were used to discover errors and to prove positive properties.
This experiment is successful: the results of Bouma and Zuidweg are
strengthened by the application of verification tools. In particular
a bug was found in the model. To repair the error, the implementation
of the ABD service had to be changed.
Henri Korver, Detecting Feature Interactions with CAESAR/ALDEBARAN,
W. Bouma and H. Zuidweg. Formal Analysis of feature interactions by
model checking. Proceedings of the Second Workshop on Protocol
Verification, Eindhoven, The Netherlands, 1993
Henri Korver, Detecting Feature Interactions with CAESAR/ALDEBARAN, Science of Computer Programming, special issue on Industrially relevant Applications of Formal Analysis Techniques, J.F. Groote and M. Ren, editors, July 1997.
Available on-line from our FTP site in PDF or PostScript
P.O. Box 94079
1090 GB Amsterdam
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|