[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech

  • Conference paper
Hybrid Systems: Computation and Control (HSCC 2005)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3414))

Included in the following conference series:

  • 3038 Accesses

Abstract

In 1995, HyTech broke new ground as a potentially powerful tool for verifying hybrid systems – yet it has remained severely limited in its applicability to more complex systems. We address the main problems of HyTech with PHAVer, a new tool for the exact verification of safety properties of hybrid systems with piecewise constant bounds on the derivatives. Affine dynamics are handled by on-the-fly overapproximation and by partitioning the state space based on user-definable constraints and the dynamics of the system. PHAVer’s exact arithmetic is robust due to the use of the Parma Polyhedra Library, which supports arbitrarily large numbers. To manage the complexity of the polyhedral computations, we propose methods to conservatively limit the number of bits and constraints of polyhedra. Experimental results for a navigation benchmark and a tunnel diode circuit show the effectiveness of the approach.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Henzinger, T.A.: The theory of hybrid automata. In: Proc. IEEE Symp. Logic in Computer Science, LICS 1996, New Brunswick, New Jersey, July 27-30, pp. 278–292. IEEE Computer Society, Los Alamitos (1996)

    Chapter  Google Scholar 

  2. Ho, P.H.: Automatic Analysis of Hybrid Systems. PhD thesis, Cornell University, Technical Report CSD-TR95-1536 (1995)

    Google Scholar 

  3. Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HYTECH: A model checker for hybrid systems. Int. Journal on Software Tools for Technology Transfer 1, 110–122 (1997)

    Article  MATH  Google Scholar 

  4. Henzinger, T.A., Preussig, J., Wong-Toi, H.: Some lessons from the hytech experience. In: Proceedings of the 40th Annual Conference on Decision and Control (CDC 2001), pp. 2887–2892. IEEE Press, Los Alamitos (2001)

    Google Scholar 

  5. Cofer, D.D., Engstrom, E., Goldman, R.P., Musliner, D.J., Vestal, S.: Applications of model checking at Honeywell Laboratories. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 296–303. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  6. Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly not closed convex polyhedra and the Parma Polyhedra Library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 213–229. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  7. Fehnker, A., Ivancic, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 326–341. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Gupta, S., Krogh, B.H., Rutenbar, R.A.: Towards formal verification of analog designs. In: Proc. IEEE Intl. Conf. on Computer-Aided Design (ICCAD 2004), San Jose, CA, USA, November 7–11 (2004)

    Google Scholar 

  9. Frehse, G., Han, Z., Krogh, B.H.: Assume-guarantee reasoning for hybrid i/o-automata by over-approximation of continuous interaction. In: Proc. IEEE Conf. Decision and Control (CDC 2004), Atlantis, Bahamas, December 14–17 (2004)

    Google Scholar 

  10. Henzinger, T.A., Horowitz, B., Majumdar, R., Wong-Toi, H.: Beyond HYTECH: Hybrid systems analysis using interval numerical methods. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 130–144. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  11. Preussig, J., Kowalewski, S., Wong-Toi, H., Henzinger, T.A.: An algorithm for the approximative analysis of rectangular automata. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 228–240. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  12. Henzinger, T.A., Ho, P.H., Wong-Toi, H.: Hytech: the next generation. In: Proc. IEEE Real-Time Systems Symp. (RTSS 1995), pp. 56–65. IEEE Computer Society, Los Alamitos (1995)

    Chapter  Google Scholar 

  13. Henzinger, T.A., Ho, P.H., Wong-Toi, H.: Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Control 43, 540–554 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  14. Stursberg, O., Krogh, B.H.: Efficient representation and computation of reachable sets for hybrid systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 482–497. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  15. Silva, B.I., Stursberg, O., Krogh, B.H., Engell, S.: An assessment of the current status of algorithmic approaches to the verification of hybrid systems. In: Proc. 40th Conference on Decision and Control, CDC 2001 (2001)

    Google Scholar 

  16. Lynch, N.A., Segala, R., Vaandrager, F.W.: Hybrid I/O automata. Information and Computation 185, 105–157 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  17. Ivancic, F.: Modeling and Analysis of Hybrid Systems. PhD thesis, University of Pennsylvania, Philadelphia, PA (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Electrical and Computer Engineering, Carnegie Mellon University, Pittsburgh, PA, 15213, USA

    Goran Frehse

Authors
  1. Goran Frehse
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Automatic Control Laboratory, ETH Zurich, 8092, Zurich, Switzerland

    Manfred Morari

  2. Computer Engineering and Networks Laboratory, ETH Zurich, Switzerland

    Lothar Thiele

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Frehse, G. (2005). PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. In: Morari, M., Thiele, L. (eds) Hybrid Systems: Computation and Control. HSCC 2005. Lecture Notes in Computer Science, vol 3414. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31954-2_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-31954-2_17

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-25108-8

  • Online ISBN: 978-3-540-31954-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation