Abstract
We have developed a hybrid system safety prover, implemented in Coq using the abstraction method introduced by [2]. The development includes: a formalisation of the structure of hybrid systems; a framework for the construction of an abstract system (consisting of decidable “over-estimators” of abstract transitions and initiality) faithfully representing a concrete hybrid system; a translation of abstract systems to graphs, enabling the decision of abstract state reachability using a certified graph reachability algorithm; a proof of the safety of an example hybrid system generated using this tool stack. To produce fully certified safety proofs without relying on floating point computations, the development critically relies on the computable real number implementation of the CoRN library of constructive mathematics formalised in Coq. The development also features a nice interplay between constructive and classical logic via the double negation monad.
This research was supported by the BRICKS/FOCUS project 642.000.501, Advancing the Real use of Proof Assistants.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ábrahám-Mumm, E., Hannemann, U., Steffen, M.: Assertion-based analysis of hybrid systems with PVS. In: Moreno-Díaz Jr., R., Buchberger, B., Freire, J.-L. (eds.) EUROCAST 2001. LNCS, vol. 2178, pp. 94–109. Springer, Heidelberg (2001)
Alur, R., Dang, T., Ivančić, F.: Predicate abstraction for reachability analysis of hybrid systems. ACM Trans. Embedded Comput. Syst. 5, 152–199 (2006)
Bagnara, R., Hill, P., Zaffanella, E.: The parma polyhedra library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1-2), 3–21 (2008)
Bjørner, N., Manna, Z., Sipma, H., Uribe, T.: Deductive verification of real-time systems using STeP. Theor. Comput. Sci. 253(1), 27–60 (2001)
Chutinan, A., Krogh, B.: Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 76–90. Springer, Heidelberg (1999)
Clarke, E., Fehnker, A., Han, Z., Krogh, B., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. J. Found. Comput. Sci. 14(4), 583–604 (2003)
Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the constructive Coq repository at Nijmegen. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 88–103. Springer, Heidelberg (2004)
Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005)
Henzinger, T.: The theory of hybrid automata. pp. 278–292 (1996)
Henzinger, T., Rusu, V.: Reachability verification for hybrid automata. In: Henzinger, T.A., Sastry, S.S. (eds.) HSCC 1998. LNCS, vol. 1386, pp. 190–204. Springer, Heidelberg (1998)
Lynch, N., Segala, R., Vaandrager, F.: Hybrid I/O automata. Inf. Comput. 185(1), 105–157 (2003)
Manna, Z., Sipma, H.: Deductive verification of hybrid systems using STeP. In: Henzinger, T.A., Sastry, S.S. (eds.) HSCC 1998. LNCS, vol. 1386, pp. 305–318. Springer, Heidelberg (1998)
The MathWorks. MATLAB, http://www.mathworks.com/products/matlab/
O’Connor, R.: Certified exact transcendental real number computation in Coq. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 246–261. Springer, Heidelberg (2008)
Pappas, G.: Hybrid system tools, http://wiki.grasp.upenn.edu/hst/
Platzer, A., Quesel, J.-D.: Keymaera: A hybrid theorem prover for hybrid systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171–178. Springer, Heidelberg (2008)
Preußig, J., Kowalewski, S., Wong-Toi, H., Henzinger, T.: An algorithm for the approximative analysis of rectangular automata. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 228–240. Springer, Heidelberg (1998)
Ratschan, S.: Efficient solving of quantified inequality constraints over the real numbers. ACM Transactions on Computational Logic 7(4), 723–748 (2006)
Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Transactions in Embedded Computing Systems 6(1) (2007)
Stursberg, O., Kowalewski, S., Hoffmann, I., Preußig, J.: Comparing timed and hybrid automata as approximations of continuous systems. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1996. LNCS, vol. 1273, pp. 361–377. Springer, Heidelberg (1997)
Wadler, P.: Monads for functional programming. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol. 925, pp. 24–52. Springer, Heidelberg (1995)
van der Weegen, E.: Automated machine-checked hybrid system safety proofs, an implementation of the abstraction method in Coq. Technical report, Radboud University Nijmegen (2009), http://www.eelis.net/research/hybrid/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Geuvers, H., Koprowski, A., Synek, D., van der Weegen, E. (2010). Automated Machine-Checked Hybrid System Safety Proofs. In: Kaufmann, M., Paulson, L.C. (eds) Interactive Theorem Proving. ITP 2010. Lecture Notes in Computer Science, vol 6172. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14052-5_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-14052-5_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14051-8
Online ISBN: 978-3-642-14052-5
eBook Packages: Computer ScienceComputer Science (R0)