Modeling and Checking Networks of Communicating Real-Time Processes

  • Jürgen Ruf
  • Thomas Kropf
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


In this paper we present a new modeling formalism that is well suited for modeling real-time systems in different application areas and on various levels of abstraction. These I/O-interval structures extend interval structures by a new communication method, where input sensitive transitions are introduced. The transitions can be labeled time intervals as well as with communication variables. For interval structures, efficient model checking techniques based on MTBDDs exist. Thus, after composing networks of I/O-interval structures, efficient model checking of interval structures is applicable. The usefulness of the new approach is demonstrated by various real-world case studies, including experimental result.


Model Check Atomic Proposition Kripke Structure Rotary Table Symbolic Model Check 
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.


  1. [1]
    R. Alur and D. Dill. Automata for Modeling Real-Time Systems. In International Colloquium on Automata, Languages and Programming, LNCS, NY, 1990. Springer-Verlag.Google Scholar
  2. [2]
    R. Alur, C. Courcoubetics, and D. Dill. Model Checking for Real-Time Systems. In Symposium on Logic in Computer Science, Washington, D.C., 1990. IEEE Computer Society Press.Google Scholar
  3. [3]
    T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic Model Checking for Real-Time Systems. In IEEE Symposium on Logic in Computer Science (LICS), pages 394–406, Santa-Cruz, California, June 1992. IEEE Computer Science Press.Google Scholar
  4. [4]
    M. Bozga, O. Maler, A. Pnueli, and S. Yovine. Some progress in the symbolic verification of timed automata. In O. Grumberg, editor, Conference on Computer Aided Verification (CAV), volume 1254 of LNCS, pages 179–190. Springer Verlag, June 1997.Google Scholar
  5. [5]
    S. Campos and E. Clarke. Real-Time Symbolic Model Checking for Discrete Time Models. In T. Rus and C. Rattray, editors, Theories and Experiences for Real-Time System Development, AMAST Series in Computing. AMAST Series in Computing, May 1994.Google Scholar
  6. [6]
    J. Frößl, J. Gerlach, and T. Kropf. An Efficient Algorithm for Real-Time Model Checking. In European Design and Test Conference (EDTC), pages 15–21, Paris, France, March 1996. IEEE Computer Society Press (Los Alamitos, California).CrossRefGoogle Scholar
  7. [7]
    J. Ruf and T. Kropf. Using MTBDDs for discrete timed symbolic model checking. Multiple-Valued Logic-An International Journal, 1998. Special Issue on Decision Diagrams, Gordon and Breach.Google Scholar
  8. [8]
    J. Ruf and T. Kropf. Symbolic model checking for a discrete clocked temporal logic with intervals. In Conference on Correct Hardware Design and Verification Methods (CHARME), pages 146–166, Montreal, Canada, October 1997. Chapman and Hall.Google Scholar
  9. [9]
    R. Bahar, E. Frohm, C. Gaona, G. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic Decision Diagrams and Their Applications. In IEEE/ACM International Conference on Computer Aided Design (ICCAD), pages 188–191, Santa Clara, California, November 1993. ACM/IEEE, IEEE Computer Society Press.Google Scholar
  10. [10]
    E. Clarke, K. McMillian, X. Zhao, M. Fujita, and J. Y. Yang. Spectral Transforms for large Boolean Functions with Application to Technology Mapping. In ACM/IEEE Design Automation Conference (DAC), pages 54–60, Dallas, TX, June 1993.Google Scholar
  11. [11]
    J. Ruf and T. Kropf. Using MTBDDs for composition and model checking of real-time systems. In FMCAD 1998. Springer, November 1998.Google Scholar
  12. [12]
    S. Johnson, P. Miner, and A. Camilleri. Studies of the single pulser in various reasoning systems. In International Conference on Theorem Provers in Circuit Design (TPCD), volume 901 of LNCS, Bad Herrenalb, Germany, September 1994. Springer-Verlag, 1995.Google Scholar
  13. [13]
    C. Lewerentz and T. Lindner, editors. Formal Development of Reactive Systems-Case Study Production Cell, number 891 in LNCS. Springer, 1995.zbMATHGoogle Scholar
  14. [14]
    SAE. J1850 class B data communication network interface. The Engineering Society For Advancing Mobility Land Sea Air and Space, October 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Jürgen Ruf
    • 1
  • Thomas Kropf
    • 1
  1. 1.Institute of Computerdesign and Fault ToleranceUniversity of Karlsruhe,Kaiserstr. 12KarlsruheGermany

Personalised recommendations