France, Robert B.

Most popular object-oriented modeling techniques (OOMTs) provide good support for the creation of conceptual models of system behavior and structure. A serious drawback of these techniques is that the concepts and notations used are not rigorously defined. This can lead to the creation of ambiguous models, and to disagreements over the proper use and interpretation of modeling constructs. An important modeling construct that is often loosely defined is aggregation. This thesis presents a precise characterization of aggregation that can help developers identify appropriate applications of the concept. Our characterization is the result of careful analysis of literature on conceptual modeling, knowledge representation and object-oriented (OO) modeling. We discuss primary and secondary properties of aggregation and propose annotations for UML (Unified Modeling Language). An extensive discussion of the more useful patterns of aggregation helps developers pick a suitable prescription of aggregation.

The rich structuring mechanisms, and abstract modeling constructs available in most graphical object-oriented modeling methods (OOMs) facilitate the creation of abstract, visually-appealing, highly-structured graphical models. On the other hand, lack of formal semantics for the modeling notation can severely limit the utility of OOMs. Formal specification techniques (FSTs) support the creation of precise and analyzable specifications, but they can be tedious to create and difficult to read, especially by system developers not trained in formal methods. The complementary strengths of OOMs and FSTs suggest that their integration can result in techniques that can be used to create precise and analyzable models. This thesis describes a technique for integrating analysis level UML (Unified Modeling Language) Class Diagrams with the formal notation Object-Z.

The use of formal methods has become increasingly important for software development. In this thesis, we present the formal specifications for a method-based authorization model for object-oriented databases. We also formalize a proposed user group structuring. We start from an existing OMT (Object Modeling Technique) description and we use Z as language for formal specification. This specification gives a precise definition of the policies and functions of this authorization system. This can be used as a basis for implementation and possible verification in those cases where a high level of security is required.