Composys, 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 done naturally and quickly by means of these formal “explanations”.

Composys, using the model to produce a project document

In addition, following strict rules, CompoSys designs the model to allow the 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 understandable (than the formal language) to a reader who is non-expert in formal language. The generated documents includes the description of system components and  their functions and inputs/outputs, all in the form of diagrams and homogeneous explanations.

Composys : enables virtual integration of the system components

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 Composys models are compatible with the Atelier B tool from Clearsy

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.

Tools and Techniques

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
  • A term dictionary editor
  • A B model checking tool
  • A component consistency checking tool
  • A natural language technical documentation generator

Comments are closed.