Combining semi-formal and formal notations in software specification: An approach to modelling time-constrained systems.

摘要

This thesis is about the integration of semi-formal, graphical representations with formal notations within a modelling approach aimed at the construction of time-constrained systems (TCS). We believe that the two types of notation, graphical (semi-formal) and, respectively, formal, can efficiently complement each other and provide the basis for a software specification approach that can be both rigorous and practical. Although many authors have envisaged the advantages of combining informality with formality in software construction, there are very few reports that address the problem within the context of object-orientation and project its solution over the canvas of TCS modelling.; The pillars of our approach are the following: the combination of formal and semi-formal notations for specification purposes, the integration into an object-oriented approach of modelling capabilities that target properties of TCS, the elaboration of detailed algorithms for UML to Z++ translations, and the proposal of a procedural frame for effective and reliable development of TCS. Principles and an outline of an algorithm for the reverse translation, from Z++ to UML are also included in the approach.; While the graphical notation employed is a subset of the UML, the formal notations used are Lano's Z++, an object-oriented variant of Z, and Jahanian and Mok's Real Time logic. Both structural and dynamic aspects of the system are considered and a new modelling element denoted class compound is proposed.; From a methodological point of view, after several UML-based modelling steps are completed the formalisation process can take Place, the result being a formal specification derived from the graphical representations obtained in the earlier steps. The integrated semi-formal and formal model of the system can be subsequently enhanced while the designed translation mechanisms allow changes in the graphical representations to be reflected into the formal specifications as well as modifications of the formal specifications to be fed back into the diagrammatic descriptions of the system.; A case study, an Elevator System, is included in the thesis to illustrate the application of the proposed approach and the GUI-centred design of Harmony, an integrated specification environment intended to support the approach, is also presented. (Abstract shortened by UMI.)