La méthodologie CDL et l’outillage OBP

Le système contrôleur SM

Le cas d’étude retenu pour illustrer puis valider notre approche est un sous-système SM (System Manager) d’un système militaire. Le logiciel embarqué de ce système est responsable de la commande et du contrôle de l’ensemble du système, ses modes internes et ses actions en réponse aux informations reçues de l’environnement. Durant son fonctionnement, le système SM est relié à des périphériques (radars, capteurs, rampes de lancement. . . ) et il gère la connexion des opérateurs au système via des HMIs (Human Machine Interface) (figure 3.1). Le système étudié est critique, soumis à des contraintes de fiabilité et de sureté strictes. SM a été modélisé en UML2 à l’aide de l’outil Rhapsody puis implémenté en code Java. Le modèle comportemental du système a été traduit vers le langage Fiacre [Berthomieu et al. 2007, Berthomieu et al. 2008]. Les scénarios d’utilisation du SM ont été formalisés en CDL. Les exigences exprimées dans le cahier des charges du composant SM sont au nombre de 70. 3.1.2 Architecture du système Le SM permet aux opérateurs de lancer une mission, d’arrêter une mission ou d’éteindre le système. Pour ce faire, les opérateurs peuvent, via des consoles appelées HMI, envoyer des requêtes. Les HMIs envoient des requêtes au SM au moyen de communications asynchrones. Le SM répond par l’affirmative ou la négative et renseigne au besoin les HMIs de l’évolution du système. Dans certains cas, le SM doit communiquer avec d’autres acteurs, comme l’authentification (Authentification) ou le gestionnaire d’équipements (EquipmentManager), pour décider s’il accède ou non à une requête. Pour la construction des contextes, les acteurs HMIs sont considérés comme des acteurs inclus dans le contexte et le gestionnaire d’équipements et l’authentification sont considérés comme des processus du système (figure 3.1). 

Cas d’utilisation

 Durant l’initialisation, le SM commence par demander au gestionnaire d’équipements quelles sont les consoles atteignables. Une fois renseigné, il informe ces dernières qu’il est prêt à recevoir des requêtes de login. Pour pouvoir décider s’il accède à la requête de login, le SM consulte d’abord l’authentification. Si les informations sont correctes, il informe, la console correspondante de son état courant en plus d’accepter la commande. 

Exemple d’exigence à vérifier sur le modèle 

Pour compléter l’illustration du cas d’étude, nous présentons une exigence R extraite du cahier de charge du système SM. Ainsi, l’approche présentée dans ce mémoire a pour but de faire le lien entre la forme informelle des exigences présentées dans le cahier des charges et les propriétés formalisées dans les modèles CDL. Nous allons détailler par la suite le processus permettant la mise en oeuvre de ce lien. Exigence R : « During the initialization phase, registered console might ask the SM for loging. The SM have to associate an identifier to asking console within the MaxDlog delay. » Ainsi, au cours de la procédure d’initialisation, SM doit associer un identificateur à chaque périphérique (HMI) du système ayant demandé à se loguer, avant un délai MaxD_log. Chaque périphérique logué peut demander une opération et reçoit en retour un rôle avant un délai MaxD_oper. L’initialisation s’achève avec succès, lorsque SM a affecté tous les identificateurs et les rôles aux périphériques. Dans le chapitre 9, nous présentons l’application de l’approche proposée dans ce mémoire pour la génération d’une spécification formelle des exigences textuelles telle que l’exigence R. 

LES PRINCIPES MIS EN ŒUVRE DE LA VÉRIFICATION AVEC CDL

 Prise en compte de l’environnement des modèles à valider

 Un système réactif communique de façon continue avec son environnement de manière à répondre à ses sollicitations. Pour appliquer une vérification par model-checking, il est donc nécessaire de fermer ce système en décrivant son environnement. De façon générale, dans le domaine de l’embarqué, les environnements ne sont pas quelconques, mais sont bien identifiés. Ils sont définis par les connaissances que l’ingénieur a des différentes phases qui caractérisent le cycle de vie du système à concevoir. De plus, les exigences incluses dans la spécification sont, dans la majorité des cas, relatives à ces phases, qui régissent le comportement du système, tel que les phases d’initialisation, d’échange de données, de changement de modes, de reconfiguration, ou encore, les modes dégradés. Ces modes sont activés par des événements issus de l’environnement du système. Ce dernier est composé d’autres entités logicielles ou sous-systèmes. Il devient donc alors inutile de prendre en compte la totalité des comportements de l’environnement pour la vérification de chaque exigence. De ce fait, l’idée consiste à se focaliser sur une partie pertinente du comportement du système et sur les propriétés que l’on souhaite vérifier. Le fait de restreindre les comportements de l’environnement permet de réduire la taille de l’automate global obtenu après composition (synchronisation forte) du système avec ce dernier. Sur cette idée, une méthode de description de l’environnement sous la forme de cas d’utilisation (ou contextes) a été développée [Roger 2006, Dhaussy & Boniol 2007, Dhaussy et al. 2009, Dhaussy et al. 2011]. Elle propose à l’utilisateur de spécifier, dans le langage CDL1 , le comportement souhaité de l’environnement du modèle à valider. Le langage CDL, présenté en détail dans la section 3.3, est intégré dans une méthodologie de vérification et exploité par l’outillage OBP. 

Identification des contextes pour contourner l’explosion combinatoire

 Lors de la vérification de propriétés sur un modèle, un model-checker explore tous ses comportements et vérifie, lors de l’exploration, s’il y a violation des propriétés exprimées. Toutefois, il est souvent le cas que le nombre de comportements atteignables du modèle exploré est beaucoup trop grand à cause de l’explosion du nombre d’états du système. Lors de la mise en œuvre du model-checking, traditionnellement, la description des contextes, c’est-à-dire des interactions entre l’environnement et le modèle, est incluse dans la description du modèle du système (Figure 3.3.a) à valider. Le contexte prend la forme d’un automate composé avec d’autres automates du modèle à valider lors de l’exploration. A ce niveau, pour éviter l’explosion combinatoire, il faut identifier et expliciter des contextes qui soient suffisamment restrictifs pour limiter le nombre de comportements à explorer lors du model-checking. C’est le premier stade d’une politique de « diviser pour régner » en activant des sous-ensembles des comportements du modèle. Mais l’expérience montre que pour éviter l’explosion, les contextes doivent décrire un nombre limité de comportements de l’environnement [Dhaussy et al. 2011]. Ceci implique donc la description d’une multitude de contextes ce qui peut être très pénalisant dans un processus industriel. Dans l’approche développée dans [Dhaussy et al. 2011], il a été choisi d’expliciter les contextes séparément du modèle, dans un formalisme spécifique qui permet de les traiter avant la composition avec le modèle. Pour identifier les contextes, l’utilisateur se base sur la connaissance qu’il a de l’environnement du système ou de ses parties, pour les spécifier formellement. Ils correspondent aux modes d’utilisation du composant modélisé. Dans le contexte des systèmes embarqués réactifs, l’environnement de chaque composant d’un système est souvent bien connu. Il est donc plus simple d’identifier cet environnement que de chercher à réduire l’espace des configurations du modèle du système à explorer. L’objectif est de disposer (Figure 3.3.b) de la description des sous-ensembles des comportements des acteurs de l’environnement (Contextei , i œ [1..n] en Figure 3.3.b) et des propriétés (Propriétéi) associées à ces comportements. Cette identification des contextes peut déjà permettre de contourner l’explosion lors de l’exploration du modèle. Pour la mise en œuvre de cette approche, le processus de développement du système doit inclure une étape de spécification de l’environnement permettant d’identifier explicitement des ensembles de comportements. L’hypothèse forte qui est faite ici pour mettre en œuvre ce processus méthodologique est que le concepteur est capable d’identifier les interactions entre le système et son environnement. Chaque contexte exprimé au départ est considéré comme fini, c’est-à-dire que les scénarios décrits par ce contexte ne présentent pas de comportements itératifs infinis. Cette hypothèse est justifiée, en particulier dans le domaine de l’embarqué, par le fait que le concepteur d’un composant logiciel doit connaître précisément et complètement le périmètre (contraintes, conditions) de son utilisation pour pouvoir le développer correctement. Il serait nécessaire d’étudier formellement la validité de cette hypothèse de travail en fonction des applications ciblées.