Introduction

Coco is a modern imperative programming language designed specifically for the development of event-driven concurrent software in a component-based way. It is also designed to act as an intermediate language that enables straightforward integration into front-end modelling tools. It has a formal semantics, giving a precise meaning to the systems described.

A fundamental building block in Coco is the concept of a component. A component captures a defined part of a system, and has defined interaction points with other components in its environment. A component can either specify a software implementation, or it can specify a network of components. The interactions that a component can perform with other components in a system are specified in terms of services across ports on a component boundary, where services are either synchronous function calls or asynchronous signals.

Component Provided Port Required Port Required Port function calls function calls signals signals

A component can have zero or more provided ports, which specifies the services that the component implements, and provides to other parts of the system. These services are either function calls that can be called on the component, or asynchronous signals that the component can send to other components.

A component can also have zero or more required ports, which specified the services that the component uses from other components in its environment. These are either functions that the component can call on other components, or asynchronous signals that it can receive from other parts of the system that it is connected to.

Coco describes software in terms of:

  • Structure: static relationships between components.
  • Communication: runtime interactions between instances of components.
  • Behaviour: runtime behaviour of the components and ports. These are described using state machines.
  • Correctness properties: properties of the software that will be formally verified (see Ports and Components).

Coco also captures other configuration information regarding the runtime semantics, which has to be reflected as part of the verification and code generation. Details of the runtime semantics can be found in Executing a State Machine.