Test automatique de propriétés dans un atelier de développement de logiciels sûrs
Institution:
Paris, CNAMDisciplines:
Directors:
Abstract EN:
The FoCal environment, developed by researchers coming from the laboratories LIP6, CÉDRIC and INRIA), allows one to incrementally build library components with a high level of confidence and quality. A component of a FoCal library can contain specifications, implementations of operations and proofs that the implementations satisfy their specifications. The components are translated into OCaml code and verified by the Coq proof assistant. Even if the FoCal environment ensures a high level of confidence because of its methodology based on specification and proofs, we cannot do without testing. Low level properties, for example axioms, are usually not proven. FoCal permits one to import OCaml untrusted code into a FoCal certified code, which can \emph{break} the specification. Finally, testing could be used to check an implementation when a proof attempt fails or when the proof is not yet done, in order to find counter-examples for examples. This thesis deals with the design and development of a testing tool integrated into FoCal. The methodology consists in testing properties automatically. Test data are defined as valuations of the quantified variables of the property under test which satisfy the premises (called the precondition) of the property. The conclusion of the property serves as an oracle. We propose two approaches to select test data: randomly or through the usage of constraint reasoning. For the latter case, we translate the precondition into a constraint system whose resolution will provide us with the expected test data. Our approach is formally defined and we prove that the test data obtained by constraint resolution satisfy the precondition.
Abstract FR:
L'environnement FoCal, développé conjointement par des chercheurs des laboratoires CÉDRIC, LIP6 et de l'INRIA, permet de construire de manière incrémentale des composants de bibliothèque avec un haut niveau de confiance et de qualité. Un composant de bibliothèque FoCal peut contenir des spécifications, l'implantation des opérations spécifiées et des preuves que la spécification et l'implantation sont en conformité. Les composants FoCal sont traduits en code exécutable OCaml et vérifiés par l'assistant à la preuve Coq. Même si un développement en FoCal nous assure un haut degré de confiance dans le programme, de par une spécification formelle et les preuves de correction, nous ne pouvons nous passer du test. Les propriétés de bas niveau, comme les axiomes, ne sont en général pas prouvées. FoCal autorise l'importation de code non sûr au sein de code FoCal certifié, ce qui peut amener à « casser » la spécification. Finalement, le test peut être utilisé pour avoir confiance en une implantation dont la preuve de correction n'est pas encore effectuée ou terminée ou lorsqu'une tentative de preuve échoue, pour trouver des contre-exemples. Ce manuscrit présente le développement d'un outil de test intégré à FoCal. La méthodologie repose sur le test automatique de propriétés. Les jeux de test sont définis comme des valuations des variables quantifiées de la propriété sous test, qui satisfont les prémisses de la propriété (précondition). La conclusion de la propriété sert d'oracle pour le test. Nous proposons deux stratégies de recherche des jeux de test : aléatoire et par résolution de contraintes. Pour cette dernière, nous traduisons la précondition de la propriété en un système de contraintes. Sa résolution nous permet d'obtenir les jeux de test recherchés. Cette méthodologie est formellement définie et nous prouvons que les jeux de test ainsi construits satisfont la précondition.