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