Concepts pour la correction de configurations complexes de composants, connecteus et contrats – Cx

Cx est un projet de recherche industrielle de 36 mois proposé par un
partenaire académqiue (ONERA, coordinateur) et une PME (ClearSy).

L'ingénierie système, dans l'industrie civile comme dans l'industrie
militaire, manque d'un environnement efficacepour la modélisation et
la vérification de l'architecture des systèmes. Des approches
industrielles existent, principalement basées sur UML/SysML, mais leur
expressivité en ce qui concerne les concepts architecturaux, est assez
limitée. Leur possibilité de vérification formelle est encore plus
limitée. Pourtant, l'état de l'art académique est riche, avec de
nombreux concepts qui permettent de traiter les préoccupations
usuelles, mais sans chaîne véritablement outillée de bout en bout.

Cx est dédié à combler cet écart entre les concepts architecturaux
riches développés dans la littérature, et les pratiques industrielles
concernant la modélisation et la vérification d'architecture. Notre
contribution consistera en partie à sélectionner un sous-ensemble
adéquat de ces concepts, et à produire un synthèse à la fois adaptée à
la conception de systèmes industriels et à la vérification
formelle. Nous voulons appliquer des concepts théoriques prometteurs
proposés par les approches algébriques de telle manière que les
ingénieurs système puissent profiter de l'abstraction, la modularité
et la compositionnalité qu'elles offrent. Pour cela, nous suivrons une
approche pragmatique: Cx fournira des preuves de concepts pour la
modélisation et la validation formelle d'architectures de systèmes.

Afin d'atteindre ces objectifs, nous proposerons un langage appelé
Fusain, et une méthodologie associée, pour lesquels nous avons les
exigences suivantes:

- Fusain proposera des concepts riches et abstraits:
Fusain contiendra les principaux concepts(composants, connecteurs,
interfaces, contrats comportementaux riches) traitant les
préoccupations classiques dans les architectures de systèmes.Fusain
permettra aussi de modéliser et de valider les reconfigurations
d'architectures: en effet, bien que les reconfigurations apparaissent
de plus en plus, en particulier dans les architectures avioniques
militaires, elles sont faiblement prises en compte dans les cadres de
modélisaiton actuels.

- Fusain aura des bases formelles
La définition de la sémantique formelle de Fusain aura deux
volets. Les contrats comportementaux des composants et des connecteurs
seront définis en termes de systèmes de transition et/ou de la logique
temporelle. Ce sera la base de la méthode de vérification, qui
s'appuiera sur les model checkers existants. Nous allons également
poursuivre une travail plus exploratoire sur la sémantique de la
coordination avec les approches coalgebraic. En effet, elles sont
prometteuses en terme de modularité et de compositionnalité des
langages de spécification, qui sont des préoccupations importantes
pour les architectures. Nous allons étudier l'intérêt d'une approche
coalgebrique dans le élaboration d'une méthodologie de vérification
efficace et compositionnelle.

- Cx va suivre une approche pragmatique
La définition de Fusain sera couplée avec un environnement d'édition
d'analyse syntaxique, et de la methodologie de vérification proposée
sera mise en oeuvre sous forme de prototype. Par ailleurs, notre
approche sera évaluée sur une véritable système, de taille
raisonablement grande, provenant de l'étude de cas de ClearSy.