Faculté informatique et communications IC, Section d'informatique, Institut des systèmes informatiques et multimédias ISIM (Laboratoire de génie logiciel LGL)

Specifying reactive system behavior

Sendall, Shane ; Strohmeier, Alfred (Dir.)

Thèse sciences Ecole polytechnique fédérale de Lausanne EPFL : 2002 ; no 2588.

Add to personal list
    Summary
    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.
    Résumé
    Fondamentalement, le développement des applications logicielles implique deux domaines distincts: le domaine du monde réel et le domaine du logiciel. Ces derniers convergent là où une application logicielle est employée pour transformer une situation insatisfaisante du monde réel en une situation satisfaisante. Ainsi, le développement d'applications logicielles est une activité visant à résoudre des problèmes de réalisation considérant qu’un problème a été identifié et qu’une application logicielle est désirée pour répondre à ce problème. Dans ce contexte, il est nécessaire de prendre des mesures qui assurent une solution adéquate et appropriée au problème. En particulier, il est de la plus grande importance que le problème traité et le rôle de l'applications aidant à le résoudre soient compris par l'équipe de développement d'une manière satisfaisante. Si cette condition n’est pas respectée, alors l'application créée est condamnée à être inadéquate et/ou non appropriée, indépendamment des capacités des technologies et des ressources disponibles, et aussi indépendamment des autres aspects ardus du développement de logiciel: le changement constant des besoins, la pression d’une mise sur le marché rapide, les issues sociales, politiques, morales ou économiques du projet, etc. Ceci dit, cette thèse aborde deux défis qui doivent être relevés dans chaque projet de développement d'application logicielle. Premièrement, trouver un moyen approprié pour justifier et négocier le rôle que l'application jouera dans la résolution du problème identifié. Et finalement, trouver un moyen approprié de communiquer cette connaissance aux membres de l’équipe de développement qui sont chargés de trouver une solution logicielle, sous une forme qui leur est accessible et satisfasse leurs besoins comme concepteurs. Cette thèse rapporte les moyens employés pour faire face au premier défi en tant que « stakeholders contract », ainsi que les moyens employés pour faire face au second défi en tant que « design contract ». Dans ce contexte, cette thèse étudie des techniques et des approches qui peuvent être employées pour spécifier le comportement des systèmes réactifs et qui peuvent être utilisées comme « stakeholders contract » et/ou « design contrat » sur le comportement du système. (Dans la suite, nous nous référerons respectivement au « BSC » et au « BDC »). Dans la première partie de cette thèse, un ensemble de critères qui définissent certaines qualités et caractéristiques souhaitables pour le « BSC » et le « BDC » sont donnés. En utilisant ces critères, quelques approches courantes s’accordant avec le thème de ce travail sont examinées. L'analyse des diverses approches montre qu'il y a un certain nombre de déficiences dans les approches actuelles pour répondre à ces critères. Ce résultat est employé comme motivation pour établir une nouvelle approche, dont l'objectif est d'améliorer l'état actuel de la question à l'aide de langages et d’outils communément utilisé. Par conséquent, le reste de la thèse est consacré à l'établissement de cette approche, appellée ANZAC. L'approche ANZAC utilise des langages et des outils courants, mais également beaucoup de techniques bien établies de technologie de programmation, telles que pré- et postconditions, et des principes, tels que la séparation des intérêts. Elle répond aussi bien au « BSC » qu’au « BDC » pour ce qui est de l’importance de les traiter les deux de manière unifiée, suggérant une approche simple. Cependant, en raison des intérêts distincts liés à chacun des deux contrats, deux objets de travail séparés sont employés par ANZAC (un pour chaque contrat). ANZAC définit un procédé systématique, appelé la technique de corrélation ANZAC, pour obtenir le « BDC » à partir du « BSC ». Ceci favorise le tracabilité entre les deux contrats et établit une corrélation informelle entre eux. L'aspect d’ANZAC décrivant le « BSC » est défini par les « use cases ». Le cadre proposé est une spécialisation (et clarification) des travaux sur les « use cases ». Le modèle d'ANZAC décrivant le « BDC » est défini en utilisant un sous-ensemble restreint du « Unified Modeling Language » (UML) et de son « Object Constraint Language » (OCL). Cette spécification ANZAC décrit le comportement du système respectif en utilisant un modèle qui offre trois vues complémentaires. Chaque vue capture un aspect distinct du système: état, opération et activité. La dernière partie de cette thèse montre ANZAC appliqué à une étude de cas d'un système de contrôle d'ascenseur. Elle permet de valider l'approche et montre à quel point ANZAC offre une approche propre, concise et précise pour capturer les « BSC » et les « BDC ». L'étude de cas de l’ascenseur démontre la corrélation entre les « BSC » et les « BDC » utilisant la technique de corrélation ANZAC. Elle met également en évidence la différence au niveau de la précision qui peut exister entre les deux contrats. En outre, elle démontre certaines des caractéristiques les plus avancées d’ANZAC, en particulier sa capacité à décrire des contraintes de performance et les comportements concurrents.