Consolidation de validation fonctionnelle de systèmes critiques à l'aide de model checking. Application au contrôle commande de centrales nucléaires

The verification and validation of safety-critical real-time system are subject to stringent standards and certifications. Recent progress in model-based system engineering should be applied to such systems since it allows early detection ofdefects and formal verification techniques. This thesis proposes a model-based testing (MBT) methodology dedicated to functional validation of safety-critical real-time systems. The method is directed by the structural coverage of the Lustre model co-simulated with the physical process and by the functional requirements. It relies on a repetitive use of a model checker to generate coverage-based open-loop test sequences. We also propose a refinement technique of progressively adding environment constraints during test generation. The refinement is expected to support the passage from coverage-based open-loop test sequence to functional requirements-based closed-loop test case. Our methodology also considers the state explosion problem of a model checker and proposes a heuristic called hybrid verification combining model checking and simulation.La vérification et la validation de systèmes critiques temps réel sont des activités soumises à de contraignants standards et certifications. Les progrès récents en Ingénierie Système basée sur les modèles peuvent être appliqués en utilisant des techniques formelles de vérification dès la phase amont avec un grand bénéfice pour détecter des défauts. Cette thèse propose une méthodologie basée sur les modèles dédiée à la validation fonctionnelle de tels systèmes. La méthode est dirigée à la fois par par la couverture structurelle du modèle en Lustre d’un système réactif en co-simulation avec un procédé physique, et par les besoins fonctionnels. La méthode s’appuie sur l’utilisation répétitive d’un model-checker et permet de générer des séquences en boucle ouverte. Nous proposons aussi un raffinement qui supporte le passage de cette séquence de test aux cas de tests en boucle fermée. Nous prenons en compte le problème de l’explosion combinatoire de model-checking et finalement nous proposons une heuristique dite vérification hybride combinant model-checking et simulation