Nisse Husberg
Helsinki University of Technology,
Theoretical Computer Science Laboratory,
FIN-02015 HUT, FINLAND,
Email: Nisse.Husberg@hut.fi,
WWW home page: http://www.tcs.hut.fi
and
Tapio Manner
Nokia Telecommunications,
P.O.Box 300, FIN-00045 Nokia Group, FINLAND,
Email: Tapio.Manner@ntc.nokia.com
Testing products is very expensive in the telecommunication business and remaining errors can also be very difficult to correct in a working system. In this project formal methods are used for the verification of software written in TNSDL (a dialect of SDL-88), which is used as a programming language in telecommunication products. A front-end for the PROD reachability analyser translates the TNSDL code into a high level Petri net model which can be analysed by PROD. The results are translated back to TNSDL. The complete TNSDL can be analysed, except some very difficult constructs like pointers. Dynamic processes, all data types, signals with parameters and even timers can be handled. The granularity of the model is very fine, SDL statements are considered atomary but can be folded if they are independent.