Advertisement

Timed Statecharts and Real Time Logic

  • L. Barroca
Conference paper
Part of the Dependable Computing and Fault-Tolerant Systems book series (DEPENDABLECOMP, volume 7)

Abstract

This paper deals with simple ways of proving and deducing timing constraints of real time systems. Timed Statecharts are used to specify real time reactive systems. From such specifications assertions can be proved about time constraints and new restrictions deduced. To express such constraints Real Time Logic formulas are written directly from the Timed Statecharts. A set of rules is presented to translate Timed Statecharts constraints into RTL formulas. Two examples illustrate the work presented.

Key Words

Timing constraints Timed Statecharts RTL verification of safety constraints 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    D. Harel, “Statecharts: A visual formalism for complex systems,” Science of Computer Programming, vol. 8, pp. 231–274, 1987.MathSciNetMATHCrossRefGoogle Scholar
  2. [2]
    D. Harel, “On visual formahsms,” Communications of the ACM, vol. 16, no. 4, pp. 514–530, 1988.MathSciNetCrossRefGoogle Scholar
  3. [3]
    D. Harel, H. Lachover, A. Naamad, and A. Pnueli, “Statemate: A working environment for the development of complex reactive systems,” IEEE Transactions on Software Engineering, vol. 16, no. 4, pp. 403–414, 1990.CrossRefGoogle Scholar
  4. [4]
    D. Harel, A. PnueU, J. Schmidt, and R. Sherman, “On the formal semantics of statecharts,” 2nd IEEE Symposium on Logic in Computer Science, (New York), IEEE, 1987.Google Scholar
  5. [5]
    T. Henzinger, Z. Manna, and A. Pnueli, Timed transition systems, “Proc. of the REX Workshop-Real-Time: Theory and Practice”, 1991.Google Scholar
  6. [6]
    Y. Kesten and A. Pnueli, “Timed and hybrid statecharts and their textual representation,” Formal Techniques in Real Time and Fault Tolerant Systems, LNCS 571 (J. Vytopil, ed.), pp. 591–620, Springer Verlag, 1991.Google Scholar
  7. [7]
    O. Maler, Z. Manna, and A. Pnueli, “From timed to hybrid systems,” 1992. presented at the School on Formal Techniques in Real-Time and Fault-Tolerant Systems, Nijmegen, The Netherlands.Google Scholar
  8. [8]
    O. Maler, Z. Manna, and A. Pnueli, “A formal approach to hybrid systems,” Proc. of the REX Workshop-Real-Time: Theory and Practice, 1992.Google Scholar
  9. [9]
    F. Jahanian and A. K. Mok, “Safety analysis of timing properties in real-time systems,” IEEE Transactions on Software Engineering, vol. SE-12, no. 9, pp. 890–903, 1986.Google Scholar
  10. [10]
    F. Jahanian and A. K. Mok, “A graph-theoretic approach for timing analysis and its implementation,” IEEE Transactions on Computers, vol. C-36, no. 8, pp. 961–975, 1987.CrossRefGoogle Scholar
  11. [11]
    T. Henzinger, Z. Manna, and A. Pnueli, “Temporal proof methodologies for real-time systems,” Proc. of 18th ACM Symp. Princ. of Prog. Languages, pp. 353–366, ACM, 1991.Google Scholar
  12. [12]
    F. Jahanian and D. Stuart, “A method for verifying properties of Modechart specifications,” Proc. of 9th Real Time Systems, pp. 12–21, 1988.Google Scholar
  13. [13]
    N. Leveson and J.Stolzy, “Safety analysis using Petri Nets,” IEEE Transactions on Software Engineering, vol. SE-13, no. 3, pp. 386–397, 1987.CrossRefGoogle Scholar
  14. 14]
    J. Ostroff, Temporal Logic for Real-Time Systems. Research Studies Press Ltd, 1989.Google Scholar
  15. [15]
    F. Jahanian, R. Lee, and A. K. Mok, “Semantics of Modechart in Real Time Logic,” Proc. of 21st Annual Hawai International Conference on System Science, pp. 479–489, 1988.Google Scholar
  16. [16]
    J. Ostroff, “Automated verification of timed transition models,” Automatic Verification Methods for Finite State Machines, LNCS 407(J. Sifakis, ed. ). Springer-Verlag, 1989.Google Scholar
  17. [17]
    J. Ostroff, “Verification of finite state real-time embedded computer systems,” 9th IEEE Int. Conf. on Distributed Computing Systems, pp. 207–216, IEEE, 1989.Google Scholar
  18. [18]
    D. Parnas, K. Heninger, J. Kallender, and J. Shore, “Software requirements for the A-7E aircraft,” memorandum report 3876, Naval Research Laboratories, Washington, D.C., 1978.Google Scholar
  19. [19]
    F. Maraninchi, “Argonaute: Graphical description, semantics and verification of reactive systems by using a process algebra,” Automatic Verification Methods for Finite State Machines, LNCS 407 (J. Sifakis, ed.). Springer-Verlag, 1989.Google Scholar

Copyright information

© Springer-Verlag/Wien 1993

Authors and Affiliations

  • L. Barroca
    • 1
  1. 1.DCSC/Dept. of Computer ScienceUniversity of YorkYorkUK

Personalised recommendations