Date: April 1997
Pages: 70
The rapid increase of parallel and distributed systems has brought new problems related to the correctness of the systems. In this work the automatic verification tool EMMA is presented, which uses Predicate/Transition nets to model TNSDL programs. The verification is based on reachability analysis with the PROD analyzer. Several methods to avoid state space explosion are discussed, e.g. model optimization, advanced state space generation algorithms and direct TNSDL program manipulation. The emphasis in this work will be on model optimizations for industrial TNSDL programs, but non-exhaustive methods are also considered. Key principles used in the modeling of TNSDL programs are also explained. In the EMMA project the {\em complete} TNSDL language has been modeled. The difference between the model and the implementation is small, because both are generated automatically from the same TNSDL specification. The results of the reachability analysis are translated back to TNSDL making the tool easier to use for specialists not acquainted with net theory.
Keywords: Verification, reachability analysis, Predicate/Transition nets, SDL, Emma.