Concepts for correctness of complex configurations of components, connectors and contracts – Cx

Cx is a 36-months industrial-research project proposed by an academic partner (Onera, coordinator) and an
SME (ClearSy).
Systems engineering, in the civil as well as in the defence industry, lacks an effective environment for
systems architecture modelling and verification. Industrial approaches exist, mainly based upon UML/SysML,
but their expressive capabilities are quite limited, as far as architecture is concerned, and the possibilities for
formal verification are more limited yet. However, the academic state of the art is rich, with many concepts
addressing common concerns but, in the end, without end-to-end corresponding tool chain.
Cx is devoted to fill in the gap between the rich architectural concepts developed in the academic literature and
the industrial state of practice concerning architecture modelling and validation. We expect our contribution
to lie in the selection of an adequate subset of these concepts and then the production of a synthesis both
adapted to industrial-grade design and formal verification. We want to apply promising theoretical concepts
proposed by algebraic approaches so that system engineers can take benefit from expressiveness, abstraction,
modularity and compositionality they offer. For this, we will follow a pragmatic approach: Cx will provide
working proofs of concepts for modelling and formally validating systems architectures.
In order to achieve theses goals, we will propose a language called Fusain, and an associated methodology,
for which we have the following requirements:
– Fusain will be rich
Fusain will contain the main concepts (components, connectors, interfaces, rich behavioural contracts)
addressing common concerns involved in systems architectures. Fusain will also allow to model and val-
idate reconfigurations of system architectures: indeed, although reconfigurations are rising in particular
in defence avionic architectures, they are poorly considered in current modelling frameworks.
– Fusain will be formally grounded
The definition of Fusain formal semantics will be twofold. The behavioural contracts of omponents and connectors
will be defined in terms of transition systems and/or temporal logic. This will be the basis
of the verification methodology, which will rely on existing model checkers. We will also pursue a
more exploratory work on the semantics of coordination with coalgebraic approaches. Indeed, they are
promising in term of modularity and compositionality of specification languages, which are important
concerns addressed by architectures. We will study the interest of a coalgebraic approach in the
development of an efficient and compositional verification methodology.
– Cx we will follow a pragmatic approach
Fusain definition will be coupled with an editing and parsing environment, and the proposed verification methodol-
ogy will be implemented as a prototype. Besides, our approach will be assessed on a real and reasonably
large-scale system coming from the ClearSy case study.