S3 v2.0 — Une avancée majeure dans le monde de la vérification formelle

Introduction¶

La nouvelle version du moteur de preuve S3 arrive … et avec elle, une amélioration significative de ses performances ! De quelle manière et comment, embarquez avec nous pour découvrir un monde de nouvelles opportunités.

S3 et la vérification formelle de systèmes et logiciels¶

Dans le monde industriel, la certification des systèmes et logiciels critiques exige des garanties très fortes de sûreté et de fiabilité. Les méthodes formelles de vérification sont des moyens de démontrer de manière rigoureuse que ces systèmes respectent leurs spécifications et leurs impératifs de sécurité. Ces méthodes sont explicitement reconnues, recommandées ou encouragées par les normes industrielles de certification.

Par exemple, les normes suivantes recommandent l’utilisation des méthodes formelles:

• logiciel ferroviaire : EN 50128 ;
• aéronautique : DO-178C et en particulier le DO-333 qui traite des méthodes formelles ;
• industrie / énergie /système de sécurité : IEC 61508.

Le Model Checking est une des techniques de vérification formelle automatique. Il consiste à démontrer mathématiquement que l’ensemble des traces d’un modèle respecte une propriété logique. Les moteurs de preuves sont des outils de Model Checking qui ont vocation à démontrer mathématiquement qu’une propriété logique est vraie, à partir d’un ensemble d’hypothèses.

Les outils de Model Checking permettent ainsi de vérifier rigoureusement que le comportement d’un programme respecte ses spécifications, offrant ainsi un niveau de confiance bien supérieur aux tests traditionnels.

S3 (Systerel Smart Solver) est l’outil de Model Checking développé par Systerel. La version v2.0 du moteur d’analyse au coeur de la solution S3 (aussi appelé moteur de preuve) arrive sur le marché, et avec elle une accélération spectaculaire des temps d’analyse nécessaires à la vérification formelle des systèmes.

À quel point le moteur de preuve S3 v2.0 est-il plus performant ?¶

Le Model Checking est particulièrement efficace pour vérifier des systèmes à états finis ou modélisables par un nombre fini d’états.

Nous l’utilisons par exemple pour vérifier des systèmes ferroviaires, parmi lesquels on peut citer :

• les systèmes d’enclenchement ferroviaire : qui commandent l’ensemble des objets à la voie tels que les aiguilles, les signaux ferroviaires etc … de manière sûre¹;
• les systèmes CBTC : “Communication Based Train Control” : systèmes de contrôle automatique du trafic ferroviaire basé sur la communication continue entre le train et des ordinateurs chargés de piloter le trafic en sécurité. ²

Les systèmes d’enclenchement ferroviaire sont parmi les plus adaptés à une analyse par Model Checking. Les systèmes CBTC sont beaucoup plus complexes à analyser car ils contiennent non seulement de la combinatoire booléenne, comme les systèmes d’enclenchement, mais aussi de l’arithmétique entière, qui fait exploser la complexité de l’analyse du modèle.

Cependant, la version v2.0 du moteur de preuve S3 a permis une accélération très importante des temps d’analyse de ces systèmes très complexes. Sur des serveurs très puissants, de plusieurs dizaines de coeurs, le temps d’analyse pour les systèmes CBTC passe de 1 an en temps cumulé de processeur avec des moteurs de preuves de la génération précédente (tels que S3 v1.0, ou ceux nos concurrents) à … 1 semaine de calcul ! A ce résultat spectaculaire s’ajoute le constat suivant : il n’y a pas de dégradation de performances sur les systèmes les plus simples, et certains types de systèmes, tels que les systèmes d’enclenchement sont, eux aussi, légèrement plus rapides à analyser.

Types de systèmes	Moteur de preuve classique	S3 v2.0
Systèmes CBTC	1 an	1 semaine
Autres systèmes	pas de dégradation des performances

Comment avons-nous atteint ces performances ?¶

Comment avons-nous atteint ces résultats spectaculaires ? La réponse tient en deux grands points :

• une diversification de nos solveurs,
• une collaboration non déterministe des solveurs.

Une diversification de nos solveurs¶

Quelques rappels sur les classes de complexité :

• les problèmes P sont des problèmes qui peuvent être résolus en temps polynomial par un algorithme déterministe,
• les problèmes NP sont des problèmes pour lesquels une solution proposée peut être vérifiée en temps polynomial,
• il est communément admis que P!=NP, c’est-à-dire qu’il n’existe pas de solution polynomiale pour résoudre les problèmes NP.

Une propriété fondamentale de la classe des problèmes NP-complets est que tout problème NP peut être ramené à un autre problème NP.

Le problème SAT³ est l’archétype des problèmes NP-complets. C’est un problème qui consiste à trouver une valuation des variables d’une formule booléenne qui la rend vraie.

A partir d’un système à vérifier, il est possible d’encoder un problème et ses propriétés sous la forme d’un ou plusieurs problèmes SAT.

Les moteurs de preuve, et donc en particulier le moteur de preuve S3, permettent de résoudre ces problèmes SAT en s’appuyant sur des solveurs CDCL⁴. Ceux-ci explorent une formule booléenne, et en déduisent des relations mathématiques entre les différentes variables, appelées clauses. Chaque clause apprise permet de couper des chemins de l’exploration permettant au final :

• soit de construire une preuve que la propriété est toujours vraie,
• soit d’attribuer des valeurs aux variables qui falsifient la propriété.

Le moteur de preuve S3 utilise un portfolio. C’est à dire qu’il lance en parallèle plusieurs solveurs, les plus divers possibles. Ces solveurs collaborent, c’est-à-dire qu’ils s’échangent les clauses qu’ils ont apprises au fur et à mesure de l’analyse d’un système.

Pour améliorer et accélérer le plus possible l’analyse, il faut que les solveurs qui collaborent ensemble soient :

• les plus variés possibles, pour diversifier les clauses qu’ils s’échangent,
• et puissants : pour que l’analyse soit la plus rapide et efficace possible.

Ces rappels faits … voyons maintenant ce qui a changé par rapport à la version v1.0.

L’ajout de deux nouveaux solveurs¶

Systerel a rajouté au coeur de la version v2.0 du moteur de preuve S3, deux nouveaux solveurs CDCL⁴ très puissants. C’est en grande partie grâce à ces nouveaux solveurs que l’analyse des systèmes CBTC est beaucoup plus rapide.

Un paramétrage plus fin des heuristiques internes de nos solveurs¶

Nos trois solveurs sont très diversifiés. Il est possible de les diversifier encore plus en paramétrant leurs heuristiques internes. Ainsi, il est possible de lancer plusieurs instances d’un même solveur en parallèle, chaque instance du même solveur, ayant des paramètres différents, ne va pas parcourir le même chemin, ne pas trouver les mêmes clauses… Ce qui assure une collaboration efficace.

Une collaboration non déterministe des solveurs¶

Comme expliqué plus haut, lors de l’analyse d’un système, notre moteur de preuve lance en parallèle un certain nombre de solveurs, les plus divers possibles. Ces solveurs collaborent en s’échangeant les clauses qu’ils ont apprises. Il existe deux manières pour eux de s’échanger les clauses :

Le mode déterministe¶

Chaque solveur se voit allouer un nombre d’opérations. Ce nombre est évidemment calibré et choisi en fonction du type de problème, du type de solveur… A l’issue de ce nombre d’opérations, un point de rendez-vous a lieu avec les autres solveurs, pour qu’ils s’échangent les clauses qu’ils ont apprises.

Avantage	Ce mode de fonctionnement est déterministe, deux exécutions de la même analyse donneront le même résultat, dans le même temps. Ce mode de fonctionnement est d’autant plus utile que, si un bogue se produit, chaque analyse le reproduira, et il sera donc possible de l’identifier pour le corriger.
Inconvénient	Puisqu’il est impossible de prévoir à l’avance le nombre d’opérations optimal pour minimiser le temps de calcul, les solveurs les plus rapides vont attendre les solveurs les plus lents. Il est donc évident que ce mode de fonctionnement ne permet pas d’optimiser à son maximum le temps de calcul.

Le mode non déterministe¶

Nous avons rajouté à notre outil la possibilité d’exploiter un portfolio en mode non déterministe. Cette fois, les points de rendez-vous ne sont plus fixés à l’avance, et chaque solveur échange les informations utiles avec les autres solveurs quand le moment lui semble le plus opportun. Ainsi, les solveurs ne s’attendent pas, tout solveur utilise 100% de l’espace de calcul qui lui est alloué, et le temps d’analyse s’en trouve donc considérablement réduit.

Cependant, quand un programme est multithreadé, c’est le système d’exploitation qui décide quand chaque thread s’exécute. L’ordonnancement peut donc changer entre deux exécutions, ainsi que l’ordre d’accès aux ressources partagées. Sans points de rendez-vous, deux exécutions de la même analyse n’auront donc pas la même trajectoire. Ce mode est par définition … non déterministe. Ceci a les conséquences suivantes :

• deux exécutions de la même analyse ne prendront pas exactement le même temps d’analyse
• si le problème SAT est satisfiable, le contre exemple exhibé ne sera pas forcément exactement le même
• de la même manière, si le problème est non satisfiable, la preuve ne sera pas forcément strictement identique, même si elle est équivalente
• enfin, si un bogue se produit pendant l’exécution, il ne sera pas forcément facile de le reproduire…

Avantage	Ce mode de fonctionnement améliore significativement le temps de calcul.
Inconvénient	Ce mode de fonctionnement est donc par définition … non déterministe. Si un bogue se produit pendant une exécution, il ne sera pas facile de le reproduire.

Pourquoi privilégier le mode non déterministe¶

Le coeur d’exploitation du moteur de preuve S3 est un (ou plusieurs) algorithme(s) CDCL⁴. Ces algorithmes reposent sur la boucle suivante :

• décision (choisir une variable et lui assigner une valeur Vrai ou Faux)
• propagation de la valeur de cette variable dans la formule (et en déduire de nouvelles assignations de variables découlant de la décision)
• détection de conflit (si conflit, en déduire la nouvelle clause)
• apprentissage de la clause (ajouter la clause aux clauses déjà connues)
• retour en arrière (et recommencer les étapes précédentes).

Ces étapes sont conceptuellement simples, et le coeur d’un tel algorithme tient en seulement quelques milliers de lignes de code.

Il est donc assez juste de considérer qu’il est très peu probable de tomber sur un bogue lors de l’exécution du moteur de preuve S3. L’utilisation du mode non-déterministe n’expose donc pas à un risque élevé.

Conclusion¶

La version v2.0 du moteur de preuve S3 a permis une amélioration spectaculaire de nos temps d’analyses sur les systèmes les plus complexes. Cette amélioration est le fruit des modifications suivantes dans le logiciel :

• une diversification plus grande des solveurs, avec l’ajout notable de deux nouveaux solveurs très différents du premier,
• l’ajout du mode d’analyse ‘non déterministe’, qu’il est tout à fait légitime d’utiliser, puisqu’il est peu probable de tomber sur un cas de figure qui poserait problème.