DeTfoRS: Design Techniques for Real-Time Hybrid Systems

References

 [1]

Suman Roy and Zhou Chaochen. Notes on Neighborhood Logic. Research Report 97, UNU/IIST, P.O.Box 3058, Macau, February 1997.
Abstract: In 1996, Zhou Chaochen and Michael Hansen proposed a first order interval logic called Neighbourhood Logic (NL) in view of specifying liveness and fairness of computing systems and also defining notions of real analysis in terms of expanding modalities introduced therein. This paper serves as a reference manual of NL. It contains proofs of various theorems of NL (including a proof of an NL deduction theorem), and also a sound and relatively complete Duration Calculus as an extension of NL.
postscript

 [2]

Rana Barua and Zhou Chaochen. Neighbourhood Logics : NL and NL². Research Report 120, UNU/IIST, P.O.Box 3058, Macau, August 1997. Presented at ComBaS Group, Technical University of Denmark, Copenhagen, Denmark, 4-7 September, 1997.
Abstract: In 1996, Zhou Chaochen and Michael Hansen proposed a first order interval logic called Neighbourhood Logic (NL) which can specify liveness and fairness of computing systems and also define notions of real analysis in terms of expanding modalities introduced therein. Here, we first show that NL forms a sound and complete system. Next, we extend NL by introducing two more expanding modalities in the upward and downward directions and propose a Two Dimensional Neighbourhood Logic (NL²), which can be used to specify super-dense computation. Finally, we also prove completeness of this new NL² .
postscript

 [3]

Qiu Zongyan and Zhou Chaochen. A Combination of Interval Logic and Linear Temporal Logic. Technical Report 123, UNU/IIST, P.O.Box 3058, Macau, September 1997. Presented at ComBaS Group, Technical University of Denmark, Copenhagen, Denmark, 4-7 September, 1997. Presented at and published in the proceedings of IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods (PROCOMET'98), 8-12 June 1998, Shelter Island, New York, USA, David Gries and Willem-Paul de Roever (eds), Chapman & Hall, 1998, pp. 444-461.
Abstract: 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.
postscript

 [4]

Arun K Pujari. Neighbourhood Logic & Interval Algebra. Technical Report 116, UNU/IIST, P.O.Box 3058, Macau, July 1997.
Abstract: A complete first order logic called Neighbourhood Logic to model hybrid systems is first proposed by Zhou and Hansen. Two neighbourhood modalities are introduced and it is shown that the logic is complete, adequate and suitable for modelling hybrid-systems. In AI literature, reasoning and representing indefinite temporal information of qualitative nature have been elaborately studied and this study originates from Allen's proposal of Interval Algebra. Since the satisfiability problem for Interval Algebra is established to be NP-complete, the main research has been to determine maximal tractable sub-algebras of Allen' algebra. It is observed that the Neighbourhood Logic provides an elegant interpretation of the results related to the tractability of Interval Algebra and the algorithmic study of the Interval Algebra provides some foundational insight to decidability class of Neighbourhood Logic. The present study is concerned with these two aspects of the Neighbourhood Logic formalism for Interval Algebra.
postscript

 [5]

Paritosh K. Pandya and Dang Van Hung. Duration Calculus with Weakly Monotonic Time. Technical Report 122, UNU/IIST, P.O.Box 3058, Macau, September 1997. Presented at and published in the proceedings of Formal Techniques in Real-Time and Fault-Tolerant Systems 5th International Symposium, Lyngby, Denmark, September 1998 (FTRTFT'98), LNCS 1486, pp. 55-64, Springer-Verlag, 1998.
Abstract: We extend Duration Calculus to a logic which allows description of Discrete Processes where several steps of computation can occur at the same time point. Moreover, the order of occurrence of these steps is relevant. The resulting logic is called Duration Calculus of Weakly Monotonic Time (WDC). It allows effects such as true synchrony and digitisation to be modelled. As an example, We formulate a new semantics of Timed CSP assuming that the communication and computation take no time. We also outline a semantics of shared variable concurrency under similar assumptions. We introduce a notion of deformation of time in (WDC). We study the duration calculus properties which remain invariant under such deformation of time.
postscript

 [6]

P.K. Pandya, Wang Hanpin, and Xu Qiwen. Towards a Theory of Sequential Hybrid Programs. Technical Report 125, UNU/IIST, P.O.Box 3058, Macau, October 1997. Presented at and published in the proceedings of IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods (PROCOMET'98), 8-12 June 1998, Shelter Island, New York, USA, David Gries and Willem-Paul de Roever (eds), Chapman & Hall, 1998, pp. 366-384.
Abstract: A theory of Sequential Hybrid Programs (SHP) is studied. These programs consist of phase statements and the normal sequential programming constructs such as assignments, conditionals and iterations. Phase statements are specifications representing some time-dependent dynamical activity. Intermixing of these two features leads to programs with a rich diversity of behaviours including super-dense time, infinite executions, finitely divergent executions and even instantaneously divergent executions. Duration calculus is extended with super-dense time, fixed point operators and infinite intervals to give a logic USDCI. A compositional semantics of SHP programs is defined using the logic USDCI. Several high-level proof rules are derived for establishing specific kinds of properties of SHP programs such as total correctness and invariants. These high-level proof rules provide a modular and syntax directed method for establishing the properties SHP programs where the program structure guides the proof of correctness.
postscript

 [7]

Fu Hongguang, Yang Lu, and Zhou Chaochen. A Computer-Aided Geometric Approach to Inverse Kinematics. Research Report 101, UNU/IIST, P.O.Box 3058, Macau, April 1997. Published in Journal of Robotic Systems, Vol.15, No.3, pp. 131-143, March 1998.
Abstract: 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.
postscript

 [8]

Dang Van Hung. Modelling and Verification of Biphase Mark Protocols in Duration Calculus Using PVS/DC^-. Research Report 103, UNU/IIST, P.O.Box 3058, Macau, April 1997. Presented at and published in the Proceedings of the 1998 International Conference on Application of Concurrency to System Design (CSD'98), 23-26 March 1998, Aizu-wakamatsu, Fukushima, Japan, IEEE Computer Society Press, 1998, pp. 88 - 98.
Abstract: 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.
postscript

 [9]

Manoranjan Satpathy, Dang Van Hung, and Paritosh K. Pandya. Some Results on The Decidability of Duration Calculus under Synchronous Interpretation. Research Report 86, UNU/IIST, P.O.Box 3058, Macau, December 1996. Presented at the 5th Vietnamese Conference of Mathematics, Hanoi, 17-20 Sep, 1997, presented at and published in the proceedings of Formal Techniques in Real-Time and Fault-Tolerant Systems 5th International Symposium, Lyngby, Denmark, September 1998 (FTRTFT'98), LNCS 1486, pp. 186-197, Springer-Verlag, 1998.
Abstract: Duration Calculus (or DC in short) presents a formal notation to specify properties of real-time systems and a calculus to formally prove such properties. Decidability is the underlying foundation to automated reasoning. But, excepting some of its simple fragments, DC has been shown to be undecidable.

DC takes the set of real numbers to represent time. The main reason of undecidability comes from the assumption that, in a real-time system, state changes can occur at any time point. But an implementation of a specification is ultimately executed on a computer, and there states change according to a system clock. Under such an assumption, it has been shown that the decidability results can be extended to cover relatively richer subsets of DC. In this report, we extend such decidability results to still richer subsets of DC.

Under the assumption that states change at real-numbered points, it has been shown that a propositional fragment of DC is undecidable. We also show that the same set still remains undecidable, even if we restrict that states change at points as designated by rational numbers.
postscript

 [10]

Li Xuan Dong, Dang Van Hung, and Zheng Tao. Checking Hybrid Automata for Linear Duration Invariants. Research Report 109, UNU/IIST, P.O.Box 3058, Macau, June 1997. Published in R.K.Shamasundar, K.Ueda (Eds.), Advances in Computing Science, Lecture Notes in Computer Science 1345, Springer-Verlag, pp. 166-180.
Abstract: 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.
postscript

 [11]

Pham Hong Thai and Dang Van Hung. Checking a Regular Class of Duration Calculus Models for Linear Duration Invariants. Technical Report 118, UNU/IIST, P.O.Box 3058, Macau, July 1997. Presented at and published in the Proceedings of the International Symposium on Software Engineering for Parallel and Distributed Systems (PDSE'98), 20 - 21 April 1998, Kyoto, Japan, Bernd Kramer, Naoshi Uchihira, Peter Croll and Stefano Russo (Eds), IEEE Computer Society Press, 1998, pp. 61 - 71.
Abstract: In this paper we define timed extended regular expressions to describe the timed behaviour of parallel real-time systems and consider the problem of checking algorithmically the set of timed behaviours defined by extended timed regular expressions for a real-time requirement specified by a linear duration invariant. In general, the problem can be solved by using the mixed integer linear programming techniques. We show that in many cases, the problem can be reduced to a finite number of linear programming problems.
postscript

 [12]

Xu Qiwen and Mohalik Swarup. Compositional Reasoning Using Assumption - Commitment Paradigm. Technical Report 136, UNU/IIST, P.O.Box 3058, Macau, February 1998. Published in International Symposium, Compositionality - The Significant Difference, Hans Langmaack and Amir Pnueli and Willem-Paul de Roever (eds), LNCS 1536, pp. 565-583, Springer-Verlag, 1998.
Abstract: Assumption-Commitment paradigms have been investigated to derive tractable rules for composing specifications of concurrent systems. We first give a short survey of several typical composition rules, and then we adopt the principle to reason about real time systems. An extension of Duration Calculus capable of describing infinite behaviours and instantaneous actions is proposed. In the calculus, verification techniques based on assumption-commitment are incorporated.
postscript

 [13]

Gao Jianping and Xu Qiwen. Rigorous Design of a Fault Diagnosis and Isolation Algorithm. Technical Report 128, UNU/IIST, P.O.Box 3058, Macau, December 1997. Presented at and selected for publishing in the proceedings of the Fifth International Workshop on Hybrid Systems, Indiana, USA, 11-13 September, 1997.
Abstract: In this paper, we present a rigorous design of a Fault Diagnosis and Isolation (FDI) algorithm. The system is modelled as a hybrid system with a network of parallel components. The requirement is specified in Duration Calculus. We use traditional program logic, suitably extended, to verify the discrete component and subsequently derive a number of properties of the system. Finally, the requirement is shown to be satisfied by proving that it can be deduced from the system properties.
postscript

DeTfoRS: Design Techniques for Real-Time Hybrid Systems