Publications

 A hybrid system is a system containing both of time-evolving components and event-driven components. A formal approach is explored in this paper, based on Extended Duration Calculus (EDC), for the development of hybrid systems. A typical example of hybrid system from modern control theory, a two-level adaptive control system is used for illustrating our approach. Its high level consists of an event-driven supervisor which reacts to the change of plant structure, and its time-evolving low level consists of adaptive controllers and other components. Firstly performance specifications and system specification of the case are formulated in EDC; then they are refined stepwisely into specifications of the supervisor and the low level components. Our approach emphasizes the interface between the two kinds of components in the hybrid system.

 This compendium consists of the papers presented at the AWCVS'06 workshop. This compendium is the preliminary proceedings for the workshop for the convenience of the workshop participants.

 We present a method for automatically generating a prototype from a UML model of system requirements that consists of a use-case model and a conceptual class model. The method is based on a formalization of UML in which a use case is formally specified by a pair of pre and post conditions in the context of a conceptual class model. To generate a prototype, we translate the pre and post conditions of a use case into a sequence of executable atomic actions. These actions are to create or delete an object, update an object, establish or remove a link between two objects with respect to an association. Such a prototype can be used to validate requirements and check system invariants. An automated prototype generator is developed in Java, and a simple library system is used as an example to illustrate the feasibility of the method.

 This paper introduces a new method for the synthesis of gate-level asynchronous controllers. The method is based on a user-level specification formalism, the path model, and a simple algebraic tool, the signal calculus, that in combination provide a formalism for the specification and analysis of path-model designs. The path model view of communication is state-based as in other asynchronous finite-state-machine methods; however it focuses on the critical component of state machines, the paths, and ignores other non-critical free states. The signal calculus, a temporal lifting of Boolean logic, helps to formalise path-model specifications algebraically, removing much of the inadequacy of traditional tabular tools like flow tables, with their dependency on table cells that is exponential in input size. The method is demonstrated on two examples.

 A new asynchronous pipeline is presented for the self-timed design discipline of quasi-delay insensitivity with dual-rail encoding and four-phase handshaking. The function blocks of the pipeline consist of a universal gate (presented in the appendix) which is particularly simple, comprising only the conventional nand and nor gates, and is supported by an equally simple development method. The simple quadgate enables optimisation techniques for completion- detection circuitry and pipeline architecture. The pipeline is reported to compare favourably with analogous designs and is demonstrated here on a selection of 32-bit adders, simulated on 10,000 pairs of random inputs.