Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Revisiting Polyhedral Analysis for Hybrid Systems

  • Conference paper
  • First Online:
Static Analysis (SAS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11822))

Included in the following conference series:

Abstract

Thanks to significant progress in the adopted implementation techniques, the recent years have witnessed a renewed interest in the development of analysis tools based on the domain of convex polyhedra. In this paper we revisit the application of this abstract domain to the case of reachability analysis for hybrid systems, focusing on the lesson learned during the development of the tool PHAVerLite. In particular, we motivate the implementation of specialized versions of several well known abstract operators, as well as the adoption of a heuristic technique (boxed polyhedra) for the handling of finite collections of polyhedra, showing their impact on the efficiency of the analysis tool.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    The tests on PHAVer-lite/SX and PHAVerLite have been executed on an Intel Core i7-3632QM CPU; the tests on PHAVer/SX were executed on a faster CPU (\({\sim }25\%\)).

  2. 2.

    The synchronization label \(a \in Lab \) only plays a role when a hybrid automaton is defined as the parallel composition of several smaller automata.

  3. 3.

    This is the case for the Apron library [24] and for PPLite up to version 0.3.

  4. 4.

    This was done for exposition purposes, since this specific benchmark can be successfully verified, more efficiently, by using a single polyhedron for each location.

  5. 5.

    Note that this implies that neither Lemma 2 applies.

  6. 6.

    To some extent, the reasoning should also apply to constraint-only representations, if the implementation attempts to identify and remove redundant constraints.

References

  1. Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Sci. Comput. Program. 58(1–2), 28–56 (2005)

    Article  MathSciNet  Google Scholar 

  2. Bagnara, R., Hill, P.M., Zaffanella, E.: Not necessarily closed convex polyhedra and the double description method. Formal Aspects Comput. 17(2), 222–257 (2005)

    Article  Google Scholar 

  3. Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. Softw. Tools Technol. Transfer 8(4/5), 449–466 (2006)

    Article  Google Scholar 

  4. Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008)

    Article  MathSciNet  Google Scholar 

  5. Bagnara, R., Hill, P.M., Zaffanella, E.: Applications of polyhedral computations to the analysis and verification of hardware and software systems. Theoret. Comput. Sci. 410(46), 4672–4691 (2009)

    Article  MathSciNet  Google Scholar 

  6. Becchi, A., Zaffanella, E.: A direct encoding for NNC polyhedra. In: Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14–17, 2018, Proceedings, Part I, pp. 230–248 (2018)

    Chapter  Google Scholar 

  7. Becchi, A., Zaffanella, E.: An efficient abstract domain for not necessarily closed polyhedra. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 146–165. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99725-4_11

    Chapter  Google Scholar 

  8. Bemporad, A., Fukuda, K., Torrisi, F.D.: Convexity recognition of the union of polyhedra. Comput. Geom. Theory Appl. 18(3), 141–154 (2001)

    Article  MathSciNet  Google Scholar 

  9. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, pp. 238–252. ACM Press, Los Angeles (1977)

    Google Scholar 

  10. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages, pp. 269–282. ACM Press, San Antonio (1979)

    Google Scholar 

  11. Cousot, P., Giacobazzi, R., Ranzato, F.: A\({^2}\)I: abstract\({^2}\) interpretation. PACMPL 3(POPL), 42:1–42:31 (2019)

    Google Scholar 

  12. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pp. 84–96. ACM Press, Tucson (1978)

    Google Scholar 

  13. Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31954-2_17

    Chapter  MATH  Google Scholar 

  14. Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Softw. Tools Technol. Transfer 10(3), 263–279 (2008)

    Article  Google Scholar 

  15. Frehse, G., et al.: ARCH-COMP19 category report: Hybrid systems with piecewise constant dynamics. In: 6th International Workshop on Applied Verification of Continuous and Hybrid Systems ARCH19. EPiC Series in Computing, vol. 61, pp. 1–13. EasyChair (2019)

    Google Scholar 

  16. Frehse, G., et al.: ARCH-COMP18 category report: Hybrid systems with piecewise constant dynamics. In: 5th International Workshop on Applied Verification of Continuous and Hybrid Systems ARCH18. EPiC Series in Computing, vol. 54, pp. 1–13. EasyChair (2018)

    Google Scholar 

  17. Frehse, G., et al.: Spaceex: scalable verification of hybrid systems. In: Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA. Proceedings, pp. 379–395 (2011)

    Google Scholar 

  18. Guernic, C.L., Girard, A.: Reachability analysis of hybrid systems using support functions. In: 21st International Conference on Computer Aided Verification, CAV 2009, Grenoble, France. Proceedings, pp. 540–554 (2009)

    Google Scholar 

  19. Halbwachs, N., Merchat, D., Gonnord, L.: Some ways to reduce the space dimension in polyhedra computations. Formal Meth. Syst. Des. 29(1), 79–95 (2006)

    Article  Google Scholar 

  20. Halbwachs, N., Merchat, D., Parent-Vigouroux, C.: Cartesian factoring of polyhedra in linear relation analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 355–365. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44898-5_20

    Chapter  MATH  Google Scholar 

  21. Halbwachs, N., Proy, Y.-E., Raymond, P.: Verification of linear hybrid systems by means of convex approximations. In: Le Charlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 223–237. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58485-4_43

    Chapter  Google Scholar 

  22. Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Meth. Syst. Des. 11(2), 157–185 (1997)

    Article  Google Scholar 

  23. Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. Softw. Tools Technol. Transfer 1(1+2), 110–122 (1997)

    Article  Google Scholar 

  24. Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: 21st International Conference on Computer Aided Verification, CAV 2009, Grenoble, France. Proceedings, pp. 661–667 (2009)

    Chapter  Google Scholar 

  25. Lamport, L.: A fast mutual exclusion algorithm. ACM Trans. Comput. Syst. 5(1), 1–11 (1987)

    Article  Google Scholar 

  26. Maréchal, A., Monniaux, D., Périn, M.: Scalable minimizing-operators on polyhedra via parametric linear programming. In: Static Analysis - 24th International Symposium, SAS 2017, New York, NY, USA, Proceedings, pp. 212–231 (2017)

    Google Scholar 

  27. Miné, A.: The octagon abstract domain. Higher-Order Symbolic Comput. 19(1), 31–100 (2006)

    Article  Google Scholar 

  28. Motzkin, T.S., Raiffa, H., Thompson, G.L., Thrall, R.M.: The double description method. In: Contributions to the Theory of Games. Annals of Mathematics Studies, vol. II, No. 28, pp. 51–73. Princeton University Press, Princeton (1953)

    Google Scholar 

  29. Pelleau, M., Miné, A., Truchet, C., Benhamou, F.: A constraint solver based on abstract domains. In: 14th International Conference Verification, Model Checking, and Abstract Interpretation, VMCAI 2013, Rome, Italy. Proceedings, pp. 434–454 (2013)

    Google Scholar 

  30. Sankaranarayanan, S., Colón, M.A., Sipma, H., Manna, Z.: Efficient strongly relational polyhedral analysis. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 111–125. Springer, Heidelberg (2005). https://doi.org/10.1007/11609773_8

    Chapter  Google Scholar 

  31. Schupp, S., Ábrahám, E., Chen, X., Ben Makhlouf, I., Frehse, G., Sankaranarayanan, S., Kowalewski, S.: Current challenges in the verification of hybrid systems. In: Berger, C., Mousavi, M.R. (eds.) CyPhy 2015. LNCS, vol. 9361, pp. 8–24. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25141-7_2

    Chapter  Google Scholar 

  32. Singh, G., Püschel, M., Vechev, M.T.: Fast polyhedra abstract domain. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18–20, 2017, pp. 46–59 (2017)

    Google Scholar 

Download references

Acknowledgment

The work of Enea Zaffanella has been partially supported by Gruppo Nazionale per il Calcolo Scientifico of Istituto Nazionale di Alta Matematica.

Author information

Authors and Affiliations

  1. University of Udine, Udine, Italy

    Anna Becchi

  2. University of Parma, Parma, Italy

    Enea Zaffanella

Authors
  1. Anna Becchi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Enea Zaffanella
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Anna Becchi or Enea Zaffanella .

Editor information

Editors and Affiliations

  1. University of Colorado, Boulder, CO, USA

    Bor-Yuh Evan Chang

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Becchi, A., Zaffanella, E. (2019). Revisiting Polyhedral Analysis for Hybrid Systems. In: Chang, BY. (eds) Static Analysis. SAS 2019. Lecture Notes in Computer Science(), vol 11822. Springer, Cham. https://doi.org/10.1007/978-3-030-32304-2_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32304-2_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32303-5

  • Online ISBN: 978-3-030-32304-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation