Distributed software process modeling has received a great deal of attention as an effort to meet the need for cooperative development by geographically distributed teams. The AttNet model is a process modeling method, which is based on the high-level Petri nets.
This thesis provides analysis techniques to support validation and verification of software processes specified by the AttNet model. Two analysis techniques for characterizing the AttNet model are supported: one is based on the AttNet model and the other is based on the unfolding of AttNets to Predicate/Transition nets. Exploiting the hierarchical nature of the AttNet model, this technique employs abstraction methods for each activity object which is a basic functional and concurrently executable unit in the AttNet model. In cases that the properties can not be proved by the hierarchical analysis techniques, the AttNets are first unfolded into the Predicate/Transition nets before the resultant Predicate/Transition nets can be analyzed using the well-known Predicate/Transition analysis techniques. This thesis also presents the analysis framework in order to clarify the relationship between the hierarchical analysis technique and the unfolding technique.
