Advertisement

Abstract

This paper is to present an algorithm to decide whether a real-time system satisfies a set of invariants which are constructed from linear inequalities of integrated durations of system states. Real-time systems in the paper are taken to be real-time automata which set up for each of state transitions a lower time bound and an upper time bound. The satisfaction problem can be translated into a family of linear programming problems. The algorithm is, according to the invariants, to reduce the infinite family of linear programming problems to an equivalent one with only finite members, and then to solve each of linear programming problems efficiently. The algorithm is so simple that no prerequisite of linear programming theory is assumed.

Keywords

Boolean Function Linear Programming Problem Regular Expression Observation Interval Transition Sequence 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    R. Alur, C. Courcoubetis, T. Henzinger, P-H Ho: Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems, in Hybrid Systems, LNCS 736, pp 209–229, R. L. Grossman, A. Nerode, A. P. Ravn and H. Rischel (eds.), Springer-Verlag, 1993Google Scholar
  2. 2.
    M. Engel, M. Kubica, J. Madey, D.J. Parnas, A.P. Ravn, A.J. van Schouwen: A Formal Approach to Computer Systems Requirements Documentation, in Hybrid Systems, LNCS 736, pp 452–474, R. L. Grossman, A. Nerode, A. P. Ravn and H. Rischel (eds.), Springer-Verlag, 1993Google Scholar
  3. 3.
    Y. Kesten, A. Pnueli, J. Sifakis, S. Yovine: Integration Graphs: A Class of Decidable Hybrid Systems, in Hybrid Systems, LNCS 736, pp 179–208, R. L. Grossman, A. Nerode, A. P. Ravn and H. Rischel (eds.), Springer-Verlag, 1993Google Scholar
  4. 4.
    S.C. Kleene: Representation of Events in Nerve Nets and Finite Automata, in Automata Studies, pp 3–41, C. Shannon and J. McCarthy (eds.), Princeton Univ. Press, Princeton, NJ, 1956Google Scholar
  5. 5.
    Z. Manna, A. Pnueli: Verifying Hybrid Systems, in Hybrid Systems, LNCS 736, pp 4–35, R. L. Grossman, A. Nerode, A. P. Ravn and H. Rischel (eds.), Springer-Verlag, 1993Google Scholar
  6. 6.
    A.P. Ravn, H. Rischel: Requirements Capture for Embedded Real-Time Systems, Proc. IMACS-MCTS'91 Symp. Modelling and Control of Technological Systems, Vol 2, pp. 147–152, Villeneuve d'Ascq, France, 1991Google Scholar
  7. 7.
    A.P. Ravn, H. Rischel, K.M. Hansen: Specifying and Verifying Requirements of Real-Time Systems, IEEE Trans. Software Eng., Vol 19, No 1, pp 41–55, January 1993Google Scholar
  8. 8.
    J.U. SkakkebÆk, A.P. Ravn, H. Rischel, Zhou Chaochen: Specification of Embedded Real-Time Systems, Proc. 4th Euromicro Workshop on Real-Time Systems, IEEE Press, pp 116–121, June 1992Google Scholar
  9. 9.
    Zhou Chaochen, C.A.R. Hoare, A.P. Ravn: A Calculus of Durations, Information Processing Letter, 40, 5, pp. 269–276, 1991Google Scholar
  10. 10.
    Zhou Chaochen, Li Xiaoshan: A Mean-Value Duration Calculus, in A Classical Mind, Essays in Honour of C. A. R. Hoare, pp 431–451, A. W. Roscoe (ed.), Prentice Hall International, 1994Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Zhou Chaochen
    • 1
  • Zhang Jingzhong
    • 2
  • Yang Lu
    • 2
  • Li Xiaoshan
    • 3
  1. 1.UNU/IISTMacau
  2. 2.CICA, Academia SinicaChengduChina
  3. 3.Software InstituteAcademia SinicaBeijingChina

Personalised recommendations