#	Pagina
attuale pagina	/open-h2020/projects/194114/results.html

Report

Teaser, summary, work performed and final results

Periodic Reporting for period 2 - UnCoVerCPS (Unifying Control and Verification of Cyber-Physical Systems)

Teaser

Summary

UnCoVerCPS provides methods for a faster and more efficient development process of safety-critical or operation-critical cyber-physical systems in (partially) unknown environments. Cyber-physical systems are very hard to control and verify because of the mix of discrete dynamics (originating from computing elements) and continuous dynamics (originating from physical elements). We are developing completely new methods for de-verticalising the development processes by a generic and holistic approach towards reliable cyber-physical systems development with formal guarantees. In order to guarantee that specifications are met in unknown environments and in unanticipated situations, we synthesise and verify controllers on-the-fly during system execution. This requires to unify control and verification approaches, which were previously considered separately by developers. For instance, each action of an automated car (e.g. lane change) is verified before execution, guaranteeing safety of the passengers. Our new methods are integrated in tools for modelling, control design, verification, and code generation that will leverage the development towards reliable and at the same time open cyber-physical systems. Our new methods are demonstrated for wind turbines, automated vehicles, smart grids, and physical human-robot interaction within a consortium that has a balanced participation of academic and industrial partners.

Work performed

During the second review period, we have continued to provide methods for a faster and more efficient development process of safety- or operation-critical cyber-physical systems in (partially) unknown environments. A special focus of the second review period has been on conformance checking of cyber-physical systems to ensure soundness of the verification results. Another focus has been to improve the efficiency of control and verification techniques to verify systems online. This makes it possible to react to unexpected situations. Due to the built-in resilience, the testing and development effort is substantially reduced. Our new methods continue to be demonstrated for wind turbines, automated vehicles, smart grids, and physical human-robot interaction, although the wind turbine use case has been discontinued based on the feedback of the last review.

Novel on-the-fly control and verification concepts

In order to predict what actions of surrounding intelligent agents are possible, we use reachability analysis to predict the set of possible future behaviours. To be able to react on time, we have developed new techniques for the verification of cyber-physical systems. This has been achieved by the results in Task 3.1 Faster methods for reachability analysis of nonlinear systems and Task 3.2 Pre-computation of reachable sets for partial reference trajectories. These results are especially important for autonomous cyber-physical systems, such as our use cases on automated driving and human-robot interaction. The smart grid use case is not so sensitive with respect to real-time computation, but guaranteeing results is hard due to the complexity of the problem. We propose compositional verification as developed in Task 3.3 to fight the curse of dimensionality. The complexity of smart grids and other cyber-physical systems is also addressed from the control perspective through Task 2.2 Networked predictive control for hybrid cyber-physical systems.

Unification of control and verification

The combination of making decisions and verifying them on-the-fly requires unifying control and verification, since it is no longer possible for a system designer to adapt the controller if a specification violation occurs. First results in this direction have been developed in Task 2.3 Enhancing the real-time computability of online control for cyber-physical systems and Task 3.4 Incremental verification in interaction with online controller adaptation. As detailed in the Description of Action, the main effort in this direction will be in the third review period.

Seamless integration of modelling and conformance testing

Our main innovation in terms of modelling is the systematic test of conformance between the models and the behaviour of the real system. In order to achieve conformance, we include set-based and stochastic uncertainty in our models, especially those describing entities surrounding the considered system. The set of possible behaviours is computed by novel algorithms for set-based and stochastic reachability analysis. The modelling has been standardized in Task 1.2 Abstraction and refinement of hybridsystem models. In UnCoVerCPS, we have agreed to use (stochastic) hybrid automata to model our use cases. Models for all use cases (wind turbines, automated vehicles, smart grids, and physical human-robot interaction) have been completed and are currently refined to address control design and verification needs. The main focus of the second period was to provide a systematic approach to conformance testing of cyber-physical systems (Task 1.3): since industrial-scale hybrid systems are typically not amenable to formal verification techniques, one typically aims to verify abstractions of the original system. However, one needs to show that this abstraction conforms to the actual system implementation including its physical dynamics. We have made quite a lot of progress in this regard and applied the
approach to the test vehicles of DL

Final results

Due to the restricted use of words, we would like to refer the reader to our deliverables and publications to read about the progress beyond the state of the art:

https://cps-vo.org/group/UnCoVerCPS/Deliverables

https://cps-vo.org/group/UnCoVerCPS/Publications