Publications

This paper is towards the development of a methodology for object-oriented software development. The intention is to support effective use of a formal model for specifying and reasoning during the requirements analysis and design of a software development process. The overall purpose is to enhance the application of the Unified Modelling Language (UML) with a formal semantics in the Rational Unified Software Development Process (RUP). The semantic framework defines the meaning of some UML submodels. It identifies both the static and dynamic relationships among these submodels. Thus, the focus of this paper is the development of a semantic model to consistently combine a use-case model and a conceptual class diagram to form a system specification.

We use a formal object-oriented specification language (OOL) to formalize and combine some UML models. With the formalization, we develop a set of refinement laws of UML models that captures the essential nature, principles, nature and patterns of object-oriented design. With the support of the incremental and iterative features of object-orientation and the Rational Unified Process (RUP), our method supports precise and consistent UML model transformation. Keywords: Design patterns, model consistency, model integration, model refinement

Integrating formal methods into UML opens up a way to complement UML-based software development with precise semantics, development methodologies, as well as rigorous verification and refinement techniques. In this paper, we present an approach to integrate a formal method to practical component-based model driven development through defining a UML profile that maps the concepts of the formal method as UML stereotypes, and implementing the profile into a CASE tool. Unlike most of the previous works in this vein, which concentrate on verifying the correctness of the models built in the development process, we focus on how the full development process can be driven by applying the refinement rules of the formal method in an incremental and interactive manner. The formal method we adopt in this work is the refinement for Component and Object Systems (rCOS). We demonstrate the development activities in the CASE tool using an example.

Model-driven architecture (MDA) has become a main stream technology for software-intensive system design. The main engineering principle behind it is that the inherent complexity of software development can only be mastered by building, analyzing and manipulating system models. MDA also deals with system complexity by providing component-based design techniques, allowing independent component design, implementation and deployment, and then system integration and reconfiguration based on component interfaces. The model of a system in any stage is an integration of models of different viewpoints. Therefore, for a model-driven method to be applied effectively, it must provide a body of techniques and an integrated suite of tools for model construction, validation, and transformation. This requires a number of modeling notations for the specification of different concerns and viewpoints of the system. These notations should have formally defined syntaxes and a unified theory of semantics. The underlying theory of the method is needed to underpin the development of tools and correct use of tools in software development, as well as to formally verify and reason about properties of systems in mission-critical applications. The modeling notations, techniques, and tools must be designed so that they can be used seamlessly in supporting development activities and documentation of artifacts in software design processes. This article presents such a method, called the rCOS, focusing on the models of a system at different stages in a software development process, their semantic integration, and how they are constructed, analyzed, transformed, validated, and verified.

We present an approach to embedding a formal method into the Rational Unified Process (RUP). The purposes are: (a) to unify different views of UML, (b) to enhance RUP and UML with the formal method to improve the quality of software systems; and (c) to support effective use of the formal method for system specification and reasoning with the iterative and incremental approach in RUP. Our overall aim is to base RUP and UML on the formal method and to scale up the use of the formal method in software system development. The model is based on Hoare and He's Unifying Theories of Programming (UTP). Keywords: Object-Orientation, RUP, UML, UTP

This paper presents a formal semantics of UML sequence diagram. In abstract syntax form, a well-formed sequence diagram corresponds to an ordered hierarchical tree structure. The static semantics of a sequence diagram is to check whether it is consistent with the class diagram declaration as well as with its well-formed tree structure. Meanwhile, the dynamic semantics is defined in terms of the state transitions that are carried out by the method invocations in the diagram. When a message is executed, it must be consistent with system state, i.e., object diagram and the state diagrams of its related objects. The semantics clearly captures the consistency between sequence diagram with class diagram and state diagram. Therefore, it is useful to develop the model consistent checking functions in UML CASE tools. And it also can be used to reason about the correctness of a design model with respect to a requirement model.

In this paper, both a UML model of requirement and a UML model of a design are defined as a pair of class diagram and a family of sequence diagrams. We then give an unified semantics for models of requirements and designs. We define the consistency between a design class diagram and the interaction diagrams and show how the removal of inconsistency can be treated as a model refinement. We then formally define the correctness of UML model of design with respect to the model of requirement.

 As an joint effort between UNU-IIST and University of Macau, we are developing a tool for automatic prototype generation and analysis (AutoPA). In this paper, we present the initial version AutoPA1.0 that implements the transformations from UML system requirement models to executable prototypes. An UML system requirement consists of a use-case model and a conceptual class model. Each use case is either described as a pair of pre and post conditions in the context of the conceptual model or represented as an activity diagram drawn in MagicDraw9.5 by the user. AutoPA can transform an activity diagram into the Java code of the prototype for execution. For a use case specified in terms of its pre and post conditions, AuoPA1.0 first transforms the specification into a sequence of atomic actions to generate a corresponding activity diagram. The prototype of requirements model can be used to validate the requirements by checking the pre and post conditions of the use case operations and the system invariants. It helps to improve the understanding between customers and designers. We will use an example of a library system to illustrate the tool and its development. Keywords: Prototype, System Requirements Model, Class Diagrams, Use-Case Model, UML.

We present AutoPA, a tool to analyze and validate the consistency and functional correctness of use case designs. The tool directly generates an executable prototype from the requirements. The requirements are captured from different views of the application. Each view is constructed as UML diagram annotated with OCL specifications. Based on a formal semantics, the tool is implemented so that both syntactic and semantic consistency among the provided views can be guaranteed. Afterwards the requirements are analyzed and translated into an executable prototype, allowing the user to interactively validate the functional properties of the requirements model. We illustrate the benefits of the tool using a real-world sized example.

 We define some important concepts of component software development including, interfaces, contracts, interaction protocols, components, component compositions, component publication and refinement. We discuss the relations among these notions, difficulties and significant issues that we need to consider when developing a formal method for component-based software engineering. We argue that to deal with the challenges, there is a need in research to link existing theories and methods of programming for effective support to component-based software engineering. We then present our initiative on a unified multiview approach to modelling, design and analysis of component systems, emphasising the integration of models for different views. An initial and short version of the report has occurred as an invited paper in Proceedings International Colloquium on Theoretical Aspects of Computing (ICTAC 2005), LNCS 3722, Springer, 2005. This work is partially supported by by the NSF project 60573085. Keywords: Components, Interfaces, Contracts, Protocols, Functionality, Consistency, Composition, Refinement, Simulation

Consider a requirements model with a set of interfaces representing use cases, and a set of system sequence diagrams specifying the scenarios of the interfaces, this paper discusses how to automatically transform such a model into an inial design model by generating a protocol state machine for each interface from its sequence diagrams, and deriving a controller class as an implementation of the interface. The generated model can be severed as the starting point for the detailed object-oriented design. The contracts of the controller class ensure that the behaviour defined by the sequence diagrams is fully complied with through pre/post-conditions. The transformation takes into account the concurrency and critical area of the respective diagrams. We present the design and implementation of the transformation, which is specified using the graphical notation of QVT Relations and integrated into a CASE tool.

 Complexity of software development has to be dealt with by dividing the different aspects and different views of the system and separating different concerns in the design. This implies the need of different modelling notations and tools to support more and more phases of the entire development process. To ensure the correctness of the models produced, the tools therefore need to integrate sophisticated checkers, generators and transformations. A feasible approach to ensure high quality of such add-ins is to base them on sound formal foundations. This paper reports our experience in the work on the Common Component Modelling Example (CoCoME) and shows where such add-ins will fit. In particular, we show how the formal techniques developed in rCOS can be integrated into a component-based development process, and where it can be integrated in and provide extension to an existing successful commercial tool for adding formally supported checking, transformation and generation modules. This is published in Formal Methods and Hybrid Real-Time Systems, Essays in Honour of Dines Bjorner and Zhou Chaochen on the Occasion of Their 70th Birthdays Lecture Notes in Computer Science 4700. Keywords: Software development tool, software process, formal methods, tool design.

Consider an object-oriented model with a class diagram, and a set of object sequence diagrams, each representing the design of object interactions for a use case. This article discusses how such an OO design model can be automatically transformed into a component-based model for the purpose of reusability, maintenance, and more importantly, distributed and independent deployment. We present the design and implementation of a tool that transforms an object-oriented model to a component-based model, which are both formally defined in the rCOS method of model driven design of component-based software, in an interactive, stepwise manner. The transformation is designed using QVT Relations and implemented as part of the rCOS CASE tool.

 This article presents a mathematical characterization of object-oriented concepts by defining an observation-oriented semantics for a relational object-oriented language with a rich variety of features including subtypes, visibility, inheritance, type casting, dynamic binding and polymorphism. The language is expressive enough for the specification of object-oriented designs and programs. We also propose a calculus based on this model to support both structural and behavioral refinement of object-oriented designs. We take the approach of the development of the design calculus based on the standard predicate logic in Hoare and He's Unifying Theories of Programming (UTP). We also consider object reference in terms of object identity as values and mutually dependent methods.

 This report introduces a theory of reactive components. We model the behaviour of an individual service by a guarded-design, which enables one to separate the responsibility of clients from the commitment made by the system, and identify a component by a set of failures and divergences. Protocols are introduced to coordinate the interactions between a component and the external environment. We adopt the notion of process refinement to formalize the substitutivity of components, and provide a complete proof method based on the notion of simulations. This report also studies the algebraic properties of component combinators.