Publications

 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.

 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.

 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.

 This paper presents an approach to formalizing and proving real-time properties of schedulers. The formal logic that we propose to use is the Duration Calculus, and the scheduler that we select here to serve as an example is the Deadline Driven Scheduling Algorithm. The specification and proof of the algorithm are formulated abstractly by using the Duration Calculus. The result may encourage others to formally treat more real-time aspects of operating systems which are conventionally a piece of ad hoc territory in computer science.

 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.

 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.

 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.

 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.

 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.

 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.

 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.

 This paper introduces infinite intervals into the Duration Calculus. The extended calculus defines a state duration over an infinite interval by a property which specifies the limit of the state duration over finite intervals, and excludes the description operator. Thus the calculus can be established without involvement of unpleasant calculation of infinity. With limits of state durations, one can treat conventional liveness and fairness, and can also measure out liveness and fairness by properties of limits. Including both finite and infinite intervals, the calculus can, in a simple manner, distinguish between terminate behaviour and nonterminate behaviour, and therefore directly specify and reason about sequentiality.

 Duration Calculus is a real-time interval logic which can be used to specify and reason about timing and logical constraints on discrete states in a dynamic system. It has been used to specify and verify designs for a number of real-time systems. This paper extends the Duration Calculus with notations to capture properties of piecewise continuous states. This is useful for reasoning about hybrid systems with a mixture of continuous and discrete states. The proof theory of Duration Calculus is extended such that results proven using mathematical analysis can be used freely in the logic. This provides a flexible interface to conventional control theory. {\bf Keywords:}Requirements, software design, hybrid systems, real-time systems, control theory, interval logic, durations.

 The Duration Calculi are calculi for designing real-time software embedded systems. The Calculi overviewed in the paper include the Duration Calculus, the Extended Duration Calculus, the Mean Value Calculus and the Probabilistic Duration Calculus. They are extensions of an Interval Temporal Logic, and can accommodate some concepts of mathematical analysis such as integrals, mean values, piecewise continuity and differentiability of functions over continuous time. The Calculi can be used to capture and refine real-time requirements for hybrid systems, to define real-time behaviour/semantics of computing systems, and to calculate system dependability in terms of requirement satisfaction probability.

 Distributed only with authors / publishers permission

 Inspired by [He94], a language to describe hybrid systems, i.e. networks of communicating discrete and continuous processes, is proposed. A semantics of the language is given in Extended Duration Calculus [ZRH93], a real-time interval logic with a proof system that allows reasoning in mathematical analysis about continuous processes to be embedded into the logic. The semantics thus provides a secure link to hybrid system models based on a general theory of dynamical systems.