This shows you the differences between two versions of the page.
|
cercles:projet_cercles [2012/06/26 00:15] 127.0.0.1 external edit |
cercles:projet_cercles [2012/06/26 00:18] (current) phil |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | Cette page se trouve désormais là : [[cercles:Projet_CERCLES]] | + | ==== Les étapes du projet ==== |
| + | |||
| + | Nous reprenons ici la descriptions des «tâches» décrites lors de la soumission du projet. Nous omettons les tâches 1 et 7 qui concernent respectivement la gestion du projet et la dissémination de ses résultats. | ||
| + | |||
| + | === 2: Etat de l'art === | ||
| + | |||
| + | Il existe de nombreux travaux concernant la vérification compositionnelle mais peu sont relatifs à la certification. Cet état de l’art est nécessaire pour connaître de manière approfondie les travaux relatifs à la fusion des modèles formels et aux différents modes de raffinement notamment en B. Les résultats de cette tâche alimenteront la tâche 3 et surtout les tâches 4 et 5. | ||
| + | |||
| + | === 3: Définition des «composants précertifiés» === | ||
| + | |||
| + | On peut caractériser de tels composants, entre autres, par une batterie complète de tests de certification. Cette batterie est construite de telle manière que son exécution correcte garantisse que le composant en question respecte sa spécification (et les propriétés associées) au sens de la DO178B donc qu’il est, par définition, pré-certifié. On fera l’hypothèse qu’on dispose de cette batterie de tests autrement dit on ne la construira donc pas (ce qui est un autre champ de recherche). En revanche, il faudra élaborer le modèle formel du composant à partir de ses tests, c’est l’un des objectifs principaux de cette tâche sans laquelle les tâches suivantes n’auraient plus de sens. Celle-ci sera également concernée par la levée du verrou V2 c’est-à-dire le passage à l’échelle. La tâche.3 ne pourra commencer que lorsque l’état de l’art (tâche précédente) sera disponible (ou peu avant) afin que l’on puisse s’inspirer de techniques ou de solutions scientifiques pré-existantes. | ||
| + | |||
| + | === 4: Solution théorique === | ||
| + | |||
| + | La tâche.4 forme le corps du projet CERCLES puisqu’il s’agit, à partir des résultats de la tâche.3 et de l’état de l’art de la tâche.2, de définir une méthodologie de modélisation et de validation de l’assemblage de composants certifiés. L’approche se veut à la fois : | ||
| + | |||
| + | * top-down: un modèle du système est produit, accompagné des propriétés fonctionnelles attendues | ||
| + | |||
| + | * bottom-up : le système s’appuie sur des composants existants qu’il convient de réutiliser au sein d’un assemblage. | ||
| + | |||
| + | Les travaux à mener devront donc permettre de : | ||
| + | |||
| + | * définir une méthode de raffinement et de décomposition du modèle système (B événementiel) qui permette de réutiliser sans effort la spécification de composants existants (similaire à la notion d’importation de machines abstraites en B logiciel) | ||
| + | |||
| + | * déterminer quels types de propriétés fonctionnelles doivent être extraits des composants existants. L’objectif est de ne retenir que les propriétés nécessaires à la démonstration des propriétés au niveau système (il n’est absolument pas envisageable de complètement spécifier en B les composants existants). A cet égard, une attention particulière devra être accordée aux propriétés impliquant le temps. | ||
| + | Ces travaux auront un impact fort sur les outils développés, en fonction des décisions prises et résultats obtenus. Par exemple, il sera peut être nécessaire de modifier le générateur d’obligations de preuve, d’ajouter des annotations dans les modèles B afin d’orienter le processus de raffinement/preuve/validation, etc. | ||
| + | |||
| + | Il faudra aussi examiner le problème de la génération des tests structurels c’est-a-dire de ceux qui dépendent de l’implémentation des composants et de leur « fusion » en vue de leur assemblage. Cette tâche est très liée à la précédente si bien que les tâche.3 et tâche.4 seront en partie menées en parallèle (avec la tâche.5 d’ailleurs). | ||
| + | |||
| + | === 5: Démonstrateur === | ||
| + | |||
| + | La (ou les) solution(s) trouvées par la tâche.4 doit(vent) être implémentée(s) c’est l’objet de la tâche.5. Toutefois, il n’est pas exclus que la technique par raffinement de B soit revue. En effet, concernant CERCLES, la situation est délicate puisqu’il faudra, dans les phases amont, orienter la suite de raffinements de manière à ce qu’elle « rencontre » les modèles de bas niveau correspondants à l’assemblage des composants pré-certifiés utilisés pour construire le système. Par conséquent, il faudra au cours de toutes les étapes de raffinement des indicateurs (une information prospective) précisant que cette orientation est la bonne et qu’on ne marquera pas le but final. C’est cette recherche d’information supplémentaire émanant du niveau bas (les composants) qui constitue la principale préoccupation de cette tâche. Il est possible que de nouveaux opérateurs (ou méthodes) de raffinement soient proposés. Le résultat final de cette tâche sera un démonstrateur qui préfigurera un atelier B spécifique dédié à la certification compositionnelle au sens de CERCLES. Ce démonstrateur sera validé partiellement à l’aide de petits exemples empruntés au monde industriel (une validation plus large sera effectuée par la tâche suivante). On notera que la tâche.5 ne pourra commencer qu’une fois les résultats de la tâche précédente acquis. Toutefois, un recouvrement partiel avec cette dernière pourra être effectué. | ||
| + | |||
| + | Parallèlement avec ces travaux il faudra élaborer un outil qui engendre du code pour l’assemblage des composants pré-certifiés. | ||
| + | |||
| + | === 6: Application industrielle === | ||
| + | |||
| + | la dernière tâche technique sera consacrée à la validation des résultats précédents (en particulier du démonstrateur) et au passage à l’échelle. Ainsi, elle sera concernée par la réalisation d’un cas (use case) industriel (proposé par Sagem) dont les spécifications seront très proches de celles d’un système critique réel (du domaine de l’aéronautique). L’idée est d’utiliser comme composants pré-certifiés des modules générés automatiquement par l’atelier SCADE. Néanmoins, il faudra, pour chaque module, élaborer la batterie de tests complète garantissant sa pré-certification au sens du projet. Il s’agit-là d’un sujet qui n’est pas dans le champ des préoccupations CERCLES. Ainsi, on utilisera les modèles en entrée de SCADE pour générer à la main ou mieux avec un outil du commerce adéquat cette batterie de tests (et on complètera manuellement s’il le faut). Les composants ainsi générés puis construits seront synchrones mais l’application dont il est question ici les composera de manière asynchrone (on sera ainsi dans un contexte GALS). Avec les méthodes et procédés issus des tâches précédentes, il faudra montrer qu’avec cette bibliothèque de composants SCADE on pourra construire l’application en question avec la garantie que ses propriétés globales (déduits de sa spécification) sont respectées. | ||
