The core of UnCoVerCPS is a model-based development for future cyber-physical system: Hence, modelling plays a key role in UnCoVerCPS. The control design and the safety verification rely on hybrid automata models of system behaviour and corresponding formalised system requirements. Due to the inherent complexity of control and verification of hybrid automata, the cyber-physical system models have to be abstracted in a way that only the most relevant effects are considered. In this work package, we investigate how to derive such simple, abstract and compositional models of cyber-physical system, possibly adding uncertainty. We refine them for control and verification and check our abstraction by conformance testing of concrete implementations. The work package improves model-based development of cyber-physical system based on the following tasks:

• Modelling and identification of networked cyber-physical systems
• Abstraction and refinement of hybrid system models for verification and control
• Conformance testing of cyber-physical system implementations for checking realisation effects
• Automatic formalisation of system requirements

The crucial part of designing a cyber-physical system with (fully or partially) autonomous behaviour is to equip the cyber-component with algorithms for control and planning, which affect the physical part (through actuation devices) consistent to given specifications. Due to the characteristics of cyber-physical systems that a pair of decision-making component and physical part is embedded into a dynamic environment, the algorithms for control and planning have to be reactive, i.e. specifications have to be satisfied also for time-varying interactions with the environment. In addition, the specifications like goals to be attained or safety restrictions to be enforced may change over time. For instances of cyber-physical systems like traffic systems, human-robot cooperation, or smart grids, the control design a-priori to operation is infeasible, since not all behaviour of the environment possibly occurring during operation can be foreseen. This motivates the investigation of online techniques for decision making within this work package.
For many realisations of cyber-physical systems the (partial) modelling or identification of the physical behaviour of the cyber-physical system and the environment is possible, offering the use of model-based predictions for decision making. This together with the necessity of considering constraints (e.g., collision avoidance in automated driving or physical coupling of nodes in a smart grid) suggests the use of model predictive control. Existing variants of this class of control techniques are, however, not readily employable for cyber-physical systems with the properties listed above. The investigations in this work package aim at extensions:

• to handle discontinuous changes of the dynamics and constraints,
• to account for the uncertainty of the predictions and to quantify the probabilities of success,
• to ensure that real-time constraints and convergence properties are obeyed,
• and to use the benefits of reachable set computations within control procedures.

As for any control involving groups of decision makers, a question for distributed cyber-physical systems is which decisions are fixed by a central instance or by a local controller. We will investigate different schemes of distributed, cooperative, and hierarchical control to explore where and how given goals and constraints should be accounted for. The results from this work package will establish a set of methods for online decision making of cyber-physical systems, based on which tools for online operation will be realised in WP 4.

This work package investigates new methods to significantly reduce the computation time for formal verification methods of continuous and hybrid systems. As a consequence, it will be possible to verify if planned actions are safe during the operation of the system. The online capability of the verification allows one to consider the current situation and thus tackle the problem of verifying systems in unknown and changing environments. Note that the proposed advances in on-the-fly verification will also benefit classical offline verification. The method of choice is reachability analysis due to its favourable computation time compared to other formal methods. The computation time is significantly decreased by the following tasks:

• Faster methods for reachability analysis of non-linear systems
• Pre-computation of reachable sets for partial reference trajectories
• Compositional verification
• Incremental verification in interaction with online controller adaptation

The development of a cyber-physical system is composed of several phases: specifications, design, coding and verification. UnCoVerCPS proposes a tool chain that realises this workflow and supports the de-verticalisation ambitions of the call, which is composed of the following tools:

• SCADE and Simplorer developed at Esterel Technologies. They are used to develop the model and the plant description and are used for certified code generation;
• SpaceEx developed at Universite Joseph Fourier Grenoble 1 and CORA developed at Technische Universitat Munchen. The interaction with SpaceEx and CORA tools increases the verification capabilities by identifying the reachable states of cyber-physical systems. Both tools will be the basis for new tools that can verify systems on-the-fly: SpaceExonl and CORAonl;
• DMPC-HS newly developed at Universitat Kassel and ScenarioMPC newly developed at Politecnico di Milano. These tools are used for the development of model predictive controllers. DMPC-HS is applied to non stochastic systems, while ScenarioMPC is applied to stochastic systems;
• the newly developed tools ConfTest for conformance testing and formalSpec to formalise specifications.

The objectives of WP 4 are the realisation of new tools, the extension of existing tools, and the integration of the tools into a tool chain.

The objective of this work package is to show the applicability and the value of the results of previous work package to selected use cases. This refers to the de-verticalisation goal as required by the call. The use cases studied in this work packages are:

• Wind turbine: this example will demonstrate that the holistic development in UnCoVerCPS yields lower costs and higher power output, while guaranteeing a defined level of safety.
• Smart grid: in this case study we investigate the scalability of our developed methods and their ability to represent and analyse a variety of stochastic uncertainties.
• Automated driving: the automotive use case addresses two different challenges. Cars are moving based on human interaction and environmental conditions. Besides developing safe autonomous behaviour, we also include human factors in the design of automated driving to study effects when the grade of automation changes, especially in dangerous situations. The consideration of other traffic participants is necessary for a holistic safety design process.
• Human-robot collaborative manufacturing: in this example we study how human behaviour can be modelled and analysed in the framework provided by UnCoVerCPS. A variety of models, controllers, and verification concepts, based on stochastic and non-stochastic uncertainties will be developed.

The use cases are selected so that they offer different and complimentary challenges in the design of controller for CPS.

The main objectives of the dissemination activities are:

• Reaching out to a large set of different targets via various dissemination channels
• Becoming an integral part of the international cyber-physical systems community
• Providing academic services, such as organising workshops and special sessions at conferences
• Implementing structures that ensure open-access of scientific results, software tools, and benchmark examples

The planned activities and the new supplements are documented in a dissemination plan, which will be updated after each project meeting. A balanced dissemination between industrial and academic audiences is supported by the 50/50 distribution of partners from industry and academia. The main dissemination activities are:

• Project website integrated into the Cyber-Physical Systems Virtual Organization
• Scientific publications
• Ensuring a strict open source policy
• Workshop and summer school organisation
• Educational activities

For each of the mentioned activities we have a separate task, except for scientific publications. The WP leader will coordinate the publication activities, identify publication opportunities and keep track of the overall publication effort.
Besides dissemination tasks, we also have a separate task on exploitation.

The main task of management is to provide an environment such that the researchers can focus on their scientific work. Purely administrative tasks will be performed in the background by the project management office at Technische Universitaet Muenchen. Management provides:

• a framework to support timely and qualitative achievement of project results;
• quality assessment of project results;
• risk management including corrective actions in the work programme;
• innovation management to maximise scientific output and dissemination;
• timely and efficient administrative and financial co-ordination of the project to meet contractual commitments.