Detecting feature interactions with Cæsar/Aldébaran

Bouma and Zuidweg (Dutch PTT) formalised a simple example of feature interaction between two telephone services in LOTOS. The interaction takes place between the Abbreviated Dialling and Originating Call Screening service in the IN CS-1 Global Functional Plane. This paper reports on the results that were gained by analysing the example in Cæsar/Aldébaran, which is an advanced LOTOS verification toolbox. The results show that even for very small examples, verification goes beyond simulation and testing.