Motivation
Academic research and industry are currently witnessing two major revolutions: Cyber-Physical Systems (CPS) and the Internet of Things(IoT). The present proposal is at the heart of the former, while being also influenced by the latter. Not surprisingly, the impact of the Big Datarevolution is not confined to the internet, social networks or online market, but also impacts CPS: systems have grown in size and their complexity has reached new peaks, to the extent that acquiring a complete knowledge about a system, and modeling it, down to its most precise details, seem unrealistic.Moreover, the engineering of large software systems, as seen in Cloud Computing and Web Services, tend to favor agile software design methods. In the end, this has the following consequence: many engineers believe that systems become too complex to be modeled in a faithfully, and this vision also seems to affect CPS.
The MODELISCALE project exactly defends the opposite idea. We believe in the benefits of modeling, but acknowledge that the communities of researchers and tool developers are in part responsible for this defiance. The steep increase in the complexity of systems (e.g., public transportation systems, electric power grids) and of their models comes from composing smaller subsystems into complex architectures. As a matter of fact, these architectures are sparse, and subsystems interactions are confined to immediate neighborhoods. Thus, the dimension (number of state variables) of a system is not the most appropriate characterization of its complexity. It is rather the structure of a system and its combinatorics of modes of operation that encapsulate its complexity.
The main objective of MODELISCALE is to advance modeling technologies (languages, compile-time analyses, simulation techniques) for CPS combining physical interactions, communication layers and software components. We believe that mastering CPS comprising thousands to millions of components requires radical changes of paradigms. For instance, modeling techniques must be revised, especially when physics is involved. Modeling languages must be enhanced to cope with larger models. This can only be done by combining new compilation techniques (to master the structural complexity of models) with new mathematical tools (new numerical methods, in particular). We identify below the different axis we want to tackle.
Modelica
Modelica is a component-based modeling language initially designed for the modeling of multi-physics systems. The mathematical paradigm underlying Modelica, known as Differential Algebraic Equations (DAE). The key challenge is to be able to combine algebraic constraints, resulting from the laws of physics, in interaction with the nonsmooth behavior of some physical phenomena (e.g., impact laws), the multiple modes of operation of the system, and the intrinsically discrete behavior of software components.In essence, Modelica is based on the concept of multi-mode DAE, so that models can switch from one behavior to another when an event occurs, typically the crossing of a threshold. This approach is paramount to the modeling of large CPS. Such large models turn out to be intractable with state-of-the-art Modelica tools: because Modelica compilation techniques are not modular, whole models have to be compiled as one unit, resulting in a very large simulation code. Parallel simulation of Modelica models is still in its infancy and gives poor results on very large models and parallel/distributed techniques for networks of FMU components are not applicable to a monolithic model .Moreover, when simulating, for instance, thermal models of a building, the opening of a window or of a door impacts the whole simulation, despite it only has a local impact on the heat exchanges and temperatures. This is caused by the sudden change of stiffness in some part of the model, that forces a change in discretization step size (assuming that a variable step solver is used for simulation), with the adverse effect that the simulation of the whole system is slowed down. The root cause of this phenomenon boils down to the fact that system models and numerical methods used to simulate them are not space adaptive — recall that such models are 0-D models, with ODEs/DAEs, with no Partial Differential Equations (PDEs).
In MODELISCALE, we will explore new modular compilation methods and distributed simulation techniques for Simulink-/Modelica-like hybrid systems modelers, with the objective of improving the scalability of models and simulations.
Co-modeling and co-simulation
The emergence of the FMI standard supporting co-modeling and co-simulation has contributed to the widespread belief that the co-simulation of a large number of models is achievable using FMI-based tools. This is unfortunately an illusion, as FMI does not guarantee the reproducibility and determinacy of simulations. There are several reasons for that. Until very recently, FMI offered no rollback mechanism, which makes the co-simulation to depend on the discretization policy. Second, as the standard is not formally specified, its various implementations by tool developers differ.
We are convinced that we will be able to define new notions of interfaces to multi-mode DAE systems, better suited to the distributed co-simulation of large models and contribute to the evolution of the FMI standard.
Beyond simulation
Many physical science engineers (mechanical, electrical, aeronautic, …) develop models with the sole objective to simulate them, while it is known that models can be used for a variety of tasks, all contributing towards the safe design and operation of a CPS: validating a design model against a set of requirements, assess the robustness of a model, test implementations against a design model, perform state estimation during system operation, just to name a few.
Early stages of CPS design usually consist in the elicitation of system-level requirements that will be used later on to design detailed models that can be simulated. Most often, the design tasks are split among several suppliers. This calls for precise requirements to be passed to them, so that, as far as feasible, suppliers can work independently. Some of the requirements specify the allowed behavior of the sub-system to be design, while others specify the assumed behavior of the sub-system’s environment.
During operation of a CPS, maintenance tasks play an ever-increasing role, to minimize the downtime of the system and, to maintain an extremely low probability of occurrence of catastrophic failures. Diagnosis enables to replace some routine inspections or precautionary replacements of critical parts (that are usually triggered by the number of hours of operation, or by calendar) by fewer maintenance operations, triggered by the estimated wear or aging of those parts. This helps to reduce immobilization times and maintenance costs. Design models could be reused to help the development of diagnosis software that will trigger maintenance operations, based on the output of parity check algorithms, capable of detecting slow or sudden changes of some parameters. Reusing design models in this context would be a genuine innovation, in comparison to the established practice, where diagnosis is designed by hand, from scratch.
We propose to investigate the extension of Modelica for the formalization of requirements and of the systematic reuse of Modelica design models to derive system diagnosis software.
Verification
Because of severe complexity or undecidability problems, CPS formal verification can be done only on partial and simplified models. When applicable, these techniques complement usefully simulations. Despite of the high level of expertise it requires, formal verification brings a level of confidence in the analyses that can not be compared with what can be obtained by simulation. Using formal verification makes sense only for the most critical parts of a CPS. A fine example is the formal correctness proof of a new generation of aircraft collision prevention system, the ACAS-X. This proof has facilitated the certification of this system, according to the established aeronautic standards(DO-178C).
We believe that the right approach towards scalable CPS is to combine design exploration by simulation, with focuses on the most critical parts of the CPS under design, using formal verification. In particular, we want to investigate the use of formal deductive systems (theorem provers) to reason about DAEs. Such approach is not meant to scale but rather to gain insights into qualitative aspects of DAEs (for instance, invariant regions, limiting cycles or equivalences). The hope is to be able to combine locally those computationally expensive symbolic procedures with the relatively lightweight structural analysis to enrich the latter, when needed, with additional non trivial aspects of multi-mode DAEs such as chattering, sliding modes or Zeno behaviors.
