CompoSys Presentation
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 effected 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
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.
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
Further information will be made available at a later date.
|
