Numerically-aided deductive safety proof for a powertrain control system.

*(English)*Zbl 1351.68150
Bogomolov, Sergiy (ed.) et al., Selected papers based on the presentations at the 7th and 8th international workshops on numerical software verification (NSV), Vienna, Austria, July 17–18, 2014 and April 13, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 317, 19-25 (2015).

Summary: The use of deductive techniques, such as theorem provers, has several advantages in safety verification of hybrid systems. There is often a gap, however, between the type of assistance that a theorem prover requires to make progress on a proof task and the assistance that a system designer is able to provide. To address this deficiency we present an extension to the deductive verification framework of differential dynamic logic that allows the theorem prover KeYmaera to locally reason about behaviors by leveraging forward invariant sets provided by external methods, such as numerical techniques and designer insights. Our key contribution is a new inference rule, the forward invariant cut rule, introduced into the proof calculus of KeYmaera. We demonstrate the cut rule in action on an example involving an automotive powertrain control systems, in which we make use of a simulation-driven numerical technique to compute a local barrier function.

For the entire collection see [Zbl 1325.68012].

For the entire collection see [Zbl 1325.68012].

##### MSC:

68Q60 | Specification and verification (program logics, model checking, etc.) |

68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |

93C30 | Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) |

PDF
BibTeX
XML
Cite

\textit{N. Aréchiga} et al., Electron. Notes Theor. Comput. Sci. 317, 19--25 (2015; Zbl 1351.68150)

Full Text:
DOI

##### References:

[1] | Beckert, Bernhard; Hähnle, Reiner; Schmitt, Peter H., Verification of object-oriented software: the key approach, (2007), Springer-Verlag · Zbl 1202.68092 |

[2] | Chen, Xin; Abraham, Erika; Sankaranarayanan, Sriram, Flow*: an analyzer for non-linear hybrid systems, (CAV, (2013)) |

[3] | Frehse, Goran, Phaver: algorithmic verification of hybrid systems past hytech, STTT, 10, 3, 263-279, (2008) · Zbl 1078.93533 |

[4] | Frehse, Goran; Le Guernic, Colas; Donzé, Alexandre; Cotton, Scott; Ray, Rajarshi; Lebeltel, Olivier; Ripado, Rodolfo; Girard, Antoine; Dang, Thao; Maler, Oded, Spaceex: scalable verification of hybrid systems, (CAV, (2011)), 379-395 |

[5] | Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M., δ-complete decision procedures for satisfiability over the reals, (J. Automated Reasoning, (2012)), 286-300 · Zbl 1358.03028 |

[6] | Henzinger, Thomas A.; Kopke, Peter W.; Puri, Anuj; Varaiya, Pravin, What’s decidable about hybrid automata?, JCSS, 57, 1, 94-124, (1998) · Zbl 0920.68091 |

[7] | Jin, Xiaoqing; Deshmukh, Jyotirmoy V.; Kapinski, James; Ueda, Koichi; Butts, Ken, Powertrain control verification benchmark, (Hybrid Systems: Computation and Control, (2014)) · Zbl 1362.93070 |

[8] | Kapinski, James; Deshmukh, Jyotirmoy V.; Sankaranarayanan, Sriram; Aréchiga, Nikos, Simulation-guided Lyapunov analysis for hybrid dynamical systems, (Hybrid Systems: Computation and Control, (2014)) · Zbl 1362.93108 |

[9] | Kapinski, James; Krogh, Bruce H., Verifying asymptotic bounds for discrete-time sliding mode systems with disturbance inputs, (ACC, (2004)), 2852-2857 |

[10] | Platzer, André, Logical analysis of hybrid systems, (2010), Springer · Zbl 1287.03075 |

[11] | Prajna, Stephen, Optimization-based methods for nonlinear and hybrid systems verification, (2005), California Institute of Technology, Caltech Pasadena, CA, USA, PhD thesis · Zbl 1078.93507 |

[12] | Topcu, U.; Seiler, P.; Packard, A., Local stability analysis using simulations and sum-of-squares programming, Automatica, 44, 2669-2675, (2008) · Zbl 1155.93417 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.