Skip to main content
SpringerLink
Log in

From Electrical Switched Networks to Hybrid Automata

  • Conference paper
  • First Online:
FM 2016: Formal Methods (FM 2016)

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

Included in the following conference series:

Abstract

In this paper, we propose a novel symbolic approach to automatically synthesize a Hybrid Automaton (HA) from a switched electrical network. The input network consists of a set of physical components interconnected according to some reconfigurable network topology. The underlying model defines a local dynamics for each component in terms of a Differential-Algebraic Equation (DAE), and a set of network topologies by means of discrete switches. Each switch configuration induces a different topology, where the behavior of the system is a Hybrid Differential-Algebraic Equations.

Two relevant problems for these networks are validation and reformulation. The first consists of determining if the network admits an Ordinary Differential Equations (ODE) that describes its dynamics; the second consists of obtaining such ODE from the initial DAE. This step is a key enabler to use existing formal verification tools that can cope with ODEs but not with DAEs.

Since the number of network topologies is exponential in the number of switches, first, we propose a technique based on Satisfiability Modulo Theories (SMT) that can solve the validation problem symbolically, avoiding the explicit enumeration of the topologies. Then, we show an SMT-based algorithm that reformulates the network into a symbolic HA. The algorithm avoids to explicitly enumerate the topologies clustering them by equivalent continuous dynamics.

We implemented the approach with several optimizations and we compared it with the explicit enumeration of configurations. The results demonstrate the scalability of our technique.

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

Access this chapter

Log in via an institution
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

References

  1. Agrawal, A., Simon, G., Karsai, G.: Semantic translation of simulink/stateflow models to hybrid automata using graph transformations. Electron. Notes Theoret. Comput. Sci. 109, 43–56 (2004). Proceedings of the Workshop on Graph Transformation and Visual Modelling Techniques (GT-VMT2004). http://www.sciencedirect.com/science/article/pii/S1571066104052089

    Article  MATH  Google Scholar 

  2. Akers, A., Gassman, M., Smith, R.: Hydraulic Power System Analysis. Fluid Power and Control. CRC Press, Boca Raton (2006). https://books.google.it/books?id=Uo9gpXeUoKAC

    Book  MATH  Google Scholar 

  3. Bae, K., Kong, S., Gao, S.: SMT encoding of hybrid systems in dReal. In: Frehse, G., Althoff, M. (eds.) 1st and 2nd International Workshop on Applied verification for Continuous and Hybrid Systems, ARCH14 2015. EPiC Series in Computing, vol. 34, pp. 188–195. EasyChair, Manchester (2015)

    Google Scholar 

  4. Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, pp. 825–885 (2009). http://dx.doi.org/10.3233/978-1-58603-929-5-825

  5. Benner, P.: Large-scale Networks in Engineering and Life Sciences. Springer, New York (2014)

    Book  Google Scholar 

  6. Cimatti, A., Mover, S., Sessa, M.: From electrical switched networks to hybrid automata (extended version). In: Fitzgerald, J., et al. (eds.) FM 2016. LNCS, vol. 9995, pp. 164–181. Springer, Heidelberg (2016). http://es.fbk.eu/people/sessa/paper/FM2016/main.pdf

    Chapter  Google Scholar 

  7. Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-based model checker for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 52–67. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_4

    Google Scholar 

  8. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: ETAPS 2013, pp. 93–107. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36742-7_7

    Book  MATH  Google Scholar 

  9. Cimatti, A., Mover, S., Tonetta, S.: A quantifier-free SMT encoding of non-linear hybrid automata. In: FMCAD, pp. 187–195 (2012). http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6462573

  10. Dang, T., Donzé, A., Maler, O.: Verification of analog and mixed-signal circuits using hybrid system techniques. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 21–36. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30494-4_3

    Chapter  Google Scholar 

  11. Frehse, G., Krogh, B.H., Rutenbar, R.A., Maler, O.: Time domain verification of oscillator circuit properties. Electron. Notes Theoret. Comput. Sci. 153(3), 9–22 (2006). doi:10.1016/j.entcs.2006.02.019

    Article  Google Scholar 

  12. Gario, M., Micheli, A.: pysmt: a solver-agnostic library for fast prototyping of smt-based algorithms. In: SMT Workshop (2015)

    Google Scholar 

  13. Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, 27–30 July 1996, pp. 278–292 (1996). http://dx.doi.org/10.1109/LICS.1996.561342

  14. Janschek, K.: Mechatronic Systems Design: Methods, Models, Concepts. Springer Science & Business Media, Berlin (2011)

    MATH  Google Scholar 

  15. Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \(\delta \)-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200–205. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_15

    Google Scholar 

  16. Lee, H.L., Althoff, M., Hoelldampf, S., Olbrich, M., Barke, E.: Automated generation of hybrid system models for reachability analysis of nonlinear analog circuits. In: The 20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015, Chiba, Japan, 19–22 January 2015, pp. 725–730 (2015). http://dx.doi.org/10.1109/ASPDAC.2015.7059096

  17. Manamcheri, K., Mitra, S., Bak, S., Caccamo, M.: A step towards verification and synthesis from simulink/stateflow models. In: Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, 12–14 April 2011, pp. 317–318 (2011). http://doi.acm.org/10.1145/1967701.1967749

  18. Massarini, A., Reggiani, U., Kazimierczuk, M.K.: Analysis of networks with ideal switches by state equations. IEEE Trans. Circ. Syst. I: Fundam. Theory Appl. 44(8), 692–697 (1997)

    Article  MATH  Google Scholar 

  19. Mathworks, T.: Simscape power systems. http://it.mathworks.com/help/physmod/sps/index.html

  20. Minopoli, S., Frehse, G.: SL2SX translator: from simulink to spaceex models. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, Vienna, Austria, 12–14 April 2016, pp. 93–98 (2016). http://doi.acm.org/10.1145/2883817.2883826

  21. Mover, S., Cimatti, A., Tiwari, A., Tonetta, S.: Time-aware relational abstractions for hybrid systems. In: EMSOFT, pp. 14:1–14:10 (2013). http://dx.doi.org/10.1109/EMSOFT.2013.6658592

  22. Nguyen, L.V., Johnson, T.T.: Benchmark: DC-to-DC switched-mode power converters (buck converters, boost converters, and buck-boost converters). In: Frehse, G., Althoff, M. (eds.) ARCH14 2015, 1st and 2nd International Workshop on Applied Verification for Continuous and Hybrid Systems. EPiC Series in Computing, vol. 34, pp. 19–24. EasyChair (2015)

    Google Scholar 

  23. Nuzzo, P., Xu, M., Ozay, N., Finn, J.B., Sangiovanni-Vincentelli, A., Murray, R., Donze, A., Seshia, S.: A contract-based methodology for aircraft electric power system design. IEEE Access. http://icyphy.org/pubs/35.html

  24. Riaza, R.: Differential-Algebraic Systems: Analytical Aspects and Circuit Applications. World Scientific, Singapore (2008)

    Book  MATH  Google Scholar 

  25. SAE International: AIR 6110 - Contiguous Aircraft/System Development Process Example (2011)

    Google Scholar 

  26. Skaar, D.L.: Using the superposition method to formulate the state variable matrix for linear networks. IEEE Trans. Educ. 44(4), 311–314 (2001)

    Article  Google Scholar 

  27. Tiwari, A.: HybridSAL relational abstracter. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 725–731. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31424-7_56

    Chapter  Google Scholar 

  28. Tiwari, A.: Time-aware abstractions in HybridSal. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 504–510. Springer, Heidelberg (2015). doi:10.1007/978-3-319-21690-4_34

    Chapter  Google Scholar 

  29. Zaki, M.H., Tahar, S., Bois, G.: Formal verification of analog and mixed signal designs: survey and comparison. In: 2006 IEEE North-East Workshop on Circuits and Systems, pp. 281–284, June 2006

    Google Scholar 

  30. Zhang, Y., Sankaranarayanan, S., Somenzi, F.: Piecewise linear modeling of nonlinear devices for formal verification of analog circuits. In: FMCAD, pp. 196–203 (2012). http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6462574

Download references

Author information

Authors and Affiliations

  1. Fondazione Bruno Kessler, Trento, Italy

    Alessandro Cimatti & Mirko Sessa

  2. University of Colorado Boulder, Boulder, USA

    Sergio Mover

  3. University of Trento, Trento, Italy

    Mirko Sessa

Authors
  1. Alessandro Cimatti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sergio Mover
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mirko Sessa
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mirko Sessa .

Editor information

Editors and Affiliations

  1. Newcastle University, Newcastle upon Tyne, United Kingdom

    John Fitzgerald

  2. US Naval Research Laboratory, Washington, District of Columbia, USA

    Constance Heitmeyer

  3. ISTI-CNR, Pisa, Italy

    Stefania Gnesi

  4. University of Cyprus, Nicosia, Cyprus

    Anna Philippou

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Cimatti, A., Mover, S., Sessa, M. (2016). From Electrical Switched Networks to Hybrid Automata. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds) FM 2016: Formal Methods. FM 2016. Lecture Notes in Computer Science(), vol 9995. Springer, Cham. https://doi.org/10.1007/978-3-319-48989-6_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-48989-6_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-48988-9

  • Online ISBN: 978-3-319-48989-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation