Specifying reactive system behavior

Fundamentally, the development of software applications involves dealing with two distinct domains: the real world and software domains; the two converge at the point where a software application is used to make an unsatisfactory real world situation into a satisfactory one. Thus, software application development is a problem solving activity that assumes a problem has been identified and a software application is desired to address this problem. In this context, it is necessary to take measures that ensure the solution will be both adequate and appropriate with respect to the problem. In particular, it is of utmost importance that the problem in hand and the application's role in helping to solve it are satisfactorily understood by the development team. If this condition is not observed then the application produced is doomed to be inadequate and/or inappropriate, independently of the capabilities of the available technologies and resources, and also independently of other wicked aspects of software development: constantly changing requirements, time-to-market pressures, significant social, political, ethical or economic issues in the project, etc. The principal objective of this thesis was to improve the state-of-the-art of specifications that are used to communicate to the development team the behavior of the (future) system. In addressing this objective, this work initially involved defining the essential requirements of specifications that could ensure that the development team has a precise, correct and common understanding of the way the system is required to behave. As a result of analyzing the identified requirements, two general kinds of specifications were distinguished and perceived to be necessary to address the requirements adequately; one that addresses the concerns of the designers, providing a precise description of the system responsibilities; and one that addresses the concerns of the stakeholders in general, providing an informal description of the goals that the stakeholders have against the system. The first specification is referred to as the Behavioral Design Contract and the second one is referred to as the Behavioral Stakeholders Contract. In this thesis, these two specifications were concretely realized as part of the ANZAC approach. The ANZAC approach defines two work artifacts called the ANZAC use case descriptions and the ANZAC specification, which express the Behavioral Stakeholders Contract and the Behavioral Design Contract, respectively. ANZAC use case descriptions offer an informal and usage-oriented description of the concordant goals that the stakeholders have against the system. An ANZAC specification offers a precise, operational description of the system's responsibilities in servicing all possible requests that it can receive over its lifetime; it uses a restricted subset of the Unified Modeling Language (UML) and its Object Constraint Language (OCL). In the ANZAC approach, the ANZAC use case descriptions are developed following the ANZAC use case framework. This framework defines the context, purpose, style and form of an ANZAC use case description, and it provides a goal-based approach to use case elicitation. Once a number of ANZAC use case descriptions are established, they can be refined to an ANZAC specification. This refinement procedure is (informally) defined by the ANZAC mapping technique. An ANZAC specification is developed by the description of three models, which each express a different but complementary view of the system. These three models are called the Concept Model, the Operation Model, and the Protocol Model. The Concept Model defines an abstract system state space in terms of concepts from the problem domain, the Operation Model describes the effect of system operations on the system state, and the Protocol Model defines the correct behavior of the system in terms of its (allowable) input protocol. As a "proof of concept", this thesis demonstrates the ANZAC approach applied to an elevator control system, which is used to show how ANZAC offers a clean approach for capturing the Behavioral Stakeholders and Design Contract. The elevator case study demonstrates the mapping between the Behavioral Stakeholders Contract and the Behavioral Design Contract using the ANZAC mapping technique. It also highlights the difference in the level of precision and formality that can be found between ANZAC use case descriptions and an ANZAC specification. Furthermore, it demonstrates some of the more advanced features of the ANZAC approach, in particular, its ability to specify performance constraints and concurrent behavior.