Top

Published in:

2016 | OriginalPaper | Chapter

From Electrical Switched Networks to Hybrid Automata

Authors : Alessandro Cimatti, Sergio Mover, Mirko Sessa

Published in: FM 2016: Formal Methods

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation

next chapter Danger Invariants

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 CrossRefMATH

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 CrossRefMATH

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)

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

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

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 CrossRef

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

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 CrossRefMATH

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 CrossRef

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 CrossRef

12.

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

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

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

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)CrossRefMATH

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)

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)CrossRefMATH

25.

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

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)CrossRef

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 CrossRef

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 CrossRef

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

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

Title: From Electrical Switched Networks to Hybrid Automata
Authors: Alessandro Cimatti
Sergio Mover
Mirko Sessa
Publisher: Springer International Publishing
Book: FM 2016: Formal Methods
Print ISBN: 978-3-319-48988-9

Electronic ISBN: 978-3-319-48989-6

Copyright Year: 2016
DOI: https://doi.org/10.1007/978-3-319-48989-6_11

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner