T1: Simulation and Verification of Cyber-Physical Systems


Date
July 27 (Monday)
Period
9:00 am - 12:00 pm (Half-day)

Abstract


This tutorial has the primary objective to provide the participants with a better understanding of simulation, both traditionally and using Affine Arithmetic Forms (AAF), and of verification of Cyber-physical Systems (CPS). It presents our investigation of (safety-critical) feature interactions and their coordination in automotive systems using traditional simulation, and our corresponding semi-symbolic AAF model of a CPS and its simulation. For formal verification, this tutorial shows minimalist qualitative models for model checking (safety-critical) CPS feature coordination and, that a specification of a software coordinator can be formally verified using the Fluent Calculus (a derivative of the Situation Calculus), when combined with additional models.

Description


Automotive systems, for instance, are safety-critical cyber-physical systems (CPS). In particular, undesired feature interaction can lead to safety-critical behavior. In order to address this problem, we investigated physical feature interaction in this context using simulation (with more than one physical variable). This allowed us to visualize both the behavior of features in isolation and their interaction.

For studying the effects of deviations for uncertain inputs of systems, often multi-run simulation is employed, which is time-consuming. Unfortunately, such simulations also do not directly support the traceability of such effects. A semi-symbolic modeling approach based on Affine Arithmetic Forms (AAF) allows the representation of uncertainty in terms of ranges. Simulations of such models directly include propagation of deviations and their traceability. We studied such a semi-symbolic model of a CPS, including coordination of safety-critical and interacting features. For feature coordination, this model introduces handling discrete uncertainty with two different behavioral modes and their integration.

Based on this research, this tutorial has the primary objective to provide the participants with a better understanding of simulation, both traditionally and using AAF.

We investigated coordination of physical feature interactions using model checking. In particular, we created and used a qualitative model for formal verification against a property in time logic. This model is intended to be minimalist, in particular the logical model based on a physical model (including speed and distance). This logical model defines the essence of operations in the dedicated environment. We also investigated formal verification of a specification of a software coordinator using the Fluent Calculus (a derivative of the Situation Calculus).

This tutorial presents a recently proposed workflow for systematic top-down design of models of a CPS. This workflow includes systematic abstraction and refinement techniques in the context of verification through model checking, and validation in the sense that a refined model is checked for its fit with reality.

Based on this research, this tutorial also shows that and how formal verification of (safety-critical) CPS can be made in addition to simulations.

Tutorial Format


Time is spent at the start of the tutorial to understand participants’ motivation and background so as to weave in their cultural and organizational context into the tutorial. Attendee contributions and discussion are purposefully encouraged, developed and managed throughout rather than at the end of different sections.The tutorial is given in the form of presentations (PowerPoint) and discussions.

Target Audiences


This tutorial is targeted to both researchers and practitioners interested in simulation and formal verification for ensuring reliability of systems.

Most of the underlying theory will be explained intuitively right at the start, but some basic understanding of mathematics and, ideally, also logic by the participants will be good to have.

Related References


The content of the proposed tutorial is partly based on or related to the following papers:

Speaker


Hermann Kaindl's avatar
Hermann Kaindl

Institute of Computer Technology, Technische Universität Wien


Hermann Kaindl is a full professor, the director of the Institute of Computer Technology and a member of the senate at TU Wien. Prior to moving to academia in early 2003, he has gained nearly 25 years of industrial experience at Siemens Austria. Kaindl is a Senior Member of the IEEE and a Distinguished Scientist Member of the ACM. He has previously held more than 50 tutorials.