Below is a list and a short description of the tutorials offered at the CPS Summer School.
This tutorial provides an introduction to the VDM Real Time dialect supported by the open-source tool called Overture. This will also demonstrate to the participants how VDM models can be exported as FMUs that can be used for co-simulations inside the INTO-CPS tool chain.
Speakers: Peter Gorm Larsen (Aarhus University), Ken Pierce (Newcastle University).
The tutorial introduces the fundamental concepts of the Modelica language. Modelica is a non-proprietary, object-oriented, equation based language for multi-domain modelling of complex physical systems containing, e.g., mechanical, electrical, thermal, or control subcomponents. The open-source OpenModelica tool will be used for working at the hands-on exercises. Please download and install OpenModelica (https://openmodelica.org/) on your laptop for following the exercises. Besides fundamental Modelica concepts the tutorial will cover FMI generation from OpenModelica for the INTO-CPS tool chain.
Speaker: Bernhard Thiele (Linköping University).
In this tutorial we will give a short introduction of the software 20-sim. We will teach you how to model and simulate computer controlled continuous time systems with 20-sim and use the FMI interface to couple 20-sim to other tools for co-simulation and HIL simulation. Bring your own laptop because 80% of the course is hands on work with the software.
Speaker: Christian Kleijn (Controllab Products).
The tutorial will consist in a short introduction of Modelio tool and a tutorial for Cyber Physical architectural design by using the INTOCPS-SysML profile defined during the project.
Speakers: Etienne Brosse (Softeam) and Richard Payne (Newcastle University).
Eclipse 4diac provides a modelling tool for the industrial automation modelling language IEC 61499. This language allows to model advanced control applications which can then be deployed on networked industrial control devices (e.g., PLCs). This tutorial gives an overview on the modelling language IEC 61499 and how Eclipse 4diac can be used to develop applications with it and how to test them with virtual devices against simulated plants in a Co-Simulation Environment.
This tutorial covers workflows for model-based CPS design that are enabled by the INTO-CPS technologies. This includes workflows where systems are developed from scratch, as well as workflows that can be adapted to existing practice. Particular attention is paid to important scenarios identified through industrial surveys, including use of legacy models and impact analysis.
Speaker: Ken Pierce (Newcastle University).
In this tutorial, we will explore our mechanisation of the UTP semantic framework in Isabelle/HOL, which provides the theoretical foundations of the INTO-CPS tool chain. In the first session, we begin with a hands-on introduction of our mechanised framework and proof tool Isabelle/UTP, showing how to prove simple logical properties about programs using algebraic laws, Hoare logic, and the weakest-precondition calculus. We will also demonstrate the use of CSP & Circus, and exemplify this with an encoding of an FMI system and model. In the second session, we will go into more detail about the foundations of Isabelle/UTP, including its lens-based state-space model and our theory of generalised reactive processes. We will also give an overview here of how differential equations can be encoded in the Isabelle tool. We will conclude by looking at our theory of hybrid relations, which is being used to give a semantics to Modelica, and demonstrate some examples of hybrid programs.
Speakers: Frank Zeyda (University of York) and Simon Foster (University of York).
In this tutorial we will explore the design of multi-parameter experiments in CPS using Design Space Exploration (DSE). We will guide participants through the process of designing experiments in SysML, though to launching DSE experiments and understanding trade-offs.
Speaker: Carl Gamble (Newcastle University).
We present the technical foundations of automated model-based testing and discuss experiences with the application of model-based testing using RT-Tester to avionics software components.
Speaker: Jörg Brauer (Verified Systems International).
The tutorial will provide an overview of traceably and provenance, and motivate the need for recording design decisions and trace links in the CPS design process. The tutorial will present traceability applies to the different activities in modelling and simulation with the INTO-CPS tool chain.
Speakers: Carl Gamble (Newcastle University) and Christian Koenig (TWT GmbH).
In this presentation we will highlight best practice methods for safety assessment of complex systems from aerospace and automotive and adapt them for application in maritime domain. The focus will be on methods for identification of hazards as well as following fault/failure propagation to identify basic faults. From this we develop an approach for a manageable and easy to use, yet thorough safety assessment procedure and present its application to a maritime cyber-physical system for collision avoidance.
Speaker: Sebastian Vander Maelen (Offis, Germany).
The tutorial will review recent developments in SMT-based verification of CPS. In particular, we will cover different modeling approaches based on SysML and hybrid automata and their encoding using symbolic formulas. We will show how to formalize typical requirements using Linear-time Temporal Logic (LTL). We will then give an overview of different SMT-based techniques to verify LTL properties. Finally, we will sketch how these techniques can be used for validating the properties and performing compositional reasoning.
Speakers: Jörg Brauer (Verified Systems International) and Stefano Tonetta (FBK).
Cyber Physical Systems (CPS) integrate physical, software, and network aspects. A unifying theory, systematic design methods, techniques and tools are needed to tackle CPS complexity. As a solution, Multi-paradigm Modelling (MPM) proposes to model every part and aspect of a system explicitly, at the most appropriate level(s) of abstraction, using the most appropriate modelling formalism(s). Modelling language engineering, including model transformation, and the study of language semantics, are used to realize MPM.
Causes of CPS complexity will be identified, followed by an introduction to (domain-specific) modelling language engineering. (Co-) simulation principles and techniques will be used to give operational semantics to possibly heterogeneous modelling languages.
Speaker: Hans Vangheluwe (University of Antwerp).