Gérard Berry

Algorithmes, machines et langages

Année 2014-2015

Prouver les programmes : pourquoi, quand, comment ?

Sixième leçon : Vérification et optimisation booléennes d'automates et circuits

Ce dernier cours de 2014-2015 introduit les méthodes implicites de manipulation de systèmes de transitions, à travers les méthodes de calcul booléen utilisées à la fois pour la vérification formelles et pour l’optimisation de circuits électroniques et de programmes qui peuvent se réduire au calcul booléen.

Ces méthodes ont révolutionné le domaine en permettant des vérifications formelles de systèmes dont le calcul explicite des états et transitions est impossible, car la taille des formules manipulées par les méthodes implicites est largement indépendante de celle des systèmes qu’ils décrivent. Nous expliquons d’abord les codages booléens d’ensembles, de relations et de fonctions, et montrons comment calculer l’image directe et l’image inverse de sous-ensembles par des fonctions. Nous étudions ensuite les codages booléens d’automates déterministes et non-déterministes, ainsi que leurs implémentations en circuits électroniques. Nous rappelons le fait que le circuit canoniquement associé à un automate non-déterministe est lui déterministe comme tous les circuits combinatoirement acycliques, ce qui montre clairement que le qualificatif « non-déterminisme » est particulièrement mal choisi : en vérification booléenne comme en optimisation de circuits, il est inutile de déterminiser les automates, et c’est souvent nuisible à cause de l’explosion exponentielle que la déterminisation peut produire. Nous montrons comment la vérification formelle de propriétés de sûreté définies par des observateurs se réduit au calcul des états accessibles, et comment effectuer ce calcul de manière implicite. Nous introduisons la première structure fondamentale du calcul booléen, les Binary Decision Diagrams, développés par R. Bryant au milieu des années 1980 (et indépendamment par J-P. Billion chez Bull en France), et expliquons pourquoi ils permettent de faire les calculs nécessaires au passage à la grande échelle; nous mentionnons leurs limitations, qui sont inévitables car le calcul booléen est NP-complet. Les BDDs seront étudiés beaucoup plus en profondeur dans le cours 2015-2015.

Pour terminer, nous montrons que le codage booléen permet de réaliser des optimisations très efficaces des circuits engendrés par les programmes Esterel. Nous insistons sur le fait que la structure du langage source et la façon d’y programmer les applications sont essentiels pour la qualité de l’optimisation finale : c’est grâce à l’interaction de la séquence, du parallélisme et de la préemption hiérarchique des comportements que les circuits engendrés par Esterel sont systématiquement meilleurs que ceux programmés et optimisés par les méthodes classiques, au moins en ce qui concerne leurs parties contrôle.