Ce blog est strictement personnel et les opinions exprimées ici n'engagent donc que moi, et notamment pas mon employeur...

mercredi 17 novembre 2010

Normes et formalisation B (I)

Avertissement : Compte tenu du sujet particulier évoqué ci-dessous, il est encore «plus vrai que d'habitude» que ce qui est écrit ne reflète que mon point de vue personnel sur la question. 


Précaution 1 : N'ayant pas l'intention de faire un billet pédagogique ou de référence, aucun rappel technique, contextuel ne sera fait. Je suppose le lecteur intéressé suffisamment informé de la problématique.


Précaution 2 : La terminologie utilisée est largement approximative, il ne s'agit pas de couper les cheveux en 4 mais plutôt de discuter de l'«esprit des choses». Par exemple, si le terme «certification» possède plusieurs définitions précises selon les contextes, l'utilisation faite ici reste conceptuelle : grosso modo, on voit bien ce dont il est question.


Mes collègues  se posent sérieusement la question d'utiliser du B dans leur développements logiciels ferroviaires. Un gros paquet de questions tourne autour de la certification.

Dans le domaine ferroviaire, et en particulier les aspects contrôle-commande, le cadre normatif est constitué des normes 50128/50129, normes dérivées de la norme CEI 61508 (cf google ;-). Ce cadre ne traite pas spécifiquement  du cas B, ni d'ailleurs du cas UML, de Lustre ... Les normes sont généralement très générique en ce qui concerne les technologies particulières employées. Sinon, on ne s'en sortirait pas hein.

Donc, il revient à l'organisme de certification de dériver sa méthodologie «spécifique B» de celle suggérée par le cadre normatif. On pourrait formuler : appliquer à B l'esprit de la norme 50128, ou plus exactement, appliquer au processus de développement intégrant du B...

Quel est l'esprit de la 50128 ? Vaste question. Pour faire bref, la norme vise essentiellement à s'assurer que, dans le cadre du développement d'un système critique (comportant du logiciel en l'occurence) :
  • les personnes impliquées dans le processus sont compétentes à la hauteur des exigences
  • le fournisseur annonce l'existence des phases de développement exigées par les niveaux de criticité du système développé. Plusieurs documents de type «plans» sont à fournir.
  • le fournisseur produit les documents qui matérialisent l'existence et donc la réalisation effective de ces phases
  • l'ensemble de ces documentations présentent de bonnes propriétés (au premier rang la traçabilité) qui permettent d'établir un niveau de confiance adéquat sur les deux affirmations suivantes :
  1. le système a été développé correctement  (le comment)
  2. le système développé est effectivement celui attendu (le quoi)

 Voilà, pour simplifier. Reste à transposer à B, c'est à dire aux phases et artefacts produits lors du sous-processus de développement formel par B.

Le développement B c'est globalement l'écriture [itérative ou cascade] de spécifications (abstraites, raffinement, implémentation), la réalisation des preuves de cohérence de cette spécification, la génération automatique de code. Le tout étant assisté par un atelier logiciel (dont une version «publique» est disponible gratuitement).

On peut mettre de côté l'homologation des outils supports, on va |"admettre" que pour une version donnée des outils B, celle utilisée pour les gros projets, le problème n'est pas là. Les outils sont «certifiés/iables» (rappel de la précaution en préambule, cette formulation n'a pas vraiment de sens reconnu, mais on voit ce qu'elle prétent affirmer). Dans la pratique, les outils sont validés par l'historique de leur usage (e.g. le compilateur gcc est validé par la densité de son utilisation). Ici, l'industriel maintiendra une version spécifique utilisée et «ayant fait ses preuves» (sans jeu de mot) au cours de son expérience passé.

En particulier, comment se passe la certification vis à vis des preuves ?
Est-ce qu'il suffit de dire qu'on a développé le logiciel et prouvé à 100% avec l'Atelier B pour éviter à avoir à montrer des tests unitaires et d'intégrations, ou il faut en faire plus ? 
Quoi ? Montrer des logs de preuves mécaniques ? 

La phase de preuve se décompose généralement en preuve automatique et en preuve intéractive. La preuve automatique n'est pas remise en cause puisque réalisé par un outil ... satisfaisant aux exigences de fiabilité. Par contre la preuve interactive peut être réalisée par l'ajout manuel de règles dites «règles ajoutées». Ces règles doivent faire l'objet d'une phase de validation, c-a-d démontrer qu'elles n'introduisent pas d'incohérence dans le système de preuve. Boum, 50128, cette phase doit avoir été prévue et doit faire l'objet d'un document qui démontre sa réalisation effective. Il faut donc un document de «Validation des règles ajoutées».

Les preuves automatiques, sous-entendu, réussies n'ont pas vraiment d'intérêt sémantique et la manière la plus simple de vérifier leur existence consiste à dispose du modèle B, de l'atelier support et à appuyer sur le bouton de preuve pour vérifier le taux de preuve annoncé dans les rapports de développement. Certes, cela n'est pas toujours matériellement possible. Tout dépend des conditions (logistique) prévues pour le déroulement de l'audit (vaste sujet également...)

Des morceaux de code B ? 

Si on a accès à des morceaux de code B, alors l'accès au modèle complet ne devrait pas être utopique ... Cela dit l'audit du modèle B, en pratique, revient à un échantillonnage de morceaux de modèles B.

Détailler les invariants de liaison ? 

Fondamentalement, le travail d'audit ne consiste pas à essayer de trouver des failles dans la stylistique du développement, surtout lorsqu'il est formel et a priori prouvé, auquel cas les invariants de liaisons sont «corrects».
Par contre, ce qui est pour le moins fondamental, c'est de vérifier que les invariants (de liaison ou pas), qui constituent les fondations d'un développement B cohérent, sont effectivement la transcriptions des propriétés attendues du système. Propriétés qui se trouvent nécessairement décrites (dev critique, 50128, etc) dans la documentation amont du projet. Donc la traçabilité entre les exigences / propriétés exprimées informellement dans la documentation projet et les assertions logiques B (essentiellement les invariants) est LE critère fondamental a évaluer.

Faire quand même des tests ?

Pour éluder le débat, il est considéré comme acceptable de ne pas tester unitairement les fonctions «atomiques» développées en B. Par contre les test d'intégration reste évidemment nécessaires car il n'y a aucune garantie formelle de bon comportement lorsqu'on assemble un composants formel et un composant classique, ni même en assemblant deux composants formels développés séparément. Le point non maîtrisé étant ici les intéractions entre composants, intéractions non modélisées, non formalisées.

Côté documentation, que doit-on donner ? 
Des explications sur le programme B ? 
Des explications sur le lien entre spec informelle et spec formelle ?

Le raisonnement pourrait être le suivant : un modèle B, c'est à dire l'ensemble des spécifications formelles,  peut-être considéré comme l'ultime documentation du code effectivement généré et in fine embarqué.

À ce titre, le modèle B étant dès lors une documentation, il peut être demandé/fourni lors d'un audit.
De même, considéré comme documentation, il doit respecter les exigences de liaisons (traçabilité) entre les documents  en amont («d'où vient ce texte B?») et les documents en aval (ici le code généré donc par définition mécaniquement traçable).

Aucun commentaire: