Seminar Room 2, ground floor (Building IMAG)
17 December 2018 - 14h00
Formal Verification of Cyber-Physical Systems in the Industrial Model-Based Design Process (Phd Defense)
by NIKOLAOS KEKATOS from Verimag Laboratory, University of Grenoble Alpes
Abstract: Cyber-Physical Systems form a class of complex, large-scale systems of frequently safety-critical nature. Formal verification approaches can provide performance and safety guarantees for these systems. They require two elements, a formal model and a set of formal specifications. However, industrial models are typically non-formal, they are analyzed in non-formal simulation environments, and their specifications are described in non-formal natural language. In this thesis, we aim to facilitate the integration of formal verification into the industrial model-based design process.
Our first key contribution is a model transformation methodology. Starting with a standard simulation model, we transform it into an equivalent verification model, a network of hybrid automata. The transformation process addresses differences in syntax, semantics, and other aspects of modeling. For this class of formal models, so-called reachability algorithms can be applied to verify safety properties. An obstacle is that scalable algorithms exist for piecewise affine (PWA) models, but not for nonlinear ones. To obtain PWA over-approximations of nonlinear dynamics, we propose a compositional syntactic hybridization technique. The result is a highly compact model that retains the modular structure of the original simulation model and largely avoids an explosion in the number of partitions.
The second key contribution is an approach to encode rich formal specifications so that they can be interpreted by tools for reachability. Herein, we consider specifications expressed by pattern templates since they are close to natural language and can be easily understood by non-expert users. We provide (i) formal definitions for select patterns that respect the semantics of hybrid automata, and (ii) monitors which encode the properties as the reachability of an error state. By composing these monitors with the formal model under study, the properties can be checked by off-the-shelf fully automated verification tools.
Furthermore, we provide a semi-automated toolchain and present results from case studies conducted in collaboration with industrial partners.
Monsieur Goran FREHSE Professeur, ENSTA ParisTech - U2IS, Directeur de thèse
Madame Thao DANG Directrice de Recherche, CNRS - Verimag, Co-Directrice de thèse
Monsieur Benoît CAILLAUD Directeur de Recherche, Inria Rennes, IRISA, Rapporteur
Monsieur Laurent FRIBOURG Directeur de Recherche, LSV - ENS Cachan, CNRS, Rapporteur
Monsieur Alexandre CHAPOUTOT Professeur, ENSTA ParisTech - U2IS, Examinateur
