Advertisement

Constructing Test Automata from Graphical Real-Time Requirements

  • Henning Dierks
  • Marc Lettrari
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2469)

Abstract

A semantics for a graphical specification language of real-time properties (Constraint Diagrams) is presented. The new semantics is given in terms of Timed Automata. A model in terms of Timed Automata satisfies the property given by a Constraint Diagram if the model in parallel composition with the semantics of the Constraint Diagram can reach a certain state. This kind of question can be checked by all model-checkers for Timed Automata. A prototype of a tool is presented that automatically translates an appropriate Constraint Diagram into the input language of the tool Uppaal.

Keywords

Temporal Logic Atomic Proposition Computation Tree Logic Time Automaton State Assertion 
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.

References

  1. ABL98.
    L. Aceto, A. Burgueño, and K. Larsen. Model Checking via Reachability Testing for Timed Automata. In Steffen [Ste98], pages 263–280.CrossRefGoogle Scholar
  2. ACD90.
    R. Alur, C. Courcoubetis, and D. Dill. Model-Checking for Real-Time Systems. In Fifth Annual IEEE Symp. on Logic in Computer Science, pages 414–425. IEEE Press, 1990.Google Scholar
  3. AD90.
    R. Alur and D.L. Dill. Automata for modeling real-time systems. In M.S. Paterson, editor, ICALP 90: Automata, Languages, and Programming, volume 443 of LNCS, pages 322–335. Springer, 1990.CrossRefGoogle Scholar
  4. AD94.
    R. Alur and D.L. Dill. A theory of timed automata. TCS, 126:183–235, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  5. DD97.
    H. Dierks and C. Dietz. Graphical Specification and Reasoning: Case Study “Generalized Railroad Crossing”. In J. Fitzgerald, C.B. Jones, and P. Lucas, editors, FME’97, volume 1313 of LNCS, pages 20–39, Graz, Austria, September 1997. Springer.Google Scholar
  6. DFMV98a.
    H. Dierks, A. Fehnker, A. Mader, and F.W. Vaandrager. Operational and Logical Semantics for Polling Real-Time Systems. In A.P. Ravn and H. Rischel, editors, FTRTFT’98, volume 1486 of LNCS, pages 29–40, Lyngby, Denmark, September 1998. Springer. short version of [DFMV98b].Google Scholar
  7. DFMV98b.
    H. Dierks, A. Fehnker, A. Mader, and F.W. Vaandrager. Operational and Logical Semantics for Polling Real-Time Systems. Technical Report CSIR9813, Computer Science Institute Nijmegen, Faculty of Mathematics and Informatics, Catholic University of Nijmegen, April 1998. full paper of [DFMV98a].Google Scholar
  8. Die96.
    C. Dietz. Graphical Formalization of Real-Time Requirements. In B. Jonsson and J. Parrow, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1135 of LNCS, pages 366–385, Uppsala, Sweden, September 1996. Springer.Google Scholar
  9. Die99.
    H. Dierks. Specification and Verification of Polling Real-Time Systems. PhD thesis, University of Oldenburg, July 1999.Google Scholar
  10. FJ97.
    K. Feyerabend and B. Josko. A Visual Formalism for Real-Time Requirements Specifications. In M. Bertran and T. Rus, editors, ARTS’97, volume 1231 of LNCS, pages 156–168, Mallorca, Spain, May 1997. Springer.Google Scholar
  11. HL94.
    C. Heitmeyer and N. Lynch. The Generalized Railroad Crossing. In IEEE Real-Time Systems Symposium, 1994.Google Scholar
  12. HLR93.
    N. Halbwachs, F. Lagnier, and P. Raymond. Synchronous observers and the verification of reactive systems. In M. Nivat, C. Rattray, T. Rus, and G. Scollo, editors, Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST’93, Workshops in Computing. Springer, June 1993.Google Scholar
  13. HM96.
    C. Heitmeyer and D. Mandrioli, editors. Formal Methods for Real-Time Computing, volume 5 of Trends in Software. Wiley, 1996.Google Scholar
  14. HNSY94.
    T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic Model Checking for Real-Time Systems. Information and Computation, 111:193–244, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  15. HZ97.
    M.R. Hansen and Zhou Chaochen. Duration Calculus: Logical Foundations. Formal Aspects of Computing, 9:283–330, 1997.zbMATHCrossRefGoogle Scholar
  16. Kle00.
    C. Kleuker. Constraint Diagrams. PhD thesis, University of Oldenburg, December 2000.Google Scholar
  17. Let00.
    M. Lettrari. Eine Testautomatensemantik für Constraint Diagrams und ihre Anwendung. Master’s thesis, University of Oldenburg, Department of Computer Science, Oldenburg, Germany, April 2000.Google Scholar
  18. LPW97.
    K.G. Larsen, P. Petterson, and Wang Yi. Uppaal in a nutshell. Software Tools for Technology Transfer, 1(1+2):134–152, December 1997.Google Scholar
  19. LPW98.
    M. Lindahl, P. Pettersson, and Wang Yi. Formal Design and Analysis of a Gear Controller. In Steffen [Ste98], pages 281–297.CrossRefGoogle Scholar
  20. Mos85.
    B. Moszkowski. A Temporal Logic for Multilevel Reasoning about Hardware. IEEE Computer, 18(2):10–19, 1985.Google Scholar
  21. Rav95.
    A.P. Ravn. Design of Embedded Real-Time Computing Systems. Technical Report 1995-170, Technical University of Denmark, 1995.Google Scholar
  22. Sch01.
    R. Schlör. Symbolic Timing Diagrams: A Visual Formalism for Model Verification. PhD thesis, University of Oldenburg, Department of Computer Science, Oldenburg, Germany, 2001.Google Scholar
  23. Ste98.
    B. Steffen, editor. Tools and Algorithms for the Construction and Analysis of Systems, volume 1384 of LNCS. Springer, 1998.Google Scholar
  24. Yov97.
    S. Yovine. Kronos: a verification tool for real-time systems. Software Tools for Technology Transfer, 1(1+2):123–133, December 1997.Google Scholar
  25. Zho93.
    Zhou Chaochen. Duration Calculi: An overview. In D. Bjørner, M. Broy, and I.V. Pottosin, editors, Formal Methods in Programming and Their Application, volume 735 of LNCS, pages 256–266. Springer, 1993.CrossRefGoogle Scholar
  26. ZHR91.
    Zhou Chaochen, C.A.R. Hoare, and A.P. Ravn. A Calculus of Durations. IPL, 40/5:269–276, 1991.CrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Henning Dierks
    • 1
  • Marc Lettrari
    • 2
  1. 1.Department of Computer ScienceUniversity of OldenburgOldenburgGermany
  2. 2.OFFISOldenburgGermany

Personalised recommendations