SeDRe


Résumé de la présentation de Loïc Fejoz

Loïc est ingénieur expert et travaille pour l'équipe MOSEL .

DIXIT

L'approche de Mosel pour la conception de systèmes est une approche par raffinements (top-down). Une des techniques utilisées est la création de diagrammes de prédicats. Ces diagrammes permettent de modéliser les états de systèmes finis ou infinis. On peut ensuite vérifier des propriétés temporelles de ces systèmes par model-checking.

Dixit est un support à cette méthode. Il permet d'éditer ces diagrammes mais aussi de générer les obligations de preuves. Dixit s'appuie en cela sur des prouveurs et model-checkers existants.