CompoSys: method and tool dedicated to formal system modelling

What is CompoSys ?

The development of Composys has been discontinued in 2012. The last version released is 1.6. 

CompoSys is a formal tool and method for system modelling. Developped by ClearSy System Engineering, a company specialized in the design and building of safety critical systems, CompoSys is system level modelling tool which benefits from formal tools and Atelier B experience.

Composys has already been used by Clearsy on a number of industrial projects, for example:

  • Functional integration of a military vehicle (SPRAT) carried out by CNIM
  • Modelling of 3 vehicles for diagnostic testing: 206, 307, 407
  • System study for platform screens (façades de quai) installed by the RATP on lines 13 and 14
  • Modelling the computer security policy of an ST Microelectronics hardware component
  • Modelling the interface of a microkernel in the field of microelectronics
  • Modelling the architecture of a USB/CAN communication card
  • Modelling the opening/closing device for Paris line 1 metro platform screen doors
  • Modelling a moving platform filling the gap betwwen the train cabin and the platform.

Results obtained with CompoSys have been communicated through a number of presentations:

Focus on CompoSys

CompoSys is aimed at easing system engineering by providing:

  • a dual modelling processus: B formal method / natural language
  • model coherency automatic and semi-automatic verifications
  • automatic generation of natural language document including several views of the system

A formal tool for system modelling

CompoSys is a tool that allows to formally describe compoennts and their interactions in an hybrid system.

schema+atelierb+composys

CompoSys also uses these common information (or formal model) to produce data for activities that require a precise view of the system. For example:

  • Reliability, Availability, Maintainability and Safety studies,
  • formal proof of properties,
  • functional specification,
  • validation sheets, …

A formal method for system modelling

The modeller is the person responsible for creating and enhancing the description of the system as it is being defined.He helps in the utilisation of this information base. In so-called “operations” he describes how the components use the various system parameters and, for the inter-component parameters, what the physical media involved are: bus, hydraulic circuits, analog circuits, electrical circuits …

The content of the operations is formalised in the form of univalent mathematical functions. In other words, the dependency between the operations and the component interactions is effected naturally and quickly by means of these formal “explanations”.

Using the model to produce a project document

In addition, following strict rules, CompoSys designs the model to allow of enhancement in natural language and with illustrations. The information base therefore has two inseparable aspects:

  • The formal aspect that allows modeller prompting and automation of checks, as well as automation of document generation in all formats needed for multi-discipline utilisation of this information.
  • The non-formal aspect that allows restoring of information that is fuller and more comprehensible (than the formal language) to a reader who is non-expert in formal language. In the generated documents is the description of system components and of their functions and inputs/outputs, all in the form of diagrams and homogeneous explanations.

Virtual integration of the components of the system

Whenever the modeller keys in a new operation, as well as carrying out syntactic and type checking, CompoSys checks 50 consistency rules, and calculates and outlines the component interactions – all this even if working from an incomplete model. In other words, CompoSys allows validation and testing of several functional architectures as they are being described.

This feature is a real asset when the system is under definition and when you want to know its degree of consistency at any given moment.

The formal language used is Event B. In addition, the models produced can be used by the formal tool Atelier B for formal demonstration of properties using abstraction, refinement and invariant concepts. CompoSys has been developed under the Eclipse environment. Two versions are available : a Unix/Linux version (under development) and a Windows version. CompoSys is an Eclipse plugin consisting of:

  • A B model editor
  • An editor of term dictionary
  • A B model checking tool
  • A component-based consistency checking tool
  • A natural language technical documentation generator

Comments are closed.