Publications

 The research on hybrid control systems attracts many scientists both in computer science and control theories and applications. The study should be carried out on a general framework abstracted from various hybrid control systems. This paper analyses the drawbacks of the present frameworks used by most researchers and proposes a new framework to overcome these shortcomes. The new framework consists of a discrete time box, a discrete event box and a digital-symbol interface. The new framework shows the crucial nature of the hybridity of time envolving variables and event driven variables in hybrid control systems. The new framework is easy to integrate the knowledges of computer science and control theories and applications. Two examples, a gas burner and an inverse pendulum are given to show the fitness of the new framework. The design and analysis aspects of hybrid control systems related to the new framework are also discussed.

 In the paper, the problem of determining the global properties of distributed systems is addressed. At each moment during the execution of a system, every process has its knowledge about the system. By message passing the processes can exchange their knowledge. We present a general algorithm for a process to synthesize the knowledge that it obtains, and to maintain its consistent view about the system. Depending on different interpretations the algorithm can be used for distributed snapshots, for verification and design of stabilizing protocols, etc.

 Fault-based testing is a technique where testers anticipate errors in a system under test in order to assess or generate test cases. The idea is to have enough test cases capable of detecting these anticipated errors. This work presents a method of fault-based test case generation for pre- and postcondition specifications. Here, errors are anticipated on the specification level by mutating the pre- and postconditions. We present the underlying theory by giving test cases a formal semantics and translate this general testing theory to a constraint satisfaction problem. A prototype test case generator serves to demonstrate the automatization of the method. It works on OCL specifications.

 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, we consider the problem of checking hybrid systems modelled by hybrid automata for a class of duration properties called linear duration invariants, which are constructed from linear inequalities of integrated durations of system states. Based on linear programming, an algorithm is developed for checking a class of hybrid automata for linear duration invariants.

 In this paper, we consider the problem of checking hybrid systems modelled by hybrid automata for a class of duration properties called linear duration invariants, which are constructed from linear inequalities of integrated durations of system states. Based on linear programming, an algorithm is developed for checking a class of hybrid automata for linear duration invariants

 In this paper, the problem of verifying a timed automaton for a Duration Calculus formula in the form of linear duration invariants is addressed. We show that by linear programming, a particular class of timed automata including the class of real-time automata as a proper subset, can be checked for linear duration invariants. The so-called real-time regular expressions is introduced to express the real-time behaviour of the timed automata in this class. Using real-time regular expressions, an algorithm based on linear programming is presented for checking an automaton in the class with respect to a linear duration invariant.

 The super-dense computation model provides an abstraction of real-time behaviour of computing systems. Logics to deal with this model are being studied. In the paper, we propose a combination of a linear temporal logic and an interval logic, and demonstrate how this combination can be used to specify a real-time semantics of an OCCAM-like programming language and its real-time properties, where the super-dense computation model is adopted.

 This paper is a study of the formal semantics of an extended and a virtual enterprise and how it is possible to represent their behaviour by the composition of models of individual enterprises. We consider core activities of an enterprise for manufacturing discrete parts products, modelled in terms of resources, processes and business goals (customer and purchase orders). The extended enterprise allows enterprises to interact, by matching customer and purchase orders. The virtual enterprise allows them to cooperate, by processes which execution cross organisational boundaries. The result is a precise technical meaning for an extended and a virtual enterprise, suitable for symbolic execution, reasoning and foremost, for understanding the difference between both concepts.

 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.

 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.

 An introductory course on Software Engineering using Formal Methods. The course includes an example (Credit Card) of an RSL specification, as well as some teaching materials.

 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.

 The RAISE Specification Language has no ``real time'' features. So, it is difficult to use it to specify real time applications. Now, we consider adding time to RSL. Our first attempt following Anne Haxthausen's proposal of encoding DC in RSL, we set up a proof assistant called DC/RJ. It is constructed from encoding of both DC semantics and proof system of Interval Logic and DC, and uses the RAISE Justification tool to do the verification for DC. In this paper, the author first introduces how DC can be integrated with RSL in detail. Then the construction and hierarchy of DC/RJ are explained. The Gas Burner example is used to show how DC/RJ works. A comparison among DC proof assistant systems, the problems and perspectives of our system are discussed at the end.

 We investigate formal derivation of control programs via the case study of a heating system. The requirements are specified using Duration Calculus, a real time interval logic, and the plant is represented as communicating phase transition systems. Afterwards, Duration Calculus and traditional program logic are applied to derive the control algorithm.

 Most results obtained in the research of hybrid control systems are related to the description and analysis of hybrid control systems. But it is doubtless that how to design a hybrid control system is of great significance in the research of hybrid control systems. This paper is devoted to discuss the design methodology of hybrid control systems. After an introduction of a new framework of hybrid control systems, a top-down design approach is proposed which is consistent to the framework. The approach consists of decomposition of system performance specifications, the design of discrete event driven decision maker and the design of digital control loops. Two examples, a gas burner and an inverse pendulum are systematically designed to show the goodness of the top-down design approach. Finally, a bottom-up analysis approach which is consistent to the new framework is proposed and then applied to these examples.