Publications

 The aim of this work is to develop a template for component-based programs which can be used in different programming languages. First, we give a model of component based systems based on the unifying theory of programming. We define the concepts interface, contract and component, and component combination. The definition can be used as the basis for the component template development. We define a contract to include method specification, and define a component as an implementation of a contract. This implementation may require services from other components with some assumptions about the schedule for resolving the conflict of shared method and resource uses with the presence of concurrency. The assumption is expressed as interaction protocols. In our model, components are correct by its design. We then give a guideline for extending the model for real-time component systems.

 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.

 In the paper, the problem of discretization of continuous time in Duration Calculus (DC) is addressed. For a DC formula $D$, for a sampling step $h$, a sampling semantics of $D$ is defined to express the properties of discrete observations of its models, while original semantics of $D$ expresses the properties of the models. In practice, only sampling semantics is implemented. So, an implementation $D$ of a system specified by $S$, both are assumed to be written in DC, is correct iff sampling semantics of $D$ implies original semantics of $S$. Some rules for proving the correctness of an implementation are given. The problem of digitization is also considered in the paper. Some forms of digitizable DC formulae are shown. Then we apply the obtained results for a non-trivial example, namely, a Biphase Mark Protocol. That protocol uses 18-cycle cell for a bit of message. A cell is formed by 5-cycle mark subcell followed by 13-cycle code subcell. We adopt the same assumptions about physical environment as in the literature. However, we are able to show stronger property: The protocol works correctly provided clock rate between writer's and reader's is within $30\%$.

 An on-line survey of former UNU-IIST fellows was made in June-August 2006. 82 former fellows answered the questions in the on-line questionnaire. This report summarises the results from the survey.

 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.

 The paper presents a model of Biphase Mark Protocols (BMP) using Duration Calculus, which seems to be more general and more intuitive than the others in the literature. With Duration Calculus we can model the behaviour of the bus in a natural way and in more detail. The model makes it possible to specify and verify BMP using PVS/DC tool. The mechanical verification not only ensures the correctness of the protocol, but also helps engineers to choose the optimal values for the parameters given the ratio between the clock rates of the sender and the receiver and the time for changing the signal from high to low and low to high.

 We give a model of component interface for real-time component based systems. We extend the specification of a method with a time constraint which is a relation between the resource availability and the amount of time spent to perform the method. We define a contract to include method specification, and define a component as an implementation of a contract. This implementation may require services from other components with some assumptions about the schedule for the use of shared methods and resources with the presence of concurrency. Our model supports the separation between functional and non-functional requirements, and the formal compositional verification of component-based real-time systems.

 The paper presents an approach to the specification and verification of real-time hybrid systems using Duration Calculus (DC). By introducing a formula {\sl int} to DC to express the intervals of time between two ticks of the system clock, it is shown that DC can be used to specify both the digital states and the analog states as well as to reason about time in distributed systems. We illustrate our approach by giving an intuitive model for the communication protocols in which the verification can be done by using the familiar natural induction rules.

 In this report, we introduce an extension of Duration Calculus called Simple Probabilistic Duration Calculus (SPDC) to express dependability requirements for real-time systems, and address the problem of verification of a SPDC formula of probabilistic timed automata. We develop a technique based on model checking to assist solving this problem for a class of SPDC.

 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

 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.

We present a linear time algorithm for improving the time efficiency for a partition of a computing system into a parallel program with synchronous communication based on the program syntax. The technique can be used for for optimizing parallel and distributed systems or in hardware/software codesign.

 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 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.

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 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.

 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.