FDL TBA

Abstract:

Cyberphysical Systems (CPS), combining physical devices and software artifacts, are commonly found in many industries, in the aerospace, automotive, railway and energy sectors. Their design involve multi-disciplinary teams, working together both on the design of the physics and of the software. This requires the modeling of the dynamics of both physics and software. A major trend in industry, is to build digital twins. They are executable models of a whole system, on which a variety of analyzes and tests can be carried out, much before a prototype of the actual system can be build. Hybrid mathematical modeling languages such as Simulink, Modelica, or System-C AMS are widely used to capture both the continuous-time (physics) and the discrete-time (software) dynamics of cyber-physical systems.
However, CPS requirements are much harder to formalize, because they only provide a partial specification of the system's behavior, with the consequence that models are non-deterministic, by essence, so that the variability of the different designs can be captured in a single model. Mathematical modeling languages such as Simulink or Modelica are ill-suited to formalize requirements, for the basic reason that they can cope only with deterministic behavior.
This panel will focus on the concepts, languages and tools, with which CPS Requirements can be formalized and used for verification and testing. Several practical approaches will be compared, namely: the Modelica Requirements Library, the SpaceEx Hybrid Systems modeling and verification tool, and Verilog & System-C AMS frameworks.

Panelist:
Lena Buffoni (lena.buffoni@liu.se), Linköping University, Sweden
Goran Frehse (goran.frehse@ensta-paris.fr), ENSTA Paris, France
Franco Fummi (franco.fummi@univr.it), University of Verona, Italy
Moderator:
Benoît Caillaud (benoit.caillaud@irisa.fr), University of Rennes & INRIA, France