Model checking algorithms for analog verification

ABSTRACT

In this contribution we present the first method for model checking on nonlinear analog systems. Based on digital CTL model checking algorithms and results in hybrid model checking, we have developed a concept to adapt these ideas to analog systems. Using an automatic state space subdivision method the continuous state space is transfered into a discrete model. In doing this, the most challenging task is to retain the essential nonlinear behavior of the analog system. To describe analog specification properties, an extension to the CTL language is needed. Two small examples show the properties and advantages of this new method and the capability of the implemented prototype tool.

REFERENCES

• 1: R. Alur, T. Henzinger, G. Lafferriere, and G. Pappas. Discrete abstractions of hybrid systems. Proceedings of IEEE, (88):971--984, 2000.
• 2: J. Burch, E. Clarke, D. Long, K. McMillian, and D. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, 13(4):401--424, 1994.
• 3: M. Dellnitz, G. Froyland, and O. Junge. The algorithms behind gaio - set oriented numerical methods for dynamical systems. In B. Fiedler, editor, Ergodic Theory, Analysis, and Efficient Simulation of Dynamical Systems, pages 145--174. Springer-Verlag, Berlin, 2001.
• 4: M. Gunther and U. Feldmann. Cad-based electric circuit modeling in industry, part i: Mathemetical structure and index of network equations. Suveys on Mathematics for Industry, 8(2):97--129, 1999.
• 5: L. Hedrich and W. Hartong. Approaches to formal verification of analog circuits. In P. Wambacq, editor, Low-Power Design Techniques and CAD Tools for Analog and RF Intergrated Circuits, pages 155--191. Kluwer Academic Publishers, Boston, 2001.
• 6: Thomas A. Henzinger , Pei-Hsin Ho, Algorithmic Analysis of Nonlinear Hybrid Systems, Proceedings of the 7th International Conference on Computer Aided Verification, p.225-238, July 03-05, 1995
• 7: R. Kurshan and K. McMillan. Analysis of digital circuits trough symbolic reduction. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 10(11):1356--71, 1991.
• 8: R. Marz. Numerical methods for differential algebraic equations. Acta Numerica, pages 141--198, 1991.
• 9: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 10: A. Neumaier. Interval methods for systems of equations. Cambridge University Press, Cambridge, 1990.
• 11: Anuj Puri, Theory of hybrid systems and discrete event systems, University of California at Berkeley, Berkeley, CA, 1996

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.m Miscellaneous

General Terms:
Algorithms, Languages, Theory, Verification

Keywords:
formal methods, model checking, nonlinear analog systems