Predicate Transformer Semantics for Hybrid Systems

We present a semantic framework for the deductive verification of hybrid systems with Isabelle/HOL. It supports reasoning about the temporal evolutions of hybrid programs in the style of differential dynamic logic modelled by flows or invariant sets for vector fields. We introduce the semantic foundations of this framework and summarise their Isabelle formalisation as well as the resulting verification components. A series of simple examples shows our approach at work.

Verification of hybrid systems using Kaucher arithmetic

The increasing complexity of technical systems leads to increasing challenges regarding the verification of those systems. Especially in the context of safety critical systems, there is a high need for reliable verification results. Currently verification is mainly based on expert knowledge and the use of high performance hardware to investigate a very high amount of test cases. This article proposes an alternative approach using an iterating segmentation and identification algorithm that is appended by interval arithmetic calculations. This combination yields guaranteed results that do not suffer from type II failures, i. e., that will never verify an erroneous system. This is especially relevant in the context of safety critical systems.

A Benchmark for Component-based Hybrid Systems Safety Verification

At scale, formal verification of hybrid systems is challenging, but a potential remedy is the observation that systems often come with a number of natural components with certain local responsibilities. Ideally, such a compartmentalization into more manageable components also translates to hybrid systems verification, so that safety properties about the whole system can be derived from local verification results. We propose a benchmark consisting of a sequence of three case studies, where components interact to achieve system safety. The baseline for the benchmark is the verification effort from a monolithic fashion (i.e., the entire system without splitting it into components). We describe how to split the system models used in these case studies into components with local responsibilities, and what is expected about their interaction to guarantee system safety. The benchmark can be used to assess the performance, automation, and verification features of component-based verification approaches.

An Algorithmic Approach to Stability Verification of Hybrid Systems: A Summary

This paper summarizes results related to a novel algorithmic approach for verifying stability of hybrid systems. The traditional approach based on Lyapunov function search suffers from several disadvantages --- it relies on the user expertise to obtain good templates for the Lyapunov function; further, an unsuccessful attempt at instantiating the templates provides no insights into the choice of better templates. To overcome these difficulties, the algorithmic approach relies on an abstraction refinement framework which systematically searches for a proof and provides insights to the user in the event of a failure to prove stability. We summarize the new foundations, techniques and software tools that we have developed for the algorithmic approach to stability verification.