Publications

Models of software components at different levels of abstraction, component interfaces, contracts, implementations and publications are important for component-based design. Refinement relations among models at the same level and between different levels are essential for model-driven development of components. Classical refinement theories mainly focus on verification and put little attention on design. Therefore, most of them are not suitable for component-based model-driven development (CB-MDD). To address this issue, in this paper, we propose two refinement relations for CB-MDD, that is a trace-based refinement and a state-based refinement. The former comprises a trace refinement between contracts and components and an alternating trace refinement between publications; while the latter comprises a data refinement between contracts and components, and an alternating data refinement between publications. Both of the two refinement relations are discussed in the framework of rCOS, which is a formal model of component and object systems. These refinement relations provide different granularity of abstraction and can capture the intuition that a refined component provides "more" and "better" services to the environment. We also show how to extend these refinement relations to allow us to compare contracts, components and publications with different interfaces by exploiting the primitive operator internalizing over contracts, components and publications.

Simpson’s four-slot algorithm has been an instructive example in studying various assertional proof methods/logics geared towards shared variable concurrency. Previously, techniques like rely-guarantee, data refinement and resource separation have been applied to simplify the construction of its correctness proof. Still, an elegant, concise and insightful proof is elusive. Recently with the new generation of logics coming of age which are, for the first time, equipped with ownership transfer, it becomes imperative to ask to what extent can ownership transfer facilitate a nice proof of the algorithm. Ownership transfer is especially promising here because the conflict resolution mechanism in the four-slot algorithm can be easily recast as an implementation based on ownership transfer.

 The paper presents a compositional proof outline of Simpson four-slot algorithm using RGSep logic, a combination of rely/guarantee method with separation logic. In the proof, we illustrate the importance of the ownership transfer facility provided by RGSep to achieve non-interferent accesses on data slots by the reader and writer.

 Asynchronous circuits have received much attention recently due to their potential for energy savings. Process algebras have been extensively used in the modelling, analysis and synthesis of asynchronous circuits. This paper develops a theoretical basis for using process algebra and associated model checking tools to verify asynchronous circuits. We formulate a model that extends existing verification theory for asynchronous circuits, and integrate it into the framework of standard process algebra theory. Our theory permits analysis of safeness (i.e. choke) and progress (i.e. illegal stop, divergence and relative starvation) conditions. We show how the model can be translated into CSP, and how the satisfaction of safeness and progress requirements can be reduced to refinement checks in CSP. Finally, the correspondence of our theory with trace theory (i.e. prefix-closed trace structures), receptive process theory and the XDI model is investigated.

 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.

 Optimization is a classical notion in control theory. It is often required in engineering practice. As a case study, this paper represents an initial contribution to the formalization of the concept of optimization of hybrid systems and also explores its analytic and synthetic techniques. The illustrative case is a fluid double-tank example , and the logical notation employed in the formalization is the Duration Calculus. {\bf Keywords:} Optimization, hybrid system, duration calculus, formal specification, formal refinement.

 In this paper, a hybrid system design method, based on cooperation between two disciplines -- control theory and computing science, is presented. The method suggests to decompose a hybrid system into control loops and decision loops. The external behaviour of control loops are specified in a notation, which is understandable by the two disciplines, while designs of control loops employ theory of differential equations. The correctness of the designs of control loops is guaranteed by control engineers analytically or experimentally. Decision loops are designed by computing engineers, and, based on the specifications of control loops, the verification of system requirements can be done by a reasoning mechanism of the notation. Two examples of the problem of inverted pendulum are given for illustration, and the Mean Value Calculus is chosen as the formal notation for specifying control loops and designing decision loops.

The television landscape is in a state of flux. In this new environment, profit-driven media companies have to balance tradeoffs between traditional and new channels of video distribution to optimize returns on their investments in content generation. This chapter describes the challenges traditional television service providers face in adapting their strategies to an environment in which the internet is playing an increasingly prominent role as a new distribution channel. In the short to intermediate run there is the challenge of finding ways to monetize an internet audience without cannibalizing profits earned through traditional distribution channels. The longer-term challenge is adapting to a distribution technology that embeds a fundamentally different economic logic for video market organization. In this chapter, we describe and analyze current trends in the internet television market and traditional television industry players’ efforts to respond to the opportunities and threats posed by internet distribution.

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.