Methodology for the formal verification of temporal properties for real-time safety-critical applications based on logical time

Méthodologie de vérification formelle de propriétés temporelles pour les applications temps-réel critiques basées sur le concept de temps logique Les systèmes temps-réel critiques doivent respecter des contraintes temporelles strictes qui doivent être considérées tout au long du cycle logiciel. Cependant, du fait que les temps d'exécution exacts ne sont généralement pas connus lors de la conception, le temps logique fournit un moyen d'abstraire les contraintes temporelles et les exécutions du temps physique, dépendant de la plateforme. Dans cette thèse, nous nous concentrons sur deux formalismes basés sur le temps logique. L'approche Synchrone-Réactive abstrait totalement le temps physique en utilisant des bases de temps discrète sur lesquelles les calculs sont déclenchés. L'approche de Temps d'Exécution Logique utilise des bases de temps logique pour représenter non seulement les instants de déclenchement, mais aussi les durées des calculs élémentaires. Dans notre travail, nous commençons par définir une unification des approches Synchrone-Réactives et de Temps d'Exécution Logique, fournissant un cadre formel naturel pour définir la sémantique de PSYC, un langage temps-réel industriel expressif. Nous définissons deux sémantiques pour celui-ci : une sémantique native à grands pas, préservant les durées logiques des intervalles de temps, définie par des règles structurelles opérationnelles ; et une sémantique synchrone à petits pas définie par traduction vers un langage Synchrone-Réactif étendant les durées des intervalles de temps à une succession de transitions atomiques. Nous montrons que les deux sémantiques sont équivalentes. Cette formalisation de la sémantique de PSYC nous permet de définir une méthodologie de vérification formelle pour PSYC basée sur du model-checking symbolique. Pour réduire l'espace d'état pendant le model checking, nous définissons une technique d'optimisation inspirée du model-checking temporisé. Enfin, nous spécifions les exigences temporelles que nous voulons vérifier via un langage de spécification de contrainte d'horloge — CCSL — qui sont ensuite traduites en observateurs synchrones.