Introduction¶

The Coco Platform is a software tool that enables developers to build their software, automatically formally verify whether it is correct, and generate high quality reliable runtime code. The tool provides developers with advanced formal verification and code generation, which are fully automated and integrated into a modern development environment.

The Coco Platform is aimed at developers building event-driven concurrent software. This type of software has to handle events coming from other parts of the system, with limited control over or knowledge of the ordering or arrival of events, and coordinate responses accordingly. It may also have to continually react to asynchronous or synchronous events from other software or hardware components. It is typically highly concurrent due to the asynchronous nature of these systems. Software with these characteristics is often one of the most difficult parts of the software to get right and test effectively using conventional testing practices. By the very nature of this type of software involving interactions between many parts of the system, errors are typically found late in the development cycle during integration testing, or worse in the field, making them expensive and difficult to fix. Further, errors that have propagated into the field are extremely difficult, if not impossible, to reproduce in a testing environment.

The Coco Platform is ideally suited for developing this type of software: Software errors are found and fixed early in the development cycle leading to a speed up in development time, higher quality reliable code, and a reduction in overall cost.

The figure above gives a high-level overview of the Coco Platform running in Eclipse. A developer builds their software in Coco, which is a new modern imperative programming language we have developed specifically for building event-driven software. The Coco Platform will then automatically formally verify whether their Coco code is correct, and provide extensive debugging information for any errors found. Developers typically follow a verification-driven development approach, where they continuously verify their Coco code, fix all of the errors found, and repeat the verification cycle until their Coco code is correct. The Coco Platform then automatically generates the corresponding runtime code.

The Coco Platform provides extensive APIs that allow users to access all functionality of the platform, including verification and code generation. For example, developers can customise the generated code to make sure that it integrates properly into their existing software developed using other tools.