Utilisation conjointe de B et TLA+ pour la modélisation et la vérification des systèmes réactifs
Résumé
La méthode B fournit un cadre rigoureux de développement de systèmes mais sa limitation concerne le type des propriétés exprimées car seuls les invariants sont considérés. Notre travail a pour objectif d'utiliser le B événementiel pour exprimer des propriétés temporelles de fatalité et d'équité. La logique temporelle des actions TLA+ a prouvé son efficacité dans l'expression et la vérification de propriétés d'équité. Elle se base sur le concept de raffinement, d'action et de transition qui exprime une compatibilité avec une modélisation B événementiel. Notre contribution consiste à proposer une méthode de spécification et de vérification utilisant conjointement B et TLA+ et leur outils de vérification l'AtelierB et le prouveur de théorèmes Isabelle.