Advertisement

Timed Verification of Asynchronous Circuits

  • Jesper Møller
  • Henrik Hulgaard
  • Henrik Reif Andersen
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2549)

Abstract

We describe a methodology for analyzing timed systems symbolically. Given a formula representing a set of timed states, we describe howto determine a new formula that represents the set of states reachable by taking a discrete transition or by advancing time. The symbolic representations are given as formulae expressed in a simple first-order logic over constraints of the form x-yd which can be combined with Boolean operators and existentially quantified. The main contribution is a way of advancing time symbolically essentially by quantifying out a special variable z which is used to represent the current zero point in time. We describe howt o model asynchronous circuits using timed guarded commands and provide examples that demonstrate the potential of the symbolic analysis.

Keywords

Model Check Discrete State Mutual Exclusion Boolean Variable Reachable State 
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. Techniques for Automatic Verication of Real-Time Systems. PhD thesis, Department of Computer Science, Stanford University, 1991. 299Google Scholar
  2. [2]
    R. Alur and D. Dill. The theory of timed automata. In Proc. Real-Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science, pages 28–73. Springer-Verlag, 1991. 275, 278, 279, 285CrossRefGoogle Scholar
  3. [3]
    E. Asarin, M. Bozga, A. Kerbrat, O. Maler, M. Pnueli, and A. Rasse. Data structures for the verification of timed automata. In O. Maler, editor, Proc. International Workshop on Hybrid and Real-Time Systems, volume 1201 of Lecture Notes in Computer Science, pages 346–360, Grenoble, France, 1997. Springer-Verlag. 278Google Scholar
  4. [4]
    F. Balarin. Approximate reachability analysis of timed automata. In Proc. Real-Time Systems Symposium, pages 52–61. IEEE Computer Society Press, 1996. 278Google Scholar
  5. [5]
    E. Balas. Disjunctive programming. Annals of Discrete Mathematics, 5:3–51, 1979. 300zbMATHCrossRefMathSciNetGoogle Scholar
  6. [6]
    G. Behrmann, K. G. Larsen, J. Pearson, C. Weise, and W. Yi. Efficient timed reachability analysis using clock difference diagrams. Technical Report 99/105, DoCS, Uppsala University, 1999. 277Google Scholar
  7. [7]
    W. Belluomini and C. J. Myers. Efficient timing analysis algorithms for timed state space exploration. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 88–100, April 1997. 278Google Scholar
  8. [8]
    W. Belluomini and C. J. Myers. Verification of timed systems using POSETs. In Proc. Tenth International Conference on Computer-Aided Verification, pages 403–415, June 1998. 278Google Scholar
  9. [9]
    B. Berthomieu and M. Diaz. Modeling and verification of time dependent systems using time Petri nets. IEEE Transactions on Software Engineering, 17(3):259–273, 1991. 275, 276, 278, 279CrossRefMathSciNetGoogle Scholar
  10. [10]
    A. Blass and Y. Gurevich. Fixed-choice and independent-choice logics. Technical Report TR-369-98, University of Michigan, August 1998. 280Google Scholar
  11. [11]
    P. Bouyer, C. Dufourd, E. Fleury, and A. Petit. Are timed automata updatable? In Proc. 12th International Conference on Computer-Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 464–479. Springer-Verlag, July 2000. 299Google Scholar
  12. [12]
    M. Bozga, O. Maler, A. Pnueli, and S. Yovine. Some progress in the symbolic verification of timed automata. In O. Grumberg, editor, Proc. Ninth International Conference on Computer-Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 179–190, 1997. 278Google Scholar
  13. [13]
    R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, 1986. 274, 302CrossRefGoogle Scholar
  14. [14]
    J. R. Burch. Trace Algebra for Automatic Verification of Real-Time Concurrent Systems. PhD thesis, Carnegie Mellon, August 1992. 278Google Scholar
  15. [15]
    J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. Fifth Annual IEEE Symposium on Logic in Computer Science, pages 428–439. IEEE Computer Society Press, 1990. 274Google Scholar
  16. [16]
    S. V. Campos, E. Clarke, W. Marrero, M. Minea, and H. Hiraishi. Computing quantitative characteristics of finite-state real-time systems. In Proc. Real-Time Systems Symposium, pages 266–70. IEEE Computer Society Press, December 1994. 278Google Scholar
  17. [17]
    E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Logics of Programs, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer-Verlag, May 1981. 274, 297Google Scholar
  18. [18]
    G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Proc. Second GI Conference, volume 33 of Lecture Notes in Computer Science, pages 134–183. Springer-Verlag, 1975. 301Google Scholar
  19. [19]
    S. A. Cook. The complexity of theorem-proving procedures. In Proc. Third Annual ACM Symposium on Theory of Computing, pages 151–158, Shaker Heights, Ohio, 1971. 301Google Scholar
  20. [20]
    D. C. Cooper. Theorem proving in arithmetic without multiplication. Machine Intelligence, 7:91–99, 1972. 300, 301zbMATHGoogle Scholar
  21. [21]
    T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. MIT Press, 1994. 277, 300Google Scholar
  22. [22]
    E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 18(8):453–457, August 1975. 275zbMATHCrossRefMathSciNetGoogle Scholar
  23. [23]
    D. L. Dill. Timing assumptions and verification of finite-state concurrent systems. In Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 197–212. Springer-Verlag, 1989. 276, 277, 278, 301Google Scholar
  24. [24]
    J. Ferrante and J. R. Geiser. An efficient decision procedure for the theory of rational order. Theoretical Computer Science, 4(2):227–233, 1977. 301zbMATHCrossRefMathSciNetGoogle Scholar
  25. [25]
    J. Ferrante and C. Rackoff. A decision procedure for the first order theory of real addition with order. SIAM Journal of Computing, 4(1):69–76, 1975. 301zbMATHCrossRefMathSciNetGoogle Scholar
  26. [26]
    M. J. Fischer and M. O. Rabin. Super-exponential complexity of presburger arithmetic. In Proc. SIAM-AMS Symposium in Applied Mathematics, volume 7, pages 27–41, 1974. 300MathSciNetGoogle Scholar
  27. [27]
    J. B. J. Fourier. Second extrait. In G. Darboux, editor, Oeuvres, pages 325–328, Paris, 1890. Gauthiers-Villars. 301, 303Google Scholar
  28. [28]
    K. Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter System (On formal undecidable theorems in Principia Mathematica and related systems). In Monatshefte für Mathematik und Physik, volume 38, pages 173–198, 1931. 300zbMATHCrossRefGoogle Scholar
  29. [29]
    M. R. Greenstreet and T. Ono-Tesfaye. A fast, ASP*, RGD arbiter. In Proc. Fifth International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 173–185, Barcelona, Spain, April 1999. IEEE. 307Google Scholar
  30. [30]
    T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994. 275, 278, 297, 300zbMATHCrossRefMathSciNetGoogle Scholar
  31. [31]
    D. Hilbert and P. Bernays. Grundlagen der Mathematik, volume 2. Springer-Verlag, 1939. 280Google Scholar
  32. [32]
    J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979. 300, 301Google Scholar
  33. [33]
    N. K. Karmarkar. A newp olynomial-time algorithm for linear programming. Proc. 16th Annual ACM Symposium on Theory of Computing, pages 302–311, 1984. 300Google Scholar
  34. [34]
    M. Koubarakis. Complexity results for first-order theories of temporal constraints. In J. Doyle, E. Sandewall, and P. Torasso, editors, Proc. Fourth Internatinal Conference on Principles of Knowledge Representation and Reasoning, pages 379–390, San Francisco, California, 1994. Morgan Kaufmann. 300, 301Google Scholar
  35. [35]
    K. G. Larsen, P. Pettersson, and W. Yi. Model-checking for real-time systems. In Proc. Tenth International Conference on Fundamentals of Computation Theory, volume 965 of Lecture Notes in Computer Science, pages 62–88, August 1995. 276, 278Google Scholar
  36. [36]
    K. G. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer, 1(1–2):134–152, 1997. 302zbMATHGoogle Scholar
  37. [37]
    O. Maler and A. Pnueli. Timing analysis of asynchronous circuits using timed automata. In P. E. Camurati and H. Eveking, editors, Proc. Eighth International Conference on Correct Hardware Design and Verification Methods, volume 987 of Lecture Notes in Computer Science, pages 189–205. Springer-Verlag, 1995. 286Google Scholar
  38. [38]
    J. Møller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Difference decision diagrams. In Proc. 13th International Conference on Computer Science Logic, volume 1683 of Lecture Notes in Computer Science, pages 111–125, Madrid, Spain, September 1999. 277, 302Google Scholar
  39. 39]
    J. Møller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Fully symbolic model checking of timed systems using difference decision diagrams. In Proc. First International Workshop on Symbolic Model Checking, volume 23–2 of Electronic Notes in Theoretical Computer Science, pages 89–108, Trento, Italy, July 1999. 279Google Scholar
  40. [40]
    D. Oppen. A 22 2 pn upper bound on the complexity of Presburger arithmetic. Journal of Computer and System Sciences, 16:323–332, 1978. 301zbMATHCrossRefMathSciNetGoogle Scholar
  41. [41]
    C. H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994. 300Google Scholar
  42. [42]
    M. Presburger. Über die vollständigkeit eines gewissen systems der arithmetik ganzer zählen, in welchem die addition als einzige operation hervortritt. Comptes-Rendus du I Congres de Mathematiciens des pays Slaves, pages 92–101, 1929. 300Google Scholar
  43. [43]
    T. G. Rokicki. Representing and Modeling Digital Circuits. PhD thesis, Stanford University, 1993. 276, 278Google Scholar
  44. [44]
    T. G. Rokicki and C. J. Myers. Automatic verification of timed circuits. In D. L. Dill, editor, Proc. Sixth International Conference on Computer-Aided Verification, volume 818 of Lecture Notes in Computer Science, pages 468–480, 1994. 278Google Scholar
  45. [45]
    S. Bornot and J. Sifakis. An algebraic framework for urgency. Information and Computation, 163(1):172–202, 2000. 281zbMATHCrossRefMathSciNetGoogle Scholar
  46. [46]
    R. Shostak. On the SUP-INF method for proving Presburger formulas. Journal of the ACM, 4(24):529–543, October 1977. 300CrossRefMathSciNetGoogle Scholar
  47. [47]
    A. Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley, CA, 2nd edition, 1951. 300, 301zbMATHGoogle Scholar
  48. [48]
    E. Verlind, G. de Jong, and B. Lin. Efficient partial enumeration for timing analysis of asynchronous systems. In Proc. ACM/IEEE Design Automation Conference, pages 55–58, June 1996. 278Google Scholar
  49. [49]
    H. Wong-Toi and D. L. Dill. Approximations for verifying timing properties. In Theories and Experiences for Real-Time Systems Development, chapter 7, pages 177–204. World Scientific Publishing, 1994. 278Google Scholar
  50. [50]
    S. Yovine. Kronos: A verification tool for real-time systems. International Journal on Software Tools for Technology Transfer, 1(1–2):123–133, October 1997. 276, 278, 302zbMATHGoogle Scholar
  51. [51]
    S. Yovine. Model checking timed automata. In Embedded Systems, volume 1494 of Lecture Notes in Computer Science, pages 114–152. Springer-Verlag, October 1998. 278Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Jesper Møller
    • 1
  • Henrik Hulgaard
    • 1
  • Henrik Reif Andersen
    • 1
  1. 1.Department of InnovationThe IT University of CopenhagenDenmark

Personalised recommendations