Home      Log In      Contacts      FAQs      INSTICC Portal


The role of the tutorials is to provide a platform for a more intensive scientific exchange amongst researchers interested in a particular topic and as a meeting point for the community. Tutorials complement the depth-oriented technical sessions by providing participants with broad overviews of emerging fields. A tutorial can be scheduled for 1.5 or 3 hours.

Tutorial proposals are accepted until:

March 20, 2019

If you wish to propose a new Tutorial please kindly fill out and submit this Expression of Interest form.


Simulation and Verification of Cyber-physical Systems


Hermann Kaindl
Vienna University of Technology
Brief Bio
Hermann Kaindl joined the Vienna University of Technology in early 2003 as a full professor. In the same year, he was elected as a member of the University Senate. Prior to moving to academia, he was a senior consultant with the division of program and systems engineering at Siemens AG Austria. There he has gained more than 24 years of industrial experience in software development. His current research interests include software and systems engineering focusing on requirements engineering and architecting, and human-computer interaction as it relates to interaction design and automated generation of user interfaces. He has published 5 books and more than 220 refereed papers in journals, books and conference proceedings. He is a Senior Member of the IEEE, a Distinguished Scientist member of the ACM and a member of the AAAI, and is on the executive board of the Austrian Society for Artificial Intelligence.

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. In addition, 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). Based on this research, this tutorial also shows that and how formal verification of (safety-critical) CPS can be made in addition to simulations.


Affine Arithmetic Forms, model checking, Fluent Calculus

Aims and Learning Objectives

This tutorial has the primary objective to provide the participants with a better understanding of simulation, both traditionally and using AAF, and of the difference to formal verification.

Target Audience

The target audience is practitioners, students and educators.

Prerequisite Knowledge of Audience

Attendees are supposed to have some basic familiarity with simulation. But they do not need to know already about formal verification, which will be introduced in this tutorial intuitively.

Detailed Outline

5min Introduction
20min Background
- Traditional Simulation
- Semi-symbolic Simulation using Affine Arithmetic Forms
- Formal Verification

30min Simulation of Physical Feature Interaction
- Modeling of Cyber-physical Systems (CPS)
- Simulation Approach
- Simulation and Visualization of Results

40min Semi-symbolic Simulation and Analysis
- Modeling using Affine Arithmetic Forms
- Connecting Based on Semantic Task Specification
- Minimum Coordinator Block
- Semi-symbolic Simulation
- Analyses

40min Minimalist Qualitative Models for Model Checking
- Modeling Approach
- Qualitative Model
- Model Checking Results

40min Verification of Feature Coordination Using the Fluent Calculus
- Modeling in the Fluent Calculus
- Verification Based on the Fluent Calculus
- Contrasting With Model Checking

5min Summary and Conclusion

Secretariat Contacts
e-mail: enase.secretariat@insticc.org