Publications

 Reports on the status of UNU-IIST and its activities after the first 6 months of operation 

 The programme and project mission of {\sf UNU/IIST}\ is reviewed, as are the policies according to which {\sf UNU/IIST}\ offers fellowships and engages in joint research projects and in advanced development projects with institutions in developing (and other) countries. We then detail all the programmatic activities that took place during 1995 --- with this review forming a major part of this report. A special emphasis is paid to Macau\--oriented actions. The ongoing relations between {\sf UNU/IIST}\ and the {\sf UN}\ System (\&c.) as such are briefly reviewed, as is the status of personnel, finances \& budget. Extensive reference is made both to internal {\sf UNU/IIST}\ documents and to {\sf UNU/IIST}\ reports and research and technical notes. Programmatic activity, staffing, budget and other plans for the 1996\--1997 Biennium are covered throughout

 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.

 The paper presents the development of a dependable messaging infrastructure for Electronic Government. Based on a few simple concepts like messages, members and channels, the infrastructure was developed to facilitate the exchange of messages by government agencies in a dependable and automated way. The dependability requirement was addressed on various levels: design, development and application. Considering design, the infrastructure comprises a small core offering plain messaging services, a repository of extensions to provide additional services, and a development framework to rigorously specify, implement and verify messaging extensions. Considering development, the infrastructure was build through rigorous use of modeling and analysis in various development stages. Considering applications, government agencies can use the infrastructure to exchange messages through carefully managed logical communication channels and the prudent use of necessary extensions, including extensions to implement required security measures. The paper presents the development and explains why the outcome satisfies the dependability requirement.

 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.

 The paper presents a formal model for a knowledge repository shared by members of a Virtual Community of Practice (VCPs), describes how the repository can be used to underpin collaborative problem solving, and how to build computer support for such processes. The repository comprises the resources used and developed by VCPs particularly through problem solving. As a case study, the paper illustrates how the problem solving process and the underlying repository can be applied in disaster prevention and handling. The repository and the process are formally described using the RAISE Specification Language

 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.