Publications

 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 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\#.

In UML, the general structure of objects, their attributes and relations are modeled as a class graph, and an instance of a class graph is defined as an object graph. The class graph of a system determines the general properties of objects and how objects collaborate in realizing a use case. In this paper, we define class graphs and their object graphs as directed labelled graphs, and investigate in a graph theoretical approach what changes in the object structure maintain the capability of providing services. We define the general notion of structure refinements. A structure refinement is a transformation from one graph to another that preserves the capability of providing services, that is the resulting class graph should be able to provide at least as well as the original graph. We give a small set of structure refinement rules that is proved to be sound and complete for a kind of structure refinement.

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

 Concurrent programming is the activity of constructing a program containing multiple processes that execute in parallel. The aim of the course is to introduce the basic concepts, principles and techniques in programming concurrent computing systems, and to provide practice in solving problems and skill in writing concurrent programs. The course will also provide methods for evaluating systems, algorithms and languages from a broad perspective. The course provides the students with understanding of the notations of concurrency, nondeterminism, synchronization, deadlock, livelock, safety and liveness. It provides students with the history of the development different language mechanisms for the realization of synchronization and interactions, including synchronization without using synchronization primitives, synchronization by semaphores, conditional regions, monitors, hand-shake communication and remote invocation. It covers communication via shared variables and message passing.

In component-based design, a component interface specification describes the guaranteed order in which the provided methods of the component are called and the assumption about the order in which the component calls methods it requires. Automata-based formalism is widely used for interface specification and compatibility checking of components. We extend this idea by introducing reactive interface automata for modeling the interface behavior of reactive components, and active interface automata for active components. The contribution is a composable model of component interfaces that allows static compatibility checking for different kinds of composition of components through their interface models. Algorithms are given for compatibility checking and generating the interface model of a composite component from its execution model.

 Modern software development has to deal with many different aspects and different views of applications. Thus it needs 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 need to integrate sophisticated checkers, generators and transformations. A feasible approach to ensuring high quality of such add-ins is to base them on sound formal foundations. This paper summarizes our research on the Refinement of Component and Object Systems (rCOS) and illustrates it with experiences from the work on the Common Component Modelling Example (CoCoME). This gives evidence that the formal techniques developed in rCOS can be integrated into a model-driven development process and shows where it may be integrated in computer-aided software engineering (CASE) tools for adding formally supported checking, transformation and generation facilities. Keywords: Formal methods, multi-view modelling, rCOS, software design process, tool design, UML

The current dominance of the service-based paradigm reflects the success of specific design and archi- tectural principles embodied in terms like SOA and REST. This paper suggests further principles for the design of services exhibiting long-running transactions, whose characteristic feature is that in the case of failure not all system states can be automatically restored: system compensation is required. The principles are expressed at the level of scope-based compensation and fault handling and ensure the con- sistency of data critical to the business logic by demanding (a) either the commitment of all of the 'scope' or nothing in case of failure, and (b) compensation is assured in case of failure in parent scopes. The notion of scope is expressed algebraically and design guidelines are suggested to ensure transactional processes satisfy those principles. To assist validation, the algebra is translated to Coloured Petri Nets; the principles are expressed as CTL formulae; and their bounded versions are checked with the CPN Tools. A simple but typical case study, 'Batch-ATM', is used throughout to illustrate definitions and finally to demonstrate the approach.

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.

In a component-based design, a component interface specification describes the guaranteed ordering in which the component accepts calls to its provided methods and the assumption about the order in which the component calls methods it requires. Automata-based formalism is widely used for interface specification and compatibility checking of components. We extend this idea by introducing the concepts of reactive interface automata (RIA) for reactive components and active interface automata (AIA) for active components. We present a component-based architecture description language for object-oriented and service-based design in which a composite reactive component is built from a number of reactive components and active components through different operators. For the architectural operators, we provide the algorithms for constructing RIA of composite components.

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

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.

 Software development tools need to support more and more phases of the entire development process, because applications must be developed more correctly and efficiently. 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. In order to know where such add-ins will fit, we investigate the use of an existing successful commercial tool and identify suitable places for adding formally supported checking, transformation and generation modules. The paper concludes with a discussion of feasibility of developing the proposed add-ins and how to give conditions such that they will actually be used.

 The collection includes the four invited talks (one is full paper and the other three are abstracts) and the 36 accepted regular papers.

 Fault-tolerance and timing have often been considered to be implementation issues of a program, quite distinct from the functional safety and liveness properties. Recent work has shown how these non-functional and functional properties can be verified in a similar way. However, the more practical question of determining whether a real-time program will meet its deadlines, i.e., showing that there is a feasible schedule, is usually done using scheduling theory, quite separately from the verification of other properties of the program. This makes it hard to use the results of scheduling analysis in the design, or redesign, of fault-tolerant and real-time programs. In this paper we show how fault-tolerance, timing, and schedulability can be specified and verified using a single notation and model. This allows a unified view to be taken of the functional and nonfunctional properties of programs and a simple transformational method to be used to combine these properties. It also permits results from scheduling theory to be interpreted and used within a formal proof framework. The notation and model are illustrated using a simple example.

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.

In component-based design, a component interface specification describes the guaranteed order in which the provided methods of the component are called and the assumption about the order in which the component calls methods it requires. Automata-based formalism is widely used for interface specification and compatibility checking of components. We extend this idea by introducing reactive interface automata for modeling the interface behavior of reactive components, and active interface automata for active components. The contribution is a composable model of component interfaces that allows static compatibility checking for different kinds of composition of components through their interface models. Algorithms are given for compatibility checking and generating the interface model of a composite component from its execution model.

 Abstract: In UML, the general structure of objects, their attributes and relations are modeled as a class graph, and an instance of a class graph is defined as an object graph. The class graph of a system determines the general properties of objects and how objects collaborate in realizing a use case. In this paper, we define class graphs and their object graphs as directed labelled graphs, and investigate in a graph theoretical approach what changes in the object structure maintain the capability of providing services. We define the general notion of structure refinements. A structure refinement is a transformation from one graph to another that preserves the capability of providing services, that is the resulting class graph should be able to provide at least as well as the original graph. We give a small set of structure refinement rules that is proved to be sound and complete for a kind of structure refinement. Keywords: Object systems, class graphs, object graphs, labelled graphs, graph transformations, refinement