Publications

 The overarching goal of a formal specification of design patterns is to enhance their understandability, address their composability problem and provide a tool support for their reusability. Understanding design patterns means uncovering when and how a specific pattern can be used to resolve a specific design problem. The lack of completeness of the existing formal specifications motivates this work. In this paper we start introducing a calculus for design patterns based on rCOS (Refinement Calculus of Object and Component Systems) specification which provides a formalization of patterns addresses the pattern composition mechanism and describes a mechanism for design refinement to patterns designs. In this first step we are focusing on the proposition of a formalization model. Thus, a model for patterns formalization is proposed and an assessment model is used for the evaluation of the proposed model and comparing it with the existing ones to show its efficiencies and limitations.

In prime event structures with binary conflicts a branching cell is a subset of events closed under downward causality and immediate conflict relations. This means that no event inside the branching cell can be in conflict with any outside event, and no outside event can enable any inside event. It bears a strong resemblance to stubborn sets - a method used for partial order reduction of transition systems, which says that if a subset T of actions (i.e. labels) is a stubborn set at state s, then, from s on (for any state reachable by a sequence of outside transitions), no inside transition can be in conflict with any outside transition and no outside transition can enable any inside one. 

A rigorous study of the relationship between the two ideas, however, is not straightforward due to the facts that 1) stubborn sets utilise sophisticated causality and conflict relations that are beyond the expressiveness of prime event structures and binary conflicts, and 2) it is challenging how to devise a technique to identify the `right' subsets of transitions as `events' such that the derived event-based system captures exactly the causality and conflict information needed by stubborn sets.

In this paper we give a solution to the problems by providing an unfolding of labelled transition systems into configuration structures, a more general structure supporting or-causality and finite conflict, and show that each branching cell in the unfolding is actually a `long-lived stubborn set', i.e. no matter how the system evolves, the (`residue' of) branching cell is always a stubborn set.

 The work presented here concerns domain description, domain model and requirements capture for an accounting system for the UNU financial administration. A novel aspect of this work is the development of a formal model for accounting concepts and the use of this model as a reference when defining requirements.

 Real-time and hybrid systems have been studied so far under the assumption of finite variability. In this paper, we consider models in which systems exhibiting finite divergence can also be analysed. In such systems the state of the system can change infinitely often in a finite time. This kind of behaviour arises in many notations of hybrid systems, and also in theories of non-linear systems. The aim, here, is to provide a theory where pathological behaviour such as finite divergence can be analysed -- if only to prove that it does not occur in systems of interes. Finite divergence is studied using the framework of Duration Calculus. Axioms and proof rules are given. Patterns of occurrence of divergence are classified into dense divergence, accumulative divergence and discrete divergence by appropriate axioms. Induction rules are given for reasoning about discrete divergence.

The effectiveness of partial order reduction depends on the accuracy of independence and causality relations between transitions of a system. Given a concurrent system that uses synchronous communication, some of the dependency information is of local nature, whereas the rest of the information is non-local and dynamic. Accurate analysis of dependencies in a fully global manner would require traversing an unbounded number of steps into the state graph, and would thus be self-defeating for partial order reduction.

In this paper we explore the approach of using compositionality to cut the cost in analysing non-local dependency information. Non-local dependency analysis is performed only on individual components of the system, which are assumed to be relatively small transition systems. The system-level non-local dependency information of the product system is calculated directly from such information on the components.

Our work is carried out in the framework of the stubborn set method, applied to labelled transition systems. We develop the theory of stubborn sets for constructing a system using synchronisation patterns and compositional dependency relations. We show that the compositional techniques do give extra reduction on top of the more traditional approach, and in some cases this reduction is dramatic.

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.

An intelligent reactive planning agent for partially ob­ servable stochastic domains requires a number of di­ verse capabilities. First, the agent must be able to intelligently allocate its resources. This means that it must be able to decide how much time to allocate to deliberation in a way that is responsive to the environ­ ment in which the agent finds itself. It must also be able to decide when to sense and how much time and effort to spend sensing.

 This paper is a sequel of [FYZ95]. It presents a geometric approach to solving the inverse kinematics for all 3-joint placeable robotic manipulators. The distinct feature of this approach is that it uses geometric variables such as length, area ratio and Pythagoras difference to find the closed form solutions. It is proved in the paper that for any 3-joint placeable manipulator there exists a geometric variable which keeps constant during the evolution of the manipulator. With this invariant a characteristic equation of the manipulator can be derived and can be transformed into a polynomial equation with degree four. Therefore the closed form solution of the 3-joint placeable manipulator can be obtained. A characteristic equation of the 3-revolute-joint manipulator produced by this approach with assistance of Maple is listed in the Appendix of the paper. The possible application of this geometric approach for 6-joint manipulator is also discussed in the paper.

 This paper is a sequel of [FYZ95]. It presents a geometric approach to solving the inverse kinematics for all 3-joint placeable robotic manipulators. The distinct feature of this approach is that it uses geometric variables such as length, area ratio and Pythagoras difference to find the closed form solutions. It is proved in the paper that for any 3-joint placeable manipulator there exists a geometric variable which keeps constant during the evolution of the manipulator. With this invariant a characteristic equation of the manipulator can be derived and can be transformed into a polynomial equation with degree four. Therefore the closed form solution of the 3-joint placeable manipulator can be obtained. A characteristic equation of the 3-revolute-joint manipulator produced by this approach with assistance of Maple is listed in the Appendix of the paper. The possible application of this geometric approach for 6-joint manipulator is also discussed in the paper.

 This paper presents a geometric method to solve the inverse kinematics for a class of 3-joint placeable robotic manipulators. A distinct feature of the method is that a mechanical geometric reasoning process is used for replacing conventional algebraic calculations. The conventional algebraic method solves the problem by finding analytic solutions of arm equations of robotic manipulators. Arm equations are usually polynomial equations, algebraic calculations in finding the solutions are always very complicated, and even fail for some cases of 3-joint non-loose placeable manipulators [P91]. The geometric method presented in this paper specifies manipulators in terms of vectors, instead of arm equations, and employ reasonings about geometric variables such as volume, area, length and Pythagoras difference, instead of algebraic calculations. It can decide whether a 3-joint placeable manipulator is loose, and can mechanically find out analytic solutions of the inverse kinematics for any non-loose one. The method is therefore simple and understandable.

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.

 This paper presents a denotational semantics for the hardware description language Verilog using Duration Calculus. The language contains interesting features such as event-driven process, shared-variable concurrency and simulator -based description. We examine algebraic properties of Verilog, which can be used in support of program simplification and optimization. To covert programs to normal form, we enrich the language with guarded choice and compound guard.

 In this report we propose a simple model for component based real-time systems using duration automata. A component based real-time system consists of a host which is a general duration automaton and several components which are duration automata with some restrictions. Components can communicate with the host only. For this model we propose an algorithm for solving the emptiness problem using black box testing for components and with a complexity in the same complexity class as for solving the emptiness problem for untimed component based systems. Furthermore, the verification of behavioural real-time properties in this model can be done with techniques from Duration Calculus.

 This paper addresses the problem of modeling railway systems. We use both Mean Value Calculus and Extended Duration Calculus to specify railway systems. For railway line, signal system is discussed and a simple scheduling strategy is presented, which result in safety and liveness of railway line; For linear railway region, both running map and feasibility conditions are described. The framework to verify correctness of scheduling, i.e. the running map satisfies feasibility conditions, is also presented.

 This paper deals with dependability of imperfect implementations concerning given requirements. The requirements are assumed to be written as formulas in Duration Calculus. Implementations are modeled by continuous semi-Markov processes with finite state space, which are expressed in the paper as finite automata with stochastic delays of state transitions. A probabilistic model for Duration Calculus formulas is introduced, so that the satisfaction probabilities of Duration Calculus formulas with respect to semi-Markov processes can be defined, reasoned about and calculated through a set of axioms and rules of the model.

 The present paper gives a systematic way to refine specifications of hybrid control systems written in DC (Duration Calculus) into their automata models. The iteration DC formulas are introduced together with rules for transforming, refining DC formulas into the forms that describe the systems in more details. Then, the plant automata derived from DC formulas are defined, which allow the designers to derive a specification of control automata more easily. A necessary and sufficient condition for a plant automaton and a requirement to have a control automaton is given. Some simple examples are presented to illustrate the method