Publications

 A major current challenge in the area of complex multi-agent systems id the conceptual approach to, and practical treatment of, emergent behaviour. This paper indicates how Formal Methods may be applied to engineer multi-agent adaptive systems exhibiting emergence, by consideration of an 'emergence predicate' in the specification and incremental derivation of interacting components that achieve that predicate. To perform that task, 'policies' are introduced as a novel technique for constraining agents in a hierarchical manner so that the multi-agent implementation as a whole exhibits the specified emergence. The ideas are demonstrated on models of the foraging behaviour of an ant colony, and used to analyse various designs appearing in the literature.

 The complex systems lying at the heart of ensemble engineering exhibit-and are perhaps even characterised by-emergent behaviour: behaviour that is not explicitly derived from the func- tional description of the components of the ensemble at the level of abstraction at which they are provided. A typical example from Artificial Life comprises an ensemble consisting of a flock of birds; the components are the individual birds, thought of autonomously, and the emergent behaviour is that of the flock. Emergent behaviour can be understood by expanding the level of abstraction of description of the components to augment their functional behaviour; but that is infeasible in specifying ensembles of realistic size (although it is the main implementation method) since it amounts to consideration of an entire implementation. An alternative must be taken. It is proposed that to specify an ensemble, the functional behaviour of its components instead be augmented by a system-wide predicate (or conjunction of 'policies', which may be seen as kinds of weak 'ethical principles', when the components are agents) pertaining to the collec- tive behaviour of its components and accounting for emergence. An implementation, however, ranges in distribution from being centralised to being fully distributed, depending on the degree to which the emergent behaviour is incorporated in the components. So the next step in this work consists of identifying implementation designs. A further step consists of establishing cri- teria for the conformance of an implementation against a specification, and the final step applies those ideas to case studies using model checking. Important application of these ideas lies in ensembles whose dynamics is controlled by artificial agents, for which a satisfactory theory of ethical behaviour can be given that is not based on free will, and takes the form of policies. The tension between emergence and reductionism, that is felt in moving from a specification to an implementation, is resolved by making explicit the level of abstraction of a description.

 A Mean Value Calculus based formal method is provided in this report to specify and verify the steam-boiler control problem raised by J.-R. Abrial[1] for Dagstuhl seminar. In addition to specifying safety property, emphasis is put on capturing non-functional requirements such as performance and optimization. Some formal design techniques about finding an optimal implementation conforming to the system specification are also discussed.

 This report presents a general method to cope with hybrid control system specification and verification by making full use of both the simplicity of finite automata and the excessive expressing power of Mean Value Duration Calculus. The method consists of four steps: First, specify the requirements of the whole system through Mean Value Duration Calculus formulas. Second, use two real-time communicating automata to characterize the design decisions, which describe the plant and control subsystems respectively. Third, translate the automata into Mean Value Duration Calculus formulas. Finally prove the design decisions conforming to the requirements specification. Taking the steam-boiler problem raised by J.-R. Abrial[1] as a running example, we demonstrate the above method in three versions of abstractions. Each version represents an abstract level for capturing the original problem requirements and provides a complete procedure of applying the above method. In addition to specifying safety property, emphasis is put on capturing non-functional requirements such as performance, reliability, and optimization. Some formal design techniques about finding an optimal implementation conforming to the system specification are also discussed.

 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 4th International Colloquium on Theoretical Aspects of Computing, ICTAC 2007 held in Macau, China in September 2007.The 29 revised full papers presented together with 3 invited talks and summaries of 2 tutorials were carefully reviewed and selected from 69 submissions. The aim of the colloquium is to bring together practitioners and researchers from academia, industry and government to present research results, and exchange experience, ideas, and solutions for their problems in theoretical aspects of computing such as automata theory and formal languages, principles and semantics of programming languages, software architectures and their description languages, software specification, refinement, and verification, model checking and theorem proving, real-time, embedded and hybrid systems, theory of parallel, distributed, and internet-based (grid) computing, simulation and modeling, and service-oriented development.

 This paper presents a predicative semantic model for integrating models from UML class diagrams and sequence diagrams. The integrated model is used for dealing with consistency problems of UML class diagrams and sequence diagrams. We also define the notion of consistent refinement of these integrated models.

 In this work, we study about formal design and verification of protocols using CSP(Communicating Sequential Processes) formalism. The protocols concern multicast communications; we develop formal models of multicast communication protocols with CSP and then verify the models using FDR which is the model checking tool of CSP.

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.

 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.

 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 component calculus, whereby a system can be divided into a number of interconnected components. We model the behaviour of individual service by a design, which enables one to separate the responsibility of clients from the commitment made by the system. We adopt the notion of refinement to formalise the replaceability of components. This allows developers to improve the system performance by reorganising its data components.

 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

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.

 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.

 In this paper, we present a rigorous design of a Fault Diagnosis and Isolation (FDI) algorithm. The system is modelled as a hybrid system with a network of parallel components. The requirement is specified in Duration Calculus. We use traditional program logic, suitably extended, to verify the discrete component and subsequently derive a number of properties of the system. Finally, the requirement is shown to be satisfied by proving that it can be deduced from the system properties.

 The major problem of checking a parallel composition of real-time systems for a real-time property is the combinatorial explosion of state spaces. To avoid this problem, one can use bisimulation equivalence w.r.t. the property to be checked to minimise the system state space. In this paper, we define such equivalence for the integrated linear duration properties of real-time automata network with shared variables. Based on this technique we develop an algorithm for checking a real-time automata network with shared variables w.r.t. a linear duration property. Using Fischer Protocol as a case study, we show that our algorithm can avoid exhaustive state space exploration significantly in some cases in comparison to some other tool in the literature.

 In this paper we formulate the design of digital dynamic systems using a programming notation, called Hybrid CSP. A continuous specification of such a system under some performance requirements is decomposed and digitized using Hybrid CSP, whose correctness is guaranteed by the control principles such as Shannon's Sampling Theorem. Therefore, a digital dynamic system can be specified and refined in a framework of formal development approach.