Publications

 Ensuring a correct test result from execution of test cases requires more than just writing of a test suite. Testing and Test Control Notation version 3 (TTCN-3) is a standardized test specification and test implementation language. Its architecture has various entities which interact by providing and/or requiring services from each other. We analyze the operations of a TTCN-3 test system and characterize the properties of these operations. We describe the interactions at a system level using sequence diagrams followed by a precise and structural specification of the operations of the TTCN-3 test systems.

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.

 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.

 This paper extends rRCOS with the notion of component coordination. A coordination of a number of components is defined as a constraint on the behaviour of the components. Such a coordination can be realised by synchronising the components with the behaviour of an active entity which we call a proces. Like a component, a process can be specified by a contract. However, a process and a component can only be composed by the CSP-like synchronisation parallel composition. In addition to coordinating the behaviour of components, a process can be used to glue a number of components to form a new component. The main theoretical result is the integration of the event-based method and the state-based method. The integration leads to the fact that components glued together by a process form a component, and the black-box specification of new component can be calculated from the behaviour of the components and the process.

 The method of refinement of component and object systems, known as rCOS, provides a notation with a formally defined relational semantics. In rCOS, the notions of interfaces, contracts, components, and component publications are formally defined. With the definitions of various compositions and refinement relations between contracts and components, the key software artifacts in all phases of a component-based model driven design process can be formally specified, analyzed and refined. This paper presents our further investigation on problems of component publications and composition of components. We will define the notion of publications of components that describes how a component can be used by a third party in building their own components or in writing their applications without the access to the design or the code of the component. It is desirable that different users of the components can be given different publications according to their need. The first contribution of this paper is to provide a procedure, which calculates a weakest contract of the required interface of a component from the contract of its provided interface and its code. The other contribution, that is more significant from a component-based designer's point of view, is to define composition on publications so that the publication of a composite component can be calculated from those of its subcomponents. For this we define a set of primitive composition operators over components, including renaming, hiding, internalizing and plugging.

 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

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.

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.

 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.

 We present a design of a triple modular fault-tolerant system that is a real case we received from our collaborators in the aerospace field. The system is used to compute the action that a subsystem should take and output the result to another subsystem. We model the system as timed automata, where a fault is modelled as an unobservable transition from a "good state" to an "error state". Based on the faults that we were given by the application engineers, we design a system to tolerate the faults and use UPPAAL to check relevant properties. Keywords: Fault-tolerance, real-time embedded systems, abstraction techniques, model checking

This book presents thoroughly revised tutorial papers based on lectures given by leading researchers at the International Training School on Domain Modeling and the Duration Calculus, held in Shanghai, China, in September 2007 as an associated event of ICTAC 2007, the 4th International Colloquium on Theoretical Aspects of Computing.The four tutorial papers presented provide competent coverage of software security, domain modeling of software engineering, and duration calculus for real time systems - originating from lectures of leading experts in these fields from Europe and Asia. Topics addressed in detail are: development of real-time systems, domain engineering using abstract modeling, the area of duration calculus, and formal methods like language description using the operational semantics approach.

Compensating CSP (cCSP) is an extension to CSP for modeling long-running transactions. It can be used to specify programs of service orchestration written in a programming language like WS-BPEL. So far, only an operational semantics and a trace semantics are given to cCSP. In this paper, we extend cCSP with more operators and define for it a stable failures semantics in order to reason about non-determinism and deadlock. We give some important algebraic laws for the new operators. These laws can be justified and understood from the stable failures semantics. A case study is given to demonstrate the extended cCSP.

Compensating CSP (cCSP) is an extension to CSP for modeling long-running transactions. It can be used to specify programs of service orchestration written in a programming language like WS-BPEL. So far, only an operational semantics and a trace semantics are given to cCSP. In this paper, we extend cCSP with more operators and define for it a stable failures semantics in order to reason about non-determinism and deadlock. We give some important algebraic laws for the new operators. These laws can be justified and understood from the stable failures semantics. A case study is given to demonstrate the extended cCSP.

 This Festschrift volume, published to honour both Dines Bjørner and Zhou Chaochen on the occasion of their 70th birthdays in October and November 2007, includes 25 refereed papers by leading researchers, current and former colleagues, who congregated at a celebratory symposium held in Macao, China, in the course of the International Colloquium on Theoretical Aspects of Computing, ICTAC 2007. The papers cover a broad spectrum of subjects, from foundational and theoretical topics to algorithms and systems issues and to applications, comprising formal methods, systems modelling, hybrid and real-time systems, specification and verification, as well as interval temporal logic.Dines Bjørner is known for his many contributions to the theory and practice of formal methods for software engineering with special focus on abstraction and modelling, specification of systems and languages, and domains, requirements, and software design. He was a professor at the Technical University of Denmark (DTU) in Lyngby, near Copenhagen; he was the founding director of the United Nations University International Institute for Software Technology (UNU-IIST) in Macao during the 1990s; and a co-founder of VDM-Europe, which became Formal Methods Europe, an organisation that promotes the use of formal methods.Zhou Chaochen is known for his seminal contributions to the theory and practice of timed and hybrid systems. Starting at Peking University and as a postgraduate at the Institute for Computing Technology of the Chinese Academy of Sciences, he continued his career with an extended visit to Oxford University Computing Laboratory, where he was the prime instigator of the Duration Calculus, an interval logic for real-time systems. He also worked as a visiting professor at the Technical University of Denmark, Lyngby, at the invitation of Prof. Dines Bjørner. He was a principal research fellow at UNU-IIST during the period 1992-97, before becoming its director, an appointment he held from 1997 to 2002.

This book constitutes the refereed proceedings of the 8th International Conference on Formal Engineering Methods, ICFEM 2006, held in Macao, China, in November 2006.The 38 revised full papers presented together with 3 keynote talks were carefully reviewed and selected from 108 submissions. The papers address all current issues in formal methods and their applications in software engineering. They are organized in topical sections on specification and verification, internetware and Web-based systems, concurrent, communicating, timing and probabilistic systems, object and component orientation, testing and model checking, tools, fault-tolerance and security, as well as specification and refinement.

 The Java programming language supports component based software development through JavaBeans. JavaBeans are Java components. The JavaBeans specification document uses a natural language and informal diagrams. It is common to interpret natural language in a number of ways which is exactly the problem in the requirement analysis phase of a software development life-cycle. As there are no separate syntactical rules and kewords for JavaBeans an application of formal techniques is required to create a rigorous specification document. This report presents a formal model of JavaBeans and refines the model towards implememtation. In our model, we use predicative logic to express JavaBeans unambigiously. The goal of the abstract formalisms is to divide a system into a number of interconnected JavaBeans. This allows developers to improve the system performance by reorganizing its constituent components. A notion of refinement has been adopted to formalize the replaceability of JavaBeans. The goal of the refinement and implementation level formalisms is to develop a mathematical characterization of JavaBeans that is close to Java features which can be used to specify, refine and implement JavaBeans. The case study shows a typical course that can be taken from the abstract model to implementation oriented formalisms.