Assistant de Preuves et Systèmes Temporels/Temporisés – TAPAS

La conception et vérification formelles de systèmes critiques exigent de considérer avec la même importance, dès le début, les exigences fonctionnelles et temporelles. Néanmoins, intégrer le temps sous toutes ses formes dans les assistants de preuves reste un défi majeur car le temps est souvent intégré tard, après plusieurs niveaux de raffinement et de manière manuelle et ad-hoc. D'un autre côté, il y a de nombreux modèles de temps riches et variés qui ont chacun leur expressivité et leurs limites mais qui intègrent peu ou pas les exigences fonctionnelles. Nous distinguons le temps des autres propriétés non-fonctionnelles car beaucoup d'autres propriétés sont interdépendantes du temps (énergie, chaleur, sécurité) et le temps prend une importance particulière dans les systèmes hybrides ou systèmes cyber-physiques dont certaines parties dont décrites par des équations différentielles.
Ce projet propose des outils et une méthodologie pour combiner Event-B à des outils de vérification automatique de propriétés temporelles et promeut le temps comme un citoyen de premier niveau. D'un côté, cela augmente l'efficacité des assistants de preuve sur les propriétés temporelles qui peuvent être établies efficacement par des model-checkers. D'un autre, cela repousse les limites des outils de vérification automatique par l'utilisation de preuves sur des modèles paramétriques, lorsque la preuve généralise sur un domaine un résultat sans nécessiter l'exploration exhaustive (explicite ou symbolique) du domaine. Ceci constitue une innovation majeure pur la vérification des systèmes critiques en combinant les avantages des deux communautés qui à ce jour, progressent essentiellement séparément.