Date: April 1997
Pages: 54
In this report an analyzer based on formal methods for concurrent programs is presented. Since the seventies the Specification and Description Language SDL has been used for developing distributed and concurrent systems. These systems, which include e.g. telephone exchanges, have become extremely complicated during the last decades. Due to the complexity resulting from the concurrent transactions in systems, the development of these systems is expensive and design errors are hard to find. TNSDL is a dialect of SDL created at Nokia Telecommunications. In this report a TNSDL analyzer created in the EMMA project at the Helsinki University of Technology is presented. The analyzer first translates a TNSDL description to a Predicate/Transition net which is then analyzed with the Predicate/Transition net reachability analysis tool, PROD. In the end the analysis results are translated back to TNSDL. The EMMA analyzer supports developing and maintenance of the concurrent programs. With it various properties of the system can be proved, errors can be searched and detected and different execution paths can be traced.
Keywords: Verification, reachability analysis, Predicate/Transition nets, SDL, Emma.