| Résumé | Cet article propose une méthode de construction d'un ensemble d'obligations de preuve à partir de la spécification architecturale d'un système concurrent. Cette spécification architecturale exprime les exigences d'exactitude d'un système concurrent à un niveau élevé, sans faire référence aux fonctionnalités des composants. Les obligations de preuve dérivées de cette spécification sont exprimées sous la forme de tâches de vérification du modèle, dans un modèle de comportement pertinent, dans lequel les composants se voient attribuer leurs fonctionnalités respectives. Une extension expérimentale de l'outil SPIN est utilisée comme vérificateur ou contrôleur de modèle. La notation des schémas synoptiques utilisée pour spécifier l'architecture permet d'encapsuler dans un module représentatif des composants interchangeables ayant des fonctionnalités cibles équivalentes. Une obligation de preuve d'un tel système est représentée sous la forme d'une tâche de vérification de l'équivalence dans le modèle de comportement choisi. On démontre comment des obligations de preuve irréalisables peuvent être décomposées, en décomposant la spécification de l'architecture. La décomposition des obligations est fondée sur des conditions d'hypothèse garantie. |
|---|
