Back-to-back Testing

Problématique posée¶

Dans les systèmes critiques, les normes prévoient des activités pour maîtriser les défauts qui séparent la spécification d’un système de son implémentation.

Parmi ces activités, on trouve la vérification, les tests, la simulation, la preuve, la validation, la qualification des outils utilisés. Une des problématiques industrielles concerne la difficulté à valoriser dans la politique de validation tous les travaux menés sur des modèles ou des codes qui ne sont pas encore le logiciel exécuté sur sa plateforme d’exécution.

L’approche B2BT proposée par Systerel s’inscrit dans les techniques de génération automatique de test par Model Checking123 mais propose d’apporter de nouveaux éléments de conviction pour utiliser plus massivement les travaux menés sur des modèles ou du code source par une génération automatique de tests qualifiant la conformité de logiciel exécutable à la sémantique du modèle / code source.

Spécificités de l’outil B2BT ¶

La solution de B2BT développée par Systerel s’appuie sur nos technologies existantes. Nous avons donc fait le choix de réaliser nos modèles en High Level Language (HLL) 4, le langage utilisé par nos solutions Systerel Smart Solver (S3) 5. Un modèle peut être le résultat de différentes activités : réalisation spécifique aux activités B2BT, réutilisation des données de validation et de vérification, traduction automatique à partir d’un autre langage, etc.

Enfin, ce modèle est utilisé par l’outil B2BT afin de générer des séquences de test.

Le B2BT s’inscrit dans la catégorie du test par comparaison du comportement observable et à ce titre, les séquences générées décrivent pour chaque pas d’évolution du système les sorties attendues en fonction de ses entrées et de l’état de ses mémoires. Le choix de la stratégie utilisée pour la génération des séquences, ainsi que le niveau de confiance accordé à ces séquences sont décrites dans la deuxième partie.

Bien que cela ne soit pas l’objet de cet article, il est important de noter que le même modèle HLL, peut être utilisé par notre moteur d’analyse S3-core afin d’effectuer des activités de preuve formelle.

Application sur un modèle simple¶

Afin d’illustrer le processus de génération des séquences, une application logicielle volontairement simple, mais compréhensible et représentative est détaillée dans cette partie.

Considérons que cette application dispose de 2 entrées, représentées par deux variables booléennes \(I1\) et \(I2\), et de 2 sorties, représentées par deux variables booléennes \(O1\) et \(O2\).

Le comportement observable des sorties en fonction des entrées est décrit par les équations booléennes suivantes.

Considérons de plus que nous disposons d’un équipement testable, c’est à dire, dont il est possible de commander les entrées afin d’en contrôler les sorties, qui embarque une implémentation logicielle basée sur le comportement décrit en (1) et (2).

Génération des séquences¶

On peut construire le modèle HLL correspondant à ce système. Ce modèle est explicité dans la Fig. 1.

Figure 1 : Modèle HLL de l’application

Le modèle HLL est ensuite utilisé pour générer les séquences de test. A l’issue de la génération, on obtient un scénario de test de longueur 4 cycles, tel que présenté dans la Fig. 2 où chaque ligne représente les états successifs (f pour False, t pour True) de chaque variable d’entrée (\(I1\) et \(I2\)) et de chaque sortie (\(O1\) et \(O2\)).

Figure 2 : Séquence de test B2BT générée

Tests sur machine hôte / simulateur¶

Le test sur machine hôte / simulateur permet de mettre en place un moyen de test avec les moyens de contrôle les plus fins :

• La synchronisation de l’exécution du système à tester,

• L’observation maximale (les variables internes peuvent devenir accessibles).

Cette souplesse maximale assure le bon cadencement des entrées ainsi que la synchronisation fine des sorties.

Tests en « boîte blanche »¶

On parle de test en « boîte blanche » quand le moyen de test et la machine à tester rassemblent les conditions suivantes :

• Le moyen de test s’interface à la machine cible,

• Le moyen de test dispose d’un accès en lecture et en écriture aux variables internes du système à tester,

• Le moyen de test permet de piloter le démarrage d’un cycle sur la machine cible.

Il est alors possible de commander les différents cycles de fonctionnement du système à tester ou d’en forcer les variables.

Tests en « boîte grise »¶

On parle de test en « boîte grise » quand le moyen de test peut uniquement lire tout ou partie des variables du système à tester. Dans cette configuration, il est toujours possible de synchroniser le moyen de test à l’aide de variables internes du système à tester. Il faut au préalable que le système dispose de ce genre de variables (compteur de cycle d’exécution, état des acquisitions / émissions, etc.).

Tests en « boîte noire »¶

On parle de test en « boîte noire » quand le moyen de test n’a aucun accès aux variables internes du système à tester. Les tests sont particulièrement complexes à mettre en œuvre dans ce type de configuration. Il est possible d’essayer de synchroniser le moyen de test et le système en dimensionnant leur temps de cycle à des valeurs proches (idéalement égales) et en les démarrant de manière synchrone.

Ce genre de configuration est néanmoins nettement plus sensible aux divergences sur les temps d’exécution.

La maîtrise de l’exécution des tests sur une configuration « boîte noire » peut nécessiter une stratégie de génération des tests particulière afin de rendre le scénario compatible au glissement d’un cycle sur l’échantillonnage. Une telle stratégie est généralement plus coûteuse.

Une alternative consiste à construire une surcouche au système à tester qui embarque les vecteurs de test et les sorties attendues dans le système à tester si ses ressources en offrent la capacité. On se retrouve alors dans une configuration « boîte blanche » mais cela nécessite de modifier le logiciel afin de le rendre compatible avec l’encapsulation.

Optimisation des compilateurs¶

Considérons d’abord que le modèle soit une image sémantiquement équivalente de celle d’un code source. Les différences observables à l’exécution des tests peuvent provenir de la plateforme d’exécution de ce code (ensemble de ressources matérielles, logiciel de base, système d’exploitation) ou du compilateur utilisé pour le transformer en logiciel exécutable. Les défauts rencontrés peuvent ensuite être reproduits et analysés pour identifier la cause racine. Dans le domaine du développement de logiciels critiques, (e.g. IEC 61508-3, IEC 62138), les normes exigent que les outils contribuant à la production du logiciel exécutable soient évalués vis-à-vis du niveau de confiance accordé par rapport à l’existence de défaillance affectant ce logiciel exécutable. Les compilateurs appartiennent à cette classe d’outils. On peut considérer que cette application du B2BT constitue une solution de vérification des sorties du compilateur à l’exécution sur la cible, capturant les défaillances ayant un impact sur les sorties du logiciel exécutable. Cette analogie vaut également vis-à-vis de la plateforme d’exécution mais aussi vis-à-vis d’outils de traduction entre une sémantique de plus haut niveau et un langage compilable.

En s’appuyant sur ce garde-fou, il est désormais envisageable de considérer le B2BT comme un moyen de maitrise d’outils du commerce. Une application pourra être de s’autoriser à exploiter plus largement la puissance des compilateurs, en particulier les options d’optimisation lorsqu’elles sont accompagnées de restrictions telles que « l’activation de l’optimisation lève la garantie sur l’ordre d’évaluation des paramètres d’une fonction » lorsque les tests B2BT sont déroulés avec succès.

Continuité des activités de vérification formelle¶

Considérons ensuite le cas où le modèle qui sert à générer les tests de B2BT n’est pas dérivé du code mais est élaboré dans le cadre d’activités de vérification formelle de propriétés. L’intérêt de la vérification formelle de propriétés est de démontrer mathématiquement que des exigences de sûreté de fonctionnement tiennent sur un modèle, quelle que soit la séquence d’entrées considérée et à quelque profondeur temporelle que ce soit dans la vie du système. Dans ce cas, l’apport du B2BT est de pouvoir démontrer que la machine sous test ne comporte aucune mutation observable par rapport à la sémantique d’exécution du modèle qui a supporté les activités de preuve. Quand les obligations de preuves du modèle formel sont démontrées comme prouvées, cette preuve tient sur la sémantique d’exécution du modèle et par transitivité sur celle de la machine sous test puisqu’elle ne contient pas de déviation observable.

Dans ce cas, B2BT complète les stratégies de validation traditionnelles en permettant de démontrer le respect d’exigences de sûreté de fonctionnement par preuve sur un modèle formel associé à la démonstration de conformité à la sémantique sous-tendant la preuve sur la machine sous test par le bon déroulement des séquences B2BT.

Une telle approche permet de considérer des approches de validation hybrides où la preuve prend à sa charge la démonstration du respect des exigences de sûreté de fonctionnement. Une approche par preuve apporte une couverture complète vis-à-vis de la sûreté de fonctionnement dans le sens où la preuve apporte une démonstration que quelle que soit la séquence d’évènements sur les entrées d’un modèle, une obligation de preuve tient.

Par comparaison, une approche par test fonctionnel est fondée sur une approche par scénario. À l’exception de quelques situations rares où l’exhaustivité des combinaisons est possible, une approche par test assure une couverture par échantillonnage.

La stratégie est donc d’élaborer une politique de validation composant une preuve face aux exigences de sûreté de fonctionnement avec des tests de B2BT générés automatiquement et quelques tests fonctionnels vis-à-vis d’exigences non critiques pour la sûreté de fonctionnement (ergonomie, performances, vivacité, etc.). La preuve apporte une couverture totale face aux exigences de sûreté de fonctionnement. Le B2BT consolide que les exigences de sûreté de fonctionnement tiennent à l’exécution par échantillonnage fin du respect de la sémantique d’exécution.

Il est notable que l’élaboration d’une preuve est moins coûteuse en charge de travail que l’élaboration d’un test en charge d’ingénierie. En effet, l’écriture d’une obligation de preuve consiste à formaliser le « QUOI » d’une exigence.

Ce simple exemple montre que la preuve propose une couverture totale (quelles que soient les séquences de valeur sur les entrées, alors la propriété de sûreté de fonctionnement est respectée) là où le test échantillonne (dans l’approche par scénario, on ne teste qu’une trace du système par rapport à une quantité énorme, si ce n’est infinie). Il démontre également que l’effort d’ingénierie associé à la preuve est plus efficace et plus robuste aux évolutions que l’effort d’ingénierie au service des tests (la preuve ne s’occupe pas de chercher les scénarios, mais d’établir un invariant en toute circonstance et la recherche est déléguée à la machine).

Traitement de l’obsolescence¶

Considérons enfin le cas où le modèle est dérivé d’une version de logiciel d’un équipement obsolète.

Il est courant dans l’industrie qu’un équipement qualifié dans un passé plus ou moins récent ne puisse plus être maintenu, faute de pièces de rechange disponibles voire même d’environnement de test encore opérationnel (serveurs de test sous des OS caduques que les politiques SI bannissent ou banniront à raison des réseaux en raison des vulnérabilités qu’elles présentent). Dans le cadre du traitement d’obsolescence de tels équipements, il est possible de générer par l’approche B2BT des séquences de test de conformité à la sémantique d’exécution du code obsolète.

Ces tests proposent une couverture plus fine que des tests de validation par rapport à cette gestion d’obsolescence dont on sait que l’équipement obsolète les a passés avec succès : le bon déroulement de ces tests démontre que la nouvelle génération de l’équipement n’a pas d’altération sémantique par rapport à la sémantique d’exécution de la version qualifiée mais obsolète.

Dans l’hypothèse où son propriétaire ne dispose pas ou plus des moyens de test de validation de l’époque, les tests B2BT apportent une solution automatique pour reconstruire un référentiel de qualification de la nouvelle génération. Cette approche est à pondérer par rapport à une gestion d’obsolescence assortie d’un ensemble d’évolutions fonctionnelles. Il faudra dans ce cas procéder en deux étapes : qualifier le traitement d’obsolescence par le B2BT puis ajouter un ensemble de tests ou de preuves dédiés aux évolutions fonctionnelles.

Cette approche de traitement d’obsolescence peut se généraliser plus globalement à la maîtrise de portages vers de nouvelles plateformes d’exécution d’un logiciel antérieur.

Validation d’un système critique¶

La perspective d’emploi la plus ambitieuse sera d’utiliser la technologie B2BT couplée à un modèle réalisé par une équipe de validation pour un système critique. En effet, dans cette configuration, ce sera désormais l’équipe de validation à travers son modèle qui impose la sémantique d’exécution de l’objet conforme au besoin du client sans pour autant descendre dans la complexité des moyens de production du logiciel exécutable ou de la plateforme d’exécution de sécurité. Ce dernier cas d’emploi propose une stratégie vis-à-vis de l’intégration de composants du commerce au sein de contrôle commande critiques.

En effet, en s’assurant que la sémantique d’exécution proposée par un calculateur de sécurité du commerce et son environnement de programmation reste sans mutation par rapport à celle d’un modèle du besoin, le B2BT apporte des éléments de réponse sur l’aptitude à l’emploi d’une solution calculateur de sécurité + environnement de programmation fourni en boîte noire avec des conditions d’utilisation sûres.

Mise en œuvre sur les modèles EDF¶

En partenariat avec EDF, Systerel a mis en œuvre l’outil B2BT sur la base d’un modèle Lustre fourni par EDF. Ce modèle a été développé pour correspondre aux applications type utilisées dans certains systèmes de commande et contrôle d’une tranche nucléaire. L’objectif est ainsi d’évaluer l’applicabilité de la méthode de B2BT aux applications nucléaires. Plusieurs étapes successives ont été mises en œuvre afin de permettre l’utilisation de ce modèle pour effectuer la génération des séquences de test B2BT.

Systerel et EDF ont travaillé à la définition de critères de couvertures haut niveau. Trois critères de couverture haut niveau ont été retenus pour vérifier que les tests générés par la solution B2BT couvrent bien les comportements particulièrement sensibles et critiques de l’application. Bien que ces critères ne soient pas détaillés pour des raisons de confidentialité, on peut néanmoins noter qu’ils ont été spécifiquement définis pour ce projet. Le parcours des séquences de test, au regard de ces critères haut niveau, permettra alors d’augmenter le niveau de confiance quant à la couverture des tests par B2BT : non seulement, toutes les mutations sont testées, mais tous les chemins critiques ont bien été parcourus.

Ces étapes sont brièvement décrites ci-dessous :

1. Prétraitement des fichiers d’entrée Les fichiers d’entrée, au format Lustre V6 pour les besoins de l’étude, nécessitent une traduction vers le langage HLL,

2. Analyse de la bonne définition du modèle

   Avant de lancer la génération des séquences de test, une passe de vérification de bonne conception du modèle est réalisée à l’aide du moteur d’analyse S3. Cette vérification consiste principalement à s’assurer que le modèle initial est sain en confirmant l’absence, par exemple, d’accès aux variables en dehors des bornes définies ou encore de division par zéro.

3. Génération des séquences de test

   Une fois le modèle traduit et vérifié, il peut être transmis à l’outil de génération de séquence de test B2BT qui va appliquer les mutations et produire les séquences de test permettant de détecter les éventuels défauts.

4. Mesure du taux de couverture selon les critères définis

   La séquence de test générée est appliquée au modèle de l’application afin de mesurer la valeur du taux de couverture atteinte pour chacun des critères de couvertures définis.

5. Exécution de la séquence de test

   Cette dernière étape consiste à jouer la séquence de test sur l’équipement cible. Il est à noter que dans le cas où l’étape 1 introduirait des fautes sur la sémantique, alors celles-ci seront détectées lors de l’exécution du test, sauf cas de fautes combinées.

   Du fait de l’existence de temporisations longues (plusieurs centaines de cycles) dans l’application étudiée et de l’explosion de l’espace d’état inhérente à l’utilisation d’un moteur de preuve à des profondeurs importantes, le modèle a été outillé afin de permettre le pilotage des mémoires et des temporisations.

À ces deux types de génération de test B2B s’ajoute une génération de séquence de test orientée sur des objectifs de test de plus haut niveau que ceux de la stratégie par défaut.

Résultats¶

Conclusion¶

Ces différentes expérimentations ont montré que cette méthode de génération automatique de séquences de test permet d’adresser efficacement des problèmes de validation de systèmes industriels et de prendre en compte les contraintes matérielles (banc de test standard ou outillé) et de complexité (génération par mutation des opérateurs ou par critères haut niveau uniquement) pour l’exécution des séquences de test.