A fast service verifier for intelligent networks
Dusan Jokanovic, K. Yamano, M. Ohta, Norio Shiratori · 2003
A LOTOS verifier designed as part of the search for more usable, versatile, and efficient tools for service development in intelligent networks (INs) is reported. The verifier makes possible the automatic refutation of various bisimulation-based equivalences of LOTOS specifications. It integrates simulation and verification service design steps into one phase, making it possible to deal with large real-life service specifications. It is shown how the verifier checks for safety equivalence between two specifications of different abstraction levels of a given service. The proposed algorithm makes use of a depth-first search technique on a labeled graph generated from specifications simultaneously with the searching process. Its time and memory requirements are superior to the corresponding algorithms previously reported.>