It is well known that requirements engineering plays a critical role in software quality. The use case approach is a requirements elicitation technique commonly used in industrial applications. Software requirements are stated as a collection of use cases, each of which is written in the user``s perspective and describes a specific flow of events in the system. The use case approach offers several practical advantages in that use case requirements are relatively easy to describe, understand, and trace.
Unfortunately, there are a couple of major drawbacks. Since use cases are often stated in natural languages, they lack formal syntax and semantics. Furthermore, it is difficult to analyze their global system behavior for completeness and consistency partly because use cases describe only partial behaviors and because interactions among them are rarely represented explicitly.
In this dissertation, we propose the Constraints-based Modular Petri Nets(CMPNs) approach as an effective way to formalize the informal aspects of use cases. CMPNs, an extension of Place/Transition nets, allow the formal and incremental specification of requirements. The major contributions of this dissertation, in addition to the formal definitions of CMPNs, are the development of: (1) a systematic procedure to convert use cases stated in natural language to a CMPN model; and (2) a set of guidelines to find inconsistency and incompleteness in CMPNs. We demonstrate an application of our approach using use cases developed for telecommunications services.