The Coco Platform is a software tool that combines automated formal verification and code generation to improve the development of event-driven concurrent software across industry sectors. Engineers can develop their models in UML using MagicDraw and use the Coco Platform to automatically verify their models are correct and then generate runtime code in C++. The Coco Platform has advanced verification capabilities that enables it to automatically find a broad range of software errors, some of which are well-known to be extremely challenging to find using traditional testing practices. When an error is found, the tool provides extensive debugging information to the users in terms of their own models, enabling the user to fix their models and re-verify them quickly. The combination of modelling, formal verification and code generation leads to rapid iterations over the software design, which in turn reduces the amount of testing required, shortens development time and reduces cost.

In this presentation, we will give an overview of how the Coco Platform can be used to develop complex event-driven software, automatically formally verify UML models developed in MagicDraw, and generate the corresponding runtime code. We also give some examples of software errors that the Coco Platform can automatically find but are notoriously difficult to find using testing and therefore often occur in production.