Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Euler’s Method Applied to the Control of Switched Systems Read chapter Read first chapter

2017 | OriginalPaper | Chapter

Time-Triggered Conversion of Guards for Reachability Analysis of Hybrid Automata

Authors : Stanley Bak, Sergiy Bogomolov, Matthias Althoff

Published in: Formal Modeling and Analysis of Timed Systems

Publisher: Springer International Publishing

Log in

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

search-config
loading …

Abstract

A promising technique for the formal verification of embedded and cyber-physical systems is flow-pipe construction, which creates a sequence of regions covering all reachable states over time. Flow-pipe construction methods can check whether specifications are met for all states, rather than just testing using a finite and incomplete set of simulation traces. A fundamental challenge when using flow-pipe construction on high-dimensional systems is the cost of geometric operations, such as intersection and convex hull. We address this challenge by showing that it is often possible to remove the need to perform high-dimensional geometric operations by combining two model transformations, direct time-triggered conversion and dynamics scaling. Further, we prove the overapproximation error in the conversion can be made arbitrarily small. Finally, we show that our transformation-based approach enables the analysis of a drivetrain system with up to 51 dimensions.

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 Conic Abstractions for Hybrid Systems
next chapter Symbolic Dependency Graphs for Model-Checking
Literature
1.
Althoff, M.: An introduction to CORA 2015. In: Proceeding of the Workshop on Applied Verification for Continuous and Hybrid Systems, pp. 120–151 (2015)
2.
Althoff, M., Krogh, B.H.: Avoiding geometric intersection operations in reachability analysis of hybrid systems. In: Hybrid Systems: Computation and Control, HSCC 2012, Beijing, China, 17–19 April 2012, pp. 45–54 (2012)
3.
Althoff, M., Le Guernic, C., Krogh, B.H.: Reachable set computation for uncertain time-varying linear systems. In: Hybrid Systems: Computation and Control, pp. 93–102 (2011)
4.
Althoff, M., Rajhans, A., Krogh, B.H., Yaldiz, S., Li, X., Pileggi, L.: Formal verification of phase-locked loops using reachability analysis and continuization. In: Proceeding of the International Conference on Computer Aided Design, pp. 659–666 (2011)
5.
Althoff, M., Stursberg, O., Buss, M.: Computing reachable sets of hybrid systems using a combination of zonotopes and polytopes. Nonlinear Anal. Hybrid Syst. 4(2), 233–249 (2010)MathSciNetCrossRefMATH
6.
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. Theoret. Comput. Sci. 138(1), 3–34 (1995)MathSciNetCrossRefMATH
7.
Bak, S.: Reducing the wrapping effect in flowpipe construction using pseudo-invariants. In: 4th ACM SIGBED International Workshop on Design, Modeling, and Evaluation of Cyber-Physical Systems (CyPhy 2014), pp. 40–43 (2014)
8.
Bak, S., Bogomolov, S., Henzinger, T.A., Johnson, T.T., Prakash, P.: Scalable static hybridization methods for analysis of nonlinear systems. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, pp. 155–164. ACM, New York (2016)
9.
Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: 18th International Conference on Hybrid Systems: Computation and Control (HSCC 2015), pp. 128–133. ACM (2015)
10.
Bak, S., Duggirala, P.S.: Direct verification of linear systems with over 10000 dimensions. In: 4th International Workshop on Applied Verification for Continuous and Hybrid Systems (2017)
11.
Bak, S., Duggirala, P.S.: Hylaa: A tool for computing simulation-equivalent reachability for linear systems. In: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, pp. 173–178. ACM (2017)
12.
Bak, S., Johnson, T.T.: Periodically-scheduled controller analysis using hybrid systems reachability and continuization. In: 36th IEEE Real-Time Systems Symposium (RTSS), San Antonio, Texas. IEEE Computer Society, December 2015
13.
Benvenuti, L., Bresolin, D., Collins, P., Ferrari, A., Geretti, L., Villa, T.: Assume-guarantee verification of nonlinear hybrid systems with ARIADNE. Int. J. Robust Nonlinear Control 24, 699–724 (2014)MathSciNetCrossRefMATH
14.
Bogomolov, S., Frehse, G., Greitschus, M., Grosu, R., Pasareanu, C., Podelski, A., Strump, T.: Assume-guarantee abstraction refinement meets hybrid systems. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 116–131. Springer, Cham (2014). doi:10.​1007/​978-3-319-13338-6_​10
15.
Bogomolov, S., Frehse, G., Grosu, R., Ladan, H., Podelski, A., Wehrle, M.: A box-based distance between regions for guiding the reachability analysis of SpaceEx. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 479–494. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-31424-7_​35 CrossRef
16.
Bogomolov, S., Mitrohin, C., Podelski, A.: Composing reachability analyses of hybrid systems for safety and stability. In: Proceeding of the 8th International Symposium on Automated Technology for Verification and Analysis, pp. 67–81 (2010)
17.
Botchkarev, O., Tripakis, S.: Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. In: Lynch, N., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 73–88. Springer, Heidelberg (2000). doi:10.​1007/​3-540-46430-1_​10 CrossRef
18.
Brihaye, T., Doyen, L., Geeraerts, G., Ouaknine, J., Raskin, J.-F., Worrell, J.: Time-bounded reachability for monotonic hybrid automata: complexity and fixed points. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 55–70. Springer, Cham (2013). doi:10.​1007/​978-3-319-02444-8_​6 CrossRef
19.
Bu, L., Li, Y., Wang, L., Chen, X., Li, X.: Bach 2: bounded reachability checker for compositional linear hybrid systems. In: Proceeding of Design, Automation & Test in Europe, pp. 1512–1517 (2010)
20.
Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-39799-8_​18 CrossRef
21.
Chen, X., Sankaranarayanan, S., Ábrahám, E.: Taylor model flowpipe construction for non-linear hybrid systems. In: Proceeding of the 33rd IEEE Real-Time Systems Symposium (2012)
22.
Chen, X., Schupp, S., Makhlouf, I.B., Ábrahám, E., Frehse, G., Kowalewski, S.: A benchmark suite for hybrid systems reachability analysis. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 408–414. Springer, Cham (2015). doi:10.​1007/​978-3-319-17524-9_​29
23.
Dang, T.: Vérification et synthèse des systèmes hybrides. PhD thesis, Institut National Polytechnique de Grenoble (2000)
24.
25.
Fränzle, M., Herde, C.: HySAT: an efficient proof engine for bounded model checking of hybrid systems. Formal Methods Syst. Des. 30(3), 179–198 (2007)CrossRefMATH
26.
27.
Frehse, G., Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22110-1_​30 CrossRef
28.
Frehse, G., Jha, S.K., Krogh, B.H.: A counterexample-guided approach to parameter synthesis for linear hybrid automata. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 187–200. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-78929-1_​14 CrossRef
29.
Frehse, G., Kateja, R., Le Guernic, C.: Flowpipe approximation and clustering in space-time. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, pp. 203–212. ACM (2013)
30.
Frehse, G., Ray, R.: Flowpipe-guard intersection for reachability computations with support functions. In: Proceeding of Analysis and Design of Hybrid Systems, pp. 94–101 (2012)
31.
Ghorbal, K., Goubault, E., Putot, S.: A logical product approach to zonotope intersection. In: Proceeding of the 27th International Conference on Computer Aided Verification, pp. 212–226 (2010)
32.
Girard, A., Le Guernic, C.: Efficient reachability analysis for linear systems using support functions. In: Proceeding of the 17th IFAC World Congress, pp. 8966–8971 (2008)
33.
Girard, A., Guernic, C.: Zonotope/Hyperplane intersection for hybrid systems reachability analysis. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 215–228. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-78929-1_​16 CrossRef
34.
Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HYTECH: the next generation. In: Proceeding. of the 16th IEEE Real-Time Systems Symposium, pp. 56–65 (1995)
35.
Immler, F.: A verified algorithm for geometric zonotope/hyperplane intersection. In: Proceeding of the Conference on Certified Programs and Proofs, pp. 129–136 (2015)
36.
Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \(\delta \)-reachability analysis for hybrid systems. In: Proceeding of Tools and Algorithms for the Construction and Analysis of Systems, pp. 200–205 (2015)
37.
Kurzhanski, A., Varaiya, P.: Ellipsoidal techniques for hybrid dynamics: the reachability problem. In: Dayawansa, W.P., Lindquist, A., Zhou, Y. (eds.) New Directions and Applications in Control Theory, vol. 321, pp. 193–205. Springer, Heidelberg (2005). doi:10.​1007/​10984413_​12 CrossRef
38.
Lagerberg, A.: A benchmark on hybrid control of an automotive powertrain with backlash. Technical report R005/2007, Signals and Systems, Chalmers University of Technology (2007)
39.
Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Syst. 4(2), 250–262 (2010)MathSciNetCrossRefMATH
40.
Maïga, M., Ramdani, N., Travé-Massuyès, L., Combastel, C.: A CSP versus a zonotope-based method for solving guard set intersection in nonlinear hybrid reachability. Math. Comput. Sci. 8, 407–423 (2014)MathSciNetCrossRefMATH
41.
Mitchell, I.M., Susuki, Y.: Level set methods for computing reachable sets of hybrid systems with differential algebraic equation dynamics. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 630–633. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-78929-1_​51 CrossRef
42.
43.
44.
Ramdani, N., Nedialkov, N.S.: Computing reachable sets for uncertain nonlinear hybrid systems using interval constraint-propagation techniques. Nonlinear Anal. Hybrid Syst. 5(2), 149–162 (2010)MathSciNetCrossRefMATH
45.
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: Proceeding of the Fifth Workshop on Design, Modeling and Evaluation of Cyber Physical Systems, pp. 8–24 (2015)
46.
Smirnov, G.V.: Introduction to the Theory of Differential Inclusions. American Mathematical Society (2002)
Metadata
Title
Time-Triggered Conversion of Guards for Reachability Analysis of Hybrid Automata
Authors
Stanley Bak
Sergiy Bogomolov
Matthias Althoff
Copyright Year
2017
Book
Formal Modeling and Analysis of Timed Systems

Print ISBN: 978-3-319-65764-6

Electronic ISBN: 978-3-319-65765-3

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-319-65765-3_8

Premium Partner

    Image Credits