Improving the SAT modulo ODE approach to hybrid systems analysis by combining different enclosure methods

详细信息    查看全文

• 作者：Andreas Eggers (1)
  Nacim Ramdani (2)
  Nedialko S. Nedialkov (3)
  Martin Fr盲nzle (1)
  
  1. Department of Computing Science ; Carl von Ossietzky Universit盲t ; 26111 ; Oldenburg ; Germany
  2. Universit茅 d鈥橭rl茅ans ; PRISME ; 63 av. de Lattre de Tassigny ; 18020 ; Bourges ; France
  3. McMaster University ; Hamilton ; ON ; Canada
  
• 关键词：Analysis of hybrid discrete ; continuous systems ; Satisfiability modulo theories ; Enclosure methods for ODEs ; Bracketing systems
• 刊名：Software and Systems Modeling
• 出版年：2015
• 出版时间：February 2015
• 年：2015
• 卷：14
• 期：1
• 页码：121-148
• 全文大小：2,757 KB
• 参考文献：1. Berz, M.: COSY INFINITY version 8 reference manual. Tech. Rep. MSUCL-1088, National Superconducting Cyclotron Laboratory, Michigan State University, USA (1997)
  2. Clarke, E.M., Fehnker, A., Han, Z., Krogh, B.H., Stursberg, O., Theobald, M.: Verification of hybrid systems based on counterexample-guided abstraction refinement. In: Gravel, H., Hatcliff, J. (eds.) TACAS, Lecture Notes in Computer Science vol 2619, pp. 192鈥?07. Springer, Berlin (2003)
  3. Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201鈥?15 (1960) CrossRef
  4. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun. ACM 5, 394鈥?97 (1962) CrossRef
  5. Eggers, A., Fr盲nzle, M., Herde, C.: SAT modulo ODE: a direct SAT approach to hybrid systems. In: ATVA, LNCS, vol. 5311, pp. 171鈥?85. Springer, New York (2008)
  6. Eggers, A., Ramdani, N., Nedialkov, NS., Fr盲nzle, M.: Improving SAT modulo ODE for hybrid systems analysis by combining different enclosure methods. In: Barthe, G., Pardo, A., Schneider, G. (eds.) Proceedings of the Ninth International Conference on Software Engineering and Formal Methods (SEFM), LNCS, vol. 7041, pp. 172鈥?87. Springer, Berlin (2011). doi:10.1007/978-3-642-24690-6-13
  7. Fousse, L., Hanrot, G., Lef猫vre, V., P茅lissier, P., Zimmermann, P.: MPFR: a multiple-precision binary floating-point library with correct rounding. ACM Trans. Math. Softw. 33(2) (2007). doi:10.1145/1236463.1236468 , MPFR is available at http://www.mpfr.org/
  8. Fr盲nzle, M., Herde, C., Ratschan, S., Schubert, T., Teige, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. JSAT 1(3鈥?), 209鈥?36 (2007)
  9. Goldsztejn, A., Mullier, O., Eveillard, D., Hosobe, H.: Including ordinary differential equations based constraints in the standard CP framework. In: Cohen, D. (ed.) Principles and Practice of Constraint Programming鈥擟P 2010, LNCS, vol. 6308, pp. 221鈥?35. Springer, Berlin (2010) CrossRef
  10. Henzinger, T., Horowitz, B., Majumdar, R., Wong-Toi, H.: Beyond HyTech: hybrid systems analysis using interval numerical methods. In: Lynch, N., Krogh, B. (eds.) Hybrid Systems: Computation and Control, LNCS, vol. 1790, pp. 130鈥?44. Springer, New York (2000)
  11. Ishii, D., Ueda, K., Hosobe, H.: An interval-based SAT modulo ODE solver for model checking nonlinear hybrid systems. Int. J. Softw. Tools Technol. Transf. (STTT), 1鈥?3 (2011). doi:10.1007/s10009-011-0193-y
  12. Kieffer, M., Walter, E., Simeonov, I.: Guaranteed nonlinear parameter estimation for continuous-time dynamical models. In: Proceedings 14th IFAC Symposium on System Identification, Newcastle, pp. 843鈥?48 (2006)
  13. Lerch, M., Tischler, G., Gudenberg, J.W.V., Hofschuster, W., Kr盲mer, W. Filib++, a fast interval library supporting containment computations. ACM Trans. Math. Softw. 32(2):299鈥?24 (2006). doi:10.1145/1141885.1141893 , FILIB++ is available at oftware/filib.html" class="a-plus-plus">http://www2.math.uni-wuppertal.de/~xsc/software/filib.html
  14. Lygeros, J., Johansson, K., Simic, S., Zhang, J., Sastry, S.: Dynamical properties of hybrid automata. IEEE Trans. Autom. Control 48(1), 2鈥?7 (2003). doi:10.1109/TAC.2002.806650
  15. M眉ller, M.: 脺ber das Fundamentaltheorem in der Theorie der gew枚hnlichen Differentialgleichungen. Mathematische Zeitschrift 26, 619鈥?45 (1927) CrossRef
  16. Nedialkov, N.S.: Computing rigorous bounds on the solution of an initial value problem for an ordinary differential equation. PhD thesis, Department of Computer Science, University of Toronto, Toronto, M5S 3G4 (1999)
  17. Nedialkov, N.S.: VNODE-LP鈥攁 validated solver for initial value problems in ordinary differential equations. Tech. Rep. CAS-06-06-NN. Department of Computing and Software, McMaster University, Hamilton, L8S 4K1, VNODE-LP is available at http://www.cas.mcmaster.ca/~nedialk/vnodelp (2006)
  18. Nedialkov, N.S.: Implementing a rigorous ODE solver through literate programming. In: Rauh, A., Auer, E. (eds.) Modeling, Design, and Simulation of Systems with Uncertainties. Mathematical Engineering, vol. 3, pp. 3鈥?9. Springer, New York (2011). doi:10.1007/978-3-642-15956-5_1
  19. Podelski, A., Wagner, S.: Region stability proofs for hybrid systems. In: Raskin, J.F., Thiagarajan, P.S. (eds.) FORMATS, LNCS, vol. 4763, pp. 320鈥?35. Springer, Berlin (2007)
  20. Ramdani, N., Meslem, N., Candau, Y.: A hybrid bounding method for computing an over-approximation for the reachable space of uncertain nonlinear systems. IEEE Trans. Autom. Control 54(10), 2352鈥?364 (2009) CrossRef
  21. Ramdani, N., Meslem, N., Candau, Y.: Computing reachable sets for uncertain nonlinear monotone systems. Nonlinear Anal. Hybrid Syst. 4(2), 263鈥?78 (2010) CrossRef
  22. Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Trans. Embed. Comput. Syst. 6(1), (2007)
  23. Shtrichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E., Sistla, A. (eds.) Computer Aided Verification, LNCS, vol. 1855, pp. 480鈥?94. Springer, Berlin (2000). doi:10.1007/10722167_36
  24. Stauning, O.: Automatic validation of numerical solutions. PhD thesis, Technical University of Denmark, Lyngby, (1997). http://www2.imm.dtu.dk/documents/ftp/phdliste/phd36_97.ps, FADBAD++ is available at http://www.fadbad.com
  25. Stursberg, O., Kowalewski, S., Hoffmann, I., Preu脽ig, J.: Comparing timed and hybrid automata as approximations of continuous systems. In: Antsakalis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) Hybrid Systems IV, LNCS, vol. 1273, pp. 361鈥?77. Springer, Berlin (1997). doi:10.1007/bfb0031569
  
• 刊物类别：Computer Science
• 刊物主题：Software Engineering, Programming and Operating Systems
  Programming Techniques
  Software Engineering
  Programming Languages, Compilers and Interpreters
  Information Systems Applications and The Internet
  Business Information Systems
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1619-1374

文摘

Aiming at automatic verification and analysis techniques for hybrid discrete-continuous systems, we present a novel combination of enclosure methods for ordinary differential equations (ODEs) with the iSAT solver for large Boolean combinations of arithmetic constraints. Improving on our previous work, the contribution of this paper lies in combining iSAT with VNODE-LP, as a state-of-the-art interval solver for ODEs, and with bracketing systems, which exploit monotonicity properties allowing to find enclosures for problems that VNODE-LP alone cannot enclose tightly. We apply the combined iSAT-ODE solver to the analysis of a variety of non-linear hybrid systems by solving predicative encodings of reachability properties and of an inductive stability argument, and evaluate the impact of the different enclosure methods, decision heuristics and their combination. Our experiments include classic benchmarks from the literature, as well as a newly-designed conveyor belt system that combines hybrid behavior of parallel components, a slip-stick friction model with non-linear dynamics and flow invariants and several dimensions of parameterization. In the paper, we also present and evaluate an extension of VNODE-LP tailored to its use as a deduction mechanism within iSAT-ODE, to allow fast re-evaluations of enclosures over arbitrary subranges of the analyzed time span.