Publications

 Component-based programming is about how to create application programs by prefabricated components with new software that provides both glue between the components, and new functionality. Models of components are required to support black-box compositionality and substitutability by a third party as well as interoperability. However, the glue codes and programs designed by users of the components for new applications in general do not require these features, and they can be even designed in programming paradigms different from those of the components. In this paper, we extend the rCOS calculus of components with a model for glue programs and application programs that is different from that of components. We study the composition of a glue program with components and prove that components glued by a glue program yield a new component.

 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 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

 We construct a Galois connection between the theories that underlie CCS and CSP. It projects the complete transition system for CCS onto exactly the subset that satisfies the healthiness conditions of CSP. The construction applies to several varieties of both calculi: CCS with strong, weak or barbed simulation, and CSP with trace refinement or failures refinement, or failures/divergence.We suggest the challenge of linking other theories of concurrency by Galois connection.

 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.

 We have recently developed an object-oriented refinement calculus called rCOS. With rCOS, we formalize the object-orient design principles and patterns as refinement laws. rCOS has been proven to provide formal support to software design and program refactoring. All these features together show that rCOS can be used as a formal framework for the use-cased driven,incremental and iterative Rational Unified Process (RUP). In this paper, we apply rCOS to a step-wised development of a Point of Sale Terminal (POST) system and demonstrate how to apply the refinement laws for design and refactoring, from a requirement model to a design model, and finally, to the implementation in Visual C\#.

 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.

 Relational Calculus of Object Systems rCOS) is an OO-language which is equipped with an observation-oriented semantics and a refinement calculus based on the Hoare and He's Unifying Theories of Programming (UTP). In this paper, we give syntactic definitions for class diagrams and sequence diagrams in UML 2.0. Based on these definitions, we give an algorithm for checking the consistency of a class diagram and a sequence diagram. Furthermore, we develop an algorithm to generate rCOS code from any given consistent class diagram and sequence diagram.

 In this paper, we formalize refactoring rules as the refinement laws in rCOS [7]. Further, we also give some bigger step laws for pattern-directed refactorings. All these laws are based on the relational semantic model of rCOS.

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

 We present a method for automatically generating a prototype from a UML model of system requirements that consists of a use-case model and a conceptual class model. The method is based on a formalization of UML in which a use case is formally specified by a pair of pre and post conditions in the context of a conceptual class model. To generate a prototype, we translate the pre and post conditions of a use case into a sequence of executable atomic actions. These actions are to create or delete an object, update an object, establish or remove a link between two objects with respect to an association. Such a prototype can be used to validate requirements and check system invariants. An automated prototype generator is developed in Java, and a simple library system is used as an example to illustrate the feasibility of the method.

Two new performance estimation algorithms are presented in this report. One is an optimal lower-bound prediction for the Resource Constrained Problem, and we propose a branch-and-bound algorithm to obtain the exact solution by means of some novel bounding techniques. Experimental results show the efficiency and effect of this algorithm. The other is an approximate predication technique which is applicable to the hardware compiler for fast performance estimation. As the hardware compiler adopts the software compilation techniques, but is different from the traditional synthesis approach, the second algorithm we propose here could easily be embedded into this kind of hardware compiler to obtain results quickly.

We present a model for component software. We describe how components are specified at the interface level, design level and how they are composed. From its external view, a component consists a set of interfaces, provided to or required from its environment. From its internal view, a component is an executable code that can be coupled with other components via its interfaces. The developer has to ensure that the specification of a component is met by its design and implementation. We also combine component-based and object-oriented techniques in component-based software development This report is a refined version of UNU-IIST Report 276 and is to be presented at and published in the proceedings IFIP WCC-TCS2004, 24-26 August 2004, Toulouse, France.

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.

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.

Two-thirds simulation is equivalent to failure refinement if two redundant transition rules are added to the operational semantics of CCS. This paper also shows how to define a process calculus in which the concepts of simulation and mutual refinement coincide with testing equivalence: thus the combined benefits of all three approaches are available uniformly to all applications.

Bisimulation and its asymmetric version (simulation) are widely used in CCS to compare the behaviour of processes. In CSP, correctness issue is addressed by introducing an ordering relation known as refinement between an implementation and a specification. This report presents a new operational semantics for CSP, where two closure transitions are added to give a calculus in which simulation and refinement are identical.