Abstract

Modeling the behavior of a system under development has shown to be a very effective way to ensure that it will have better chance to be constructed correctly. With the growing complexity of systems, building this model has become a major task that requires a significant time investment and a high level of expertise. Incremental approaches that help construct a system model from partial behavioral descriptions have been widely adopted. The challenge in such approaches lies in finding both the adequate behavioral formalism that fits the needs of the analyst as well as the formal composition mechanism that facilitates the generation of the expected behavioral model and produces a verifiable model. Within this framework, use case approaches have been accepted in the industry because they make the process of requirements engineering simpler. In the first stage of their development, use cases have been associated with requirements gathering and domain analysis since they allow the partial description of system behavior in a more intuitive manner. During the last decade, their use has been expanded to include all phases of the lifecycle. Consequently, the model representing use cases has an increasing importance. Although use case approaches present benefits in terms of improving the communication among stakeholders, permitting incremental construction of the system specification, and improving the requirements traceability, such approaches have some drawbacks in relation to their lack of formality. In fact, it is difficult to validate and verify use cases for completeness and consistency. This thesis addresses the problem of modeling use cases and their composition based on formal models in order to generate a system specification that can be used for validation and verification. We tackled the problem of both composing overlapping use cases that share partial similar behaviors, and composing non overlapping use cases according to additional criteria. We experimented with different formal models of use cases having different levels of expressivenesses to develop an approach for use case composition. All use case models we tackled are state-based models. We first started by proposing an approach for composing use cases expressed as extended finite state machines with variables that characterize their states. The use case model allows the definition of explicit loops. The state characterization is used as the criterion of composition. It allows the detection of common states between use cases that have to be merged in the overall system model. When composing, we proposed an approach that protects the user-defined loops from unexpected scenarios that may threaten their behavior. As a second step, we proposed to compose use cases based on the interactions they are making between each other. In this context, an interaction is defined as an invocation of a use case by another. Unlike the first approach, use cases are no more considered overlapping. When composing, we developed an approach that avoids unexpected scenarios. Finally, we proposed a general approach for composing system behaviors where partial system behaviors are defined as state based model using imperative expressions. Each use case describes a certain system concern. The imperative expression represents the composition criterion. In fact, it defines the semantics of the composition to perform. Our approach is fully automated and provides the advantage of generating a state based model that meets the intended behavior without allowing unexpected scenarios. The approach is formalized in the case of finite state machines and extended finite state machines.