Model checking symbolique pour les systèmes temps réel

Nous décrivons des programmes à états finis sur un temps à valeurs réelles dans un langage de commandes gardées avec des horloges à valeurs réelles ou, de manière équivalente, sous forme d'automates finis avec des horloges à valeurs réelles. Le model checking répond à la question de savoir quels états d'un programme temps réel satisfont une spécification à temps arborescent (donnée dans une extension de CTL avec des variables d'horloge). Nous développons un algorithme qui calcule cet ensemble d'états de manière symbolique sous forme de point fixe d'une fonctionnelle sur des prédicats d'états, sans construire l'espace d'états. À cette fin, nous introduisons un μ-calcul sur des arbres de calcul sur un temps à valeurs réelles. Malheureusement, de nombreuses propriétés standard de programmes, telles que la réponse pour toutes les séquences d'exécution non-zénoniennes (durant lesquelles le temps diverge), ne peuvent pas être caractérisées par des points fixes : nous montrons que l'expressivité du μ-calcul temporisé est incomparable à l'expressivité du CTL temporisé. Heureusement, ce résultat ne nuit pas à la vérification symbolique des programmes temps réel « implémentables »—ceux dont les contraintes de sûreté sont closes par machine par rapport au temps divergent et dont les contraintes d'équité sont limitées à des bornes supérieures finies sur les valeurs d'horloge. Il est démontré que toutes les propriétés en CTL temporisé de tels programmes peuvent être calculées sous forme de points fixes finiment approximables dans une théorie décidable simple.