Skip to main content
SpringerLink
Log in

Hybrid Systems and Verification by Abstraction

  • Chapter
  • First Online:
Hybrid Dynamical Systems

Part of the book series: Lecture Notes in Control and Information Sciences ((LNCIS,volume 457))

Abstract

The increase of functionality offered by today’s control systems based on embedded systems requires more effort to verify the controlled system, as a malfunction can yield catastrophic results. These systems are usually hybrid systems, mixing continuous and discrete dynamics. When analyzing a hybrid system, the dimension of the state space is often so large that formal verification is out of the question. Its analysis can be carried out using abstraction, namely constructing a system with a smaller state space, preserving the properties to verify in the original system. Making use of a notion of diagnosability for hybrid systems, generalizing the notion of observability, in this paper it is shown an abstraction procedure translating a hybrid system into a timed automaton, in order to verify observability and diagnosability properties. The subclass of hybrid systems here considered is that of the durational graphs. We propose a procedure to check diagnosability, and show that the verification problem belongs to the complexity class P. This procedure is applied to an electromagnetic valve system for camless engines.

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

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

References

  1. Acosta Lua, C., Toledo, B.C., Di Benedetto, M.D., Di Gennaro, S.: Feedback regulation of electromagnetic valves for camless engines. In: Proceedings of the European Control Conference—ECC 2007, pp. 4103–4110 (2007)

    Google Scholar 

  2. Lua, C.A., Toledo, B.C., Di Benedetto, M.D., Di Gennaro, S.: Output feedback regulation of electromagnetic valves for camless engines. In: Proceedings of the American Control Conference 2007, pp. 2967–2972 (2007)

    Google Scholar 

  3. Anai, H., Weispfenning, V.: In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) Reach Set computations Using Real Quantifier Elimination, Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, pp. 103–117. Springer, Berlin (2001)

    Google Scholar 

  4. Alur, R., Dill, D.L.: A theory of timed automata, l. Theor. Comput. Sci. 126, 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  5. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138, 3–34 (1995)

    Article  MATH  Google Scholar 

  6. Asarin, E., Bournez, O., Dang, T., Maler, O.: Approximate Reachability Analysis of Piecewise Linear Dynamical Systems, Hybrid Systems: Computation and Control. Lecture Notes in Computer Science. Springer, Pittsburgh (2000)

    Google Scholar 

  7. Choffrut, C., Goldwurm, M.: Timed automata with periodic clock constraints. J. Autom. Lang. Comb. 5, 371–404 (2000)

    MathSciNet  MATH  Google Scholar 

  8. Chutinan, A., Krogh, B.: Computing polyhedral approximations to flow pipes for dynamic systems. In: Proceedings of the 37th IEEE Conference on Decision and Control, pp. 2089–2094 (1998)

    Google Scholar 

  9. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge, Massachusetts (2002)

    Google Scholar 

  10. Di Benedetto, M.D., Di Gennaro, S., D’Innocenzo, A.: Error detection within a specific time horizon and application to air traffic management. In: Proceedings of the Joint 44th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC’05), Seville, Spain, pp. 7472–7477 (2005)

    Google Scholar 

  11. Di Benedetto, M.D., Di Gennaro, S., D’Innocenzo, A.: Critical States Detection with Bounded Probability of False Alarm and Application to Air Traffic Management. In: Proceedings of the 2nd IFAC Conference on Analysis and Design of Hybrid Systems (ADHS), Alghero, Sardinia, Italy (2006)

    Google Scholar 

  12. Di Gennaro, S., Castillo Toledo, B., Di Benedetto, M.D.: Non-linear control of electromagnetic valves for camless engines. Int. J. Control Special Issue Autom. Control 80(11), 1796–1813 (2007)

    Google Scholar 

  13. D’Innocenzo, A., Di Benedetto, M.D., Di Gennaro, S.: In: Hespanha, J., Tiwari, A. (eds.) Observability of Hybrid Automata by Abstraction, Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, pp. 169–183. Springer, Berlin (2006)

    Google Scholar 

  14. D’Innocenzo, A., Julius, A.A., Pappas, G.J., Di Benedetto, M.D., Di Gennaro, S.: Verification of temporal properties on hybrid automata by simulation relations. In: Proceedings of the 46th IEEE Conference on Decision and Control, New Orleans (2007)

    Google Scholar 

  15. D’Innocenzo, A., Julius, A.A., Di Benedetto, M.D., Pappas, G.J.: Approximate timed abstractions of hybrid automata. In: Proceedings of the 46th IEEE Conference on Decision and Control. New Orleans (2007)

    Google Scholar 

  16. Girard, A.: In: Morari, M., Thiele, L. (eds.) Reachability of Uncertain Linear Systems using Zonotopes, Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, pp. 291–305. Springer, Berlin (2005)

    Google Scholar 

  17. Guibas, L.J., Nguyen, A., Zhang, L.: Zonotopes as bounding volumes. In: Proceedings of the 14th annual ACM-SIAM symposium on Discrete Algorithms, pp. 803–812, Stanford (2003)

    Google Scholar 

  18. Han, Z., Krogh, B.H.: In: Hespanha, J., Tiwari, A. (eds.) Reachability Analysis of Large-Scale Affine Systems Using Low-Dimensional Polytopes, Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, pp. 287–301. Springer, Heidelberg (2006)

    Google Scholar 

  19. Kurzhanski, A.B., Varaiya, P.: In: Lynch, N., Krogh, B.H. (eds.) Ellipsoidal Techniques for Reachability Analysis, Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, pp. 202–214. Springer, Heidelberg (2000)

    Google Scholar 

  20. Kurzhanski, A.A., Varaiya, P.: Ellipsoidal toolbox. Technical Report, UC, Berkeley (2006)

    Google Scholar 

  21. Julius, A.A., Fainekos, G., Anand, M., Lee, I., Pappas, G.J.: Robust Test Generation and Coverage for Hybrid Systems, Hybrid Systems: Computation and Control. Lecture Notes in Computer Science. Springer, Heidelberg (2007)

    Google Scholar 

  22. Fourlas, G.K., Kyriakopoulos, K.J., Krikelis, N.J.: Diagnosability of hybrid systems. In: Proceedings of the 10th Mediterranean Conference on Control and Automation - MED2002, pp. 3994–3999, Lisbon (2002)

    Google Scholar 

  23. Frank, P.M.: Fault diagnosis in dynamic systems using analytical and knowledge-based redundancy—a survey and some new results. Automatica 26(3), 459–474 (1990)

    Article  MATH  Google Scholar 

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

    Article  MATH  Google Scholar 

  25. Hopcroft, J.E., Ullman, J.D.: Introduction to automata theory. Languages and Computation. Addison-Wesley, Reading (1979)

    Google Scholar 

  26. Girard, A.: In: Morari, M., Thiele, L. (eds.) Reachability of Uncertain Linear Systems using Zonotopes, Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, pp. 291–305. Springer, New York (2005)

    Google Scholar 

  27. Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computations for families of linear vector fields. J. Symb. Comput. 32(3), 231–253 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  28. Laroussinie, F., Markey, N., Schnoebelen, P.: Efficient timed model checking for discrete-time systems. Theor. Comput. Sci. 353(1–3), 249–271, Elsevier Science Publishers (2006) (http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-TCS05.pdf)

  29. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1), 134–152 (1997)

    Article  MATH  Google Scholar 

  30. Lin, F.: Diagnosability of discrete event systems and its applications. J. Discrete Event Dyn. Syst. 4(1), 197–212 (1994)

    Article  MATH  Google Scholar 

  31. Lygeros, J., Tomlin, C., Sastry, S.: Controllers for Reachability Specifications for Hybrid Systems. Automatica 35(3), 349–370 (1999) (Special Issue on Hybrid Systems)

    Google Scholar 

  32. McIlraith, S., Biswas, G., Clancy, D., Gupta, V.: In: Lynch, N., Krogh, B. (eds.) Hybrid Systems Diagnosis, in Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, pp. 282–295. Springer, Heidelberg (2000)

    Google Scholar 

  33. Ozveren, C.M., Willsky, A.S.: Observability of discrete event dynamic systems. IEEE Trans. Autom. Control 35(7), 797–806 (1990)

    Article  MathSciNet  Google Scholar 

  34. Paoli, A., Lafortune, S.: Safe diagnosability for fault tolerant supervision of discrete event systems. Automatica 41(8), 1335–1347 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  35. Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.: Diagnosability of discrete-event systems. IEEE Trans. Autom. Control 40(9), 1555–1575 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  36. Sheth, A., Hartung, C., Han, R.: A decentralized fault diagnosis system for wireless sensor networks. In: Proceedings of the 2nd IEEE International Conference on Mobile Ad-Hoc and Sensor Systems (MASS) 2005, pp. 192–194 (1999)

    Google Scholar 

  37. Tripakis, S.: In: Damm, W., Olderog, E.R. (eds.) Fault Diagnosis for Timed Automata. Lecture Notes in Computer Science, pp. 205–221. Springer, Heidelberg (2002)

    Google Scholar 

  38. http://wiki.grasp.upenn.edu/hst/index.php?n=Main.HomePage

  39. Yazarel, H., Pappas, G.J.: Geometric programming relaxations for linear system reachability. In: Proceedings of the 2004 American Control Conference, Boston, MA (2004)

    Google Scholar 

  40. Yoo, T., Lafortune, S.: Polynomial-time verification of diagnosability of partially-observed discrete-event systems. IEEE Trans. Autom. Control 47(9), 1491–1495 (2002)

    Article  MathSciNet  Google Scholar 

  41. Yovine, S.: Kronos: a verification tool for real-time systems. Int. J. Softw. Tools Technol. Transf. Springer-Verlag 1(1), 123–133 (1997)

    Article  MATH  Google Scholar 

  42. Zhao, F., Koutsoukos, X., Haussecker, H., Reich, J., Cheung, P.: Monitoring and fault diagnosis of hybrid systems. IEEE Trans. Syst. Man Cybern. I—Part B 35(6), 1225–1240 (2005)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Information Engineering, Computer Science and Mathematics, Center of Excellence DEWS, University of L’Aquila, Via G. Gronchi, 67100, L’Aquila, Italy

    Maria Domenica Di Benedetto, Stefano Di Gennaro & Alessandro D’Innocenzo

Authors
  1. Maria Domenica Di Benedetto
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefano Di Gennaro
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alessandro D’Innocenzo
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Stefano Di Gennaro .

Editor information

Editors and Affiliations

  1. LAMIH CNRS UMR 8201, University of Valenciennes and Hainaut-Cambresis, Valenciennes, France

    Mohamed Djemai

  2. LAMIH UMR-CNRS 8201, University of Valenciennes and Hainaut-Cambresis, Valenciennes, France

    Michael Defoort

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Di Benedetto, M.D., Di Gennaro, S., D’Innocenzo, A. (2015). Hybrid Systems and Verification by Abstraction. In: Djemai, M., Defoort, M. (eds) Hybrid Dynamical Systems. Lecture Notes in Control and Information Sciences, vol 457. Springer, Cham. https://doi.org/10.1007/978-3-319-10795-0_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10795-0_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10794-3

  • Online ISBN: 978-3-319-10795-0

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation