UnCoVerCPS tool chain

UnCoVerCPS proposes to assemble a tool chain 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 Université Joseph Fourier Grenoble 1 and CORA developed at Technische Universität München. 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 Universität Kassel and ScenarioMPC newly developed at Politecnico di Milano. These tools are use 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 (Bosch) for conformance testing and formalSpec (GE) to formalise specifications. The deliverable comprises the following elements from WP4 (incl. tasks and participants): - Translation scheme from SCADE/Simplorer to hybrid automata, including a hybrid automata code generator prototype (T4.2, ET,UJF) - C++ library for zonotopes to be included in SpaceEx (T4.3, TUM,UJF) - Exchange formats and the associated APIs between the tools SCADE, Simplorer, SpaceEx, CORA, formalSpec, and ConfTest (T4.4, ET,UJF,TUM,GE) - C code generator prototype for SCADE with extensions (T4.6, ET) The interaction between the tools SCADE, Simplorer, SpaceEx, CORA, formalSpec, and ConfTest is to be demonstrated and tested on a set of applications as described in task 4.5 (UKS, PoliMi, UJF, TUM).