Spécification et vérification des propriétés de vivacité en B événementiel
| Autor: | Mosbahi, Olfa, Jaray, Jacques, Ben Ahmed, Samir |
|---|---|
| Přispěvatelé: | Proof-oriented development of computer-based systems (MOSEL), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Modélisation et simulation des systèmes complexes (MOSIC), Faculté des Sciences Mathématiques, Physiques et Naturelles de Tunis (FST), Université de Tunis El Manar (UTM)-Université de Tunis El Manar (UTM) |
| Jazyk: | francouzština |
| Rok vydání: | 2007 |
| Předmět: | |
| Zdroj: | 6ème Colloque Francophone sur la Modélisation des Systèmes Réactifs-MSR 2007 6ème Colloque Francophone sur la Modélisation des Systèmes Réactifs-MSR 2007, Oct 2007, Lyon, France. 16 p |
| Popis: | National audience; Dans ce papier, nous nous intéressons à la vérification de propriétés de vivacité sur des systèmes réactifs. Nous nous basons sur le B événementiel pour la spécification et la validation de tels systèmes. En considérant la limitation du B aux propriétés d'invariance, nous proposons d'appliquer le langage TLA+ pour la vérification de telles propriétés. Nous étendons, en particulier, l'expressivité et la sémantique d'un modèle B pour obtenir un modèle B temporel. En transformant le modèle B étendu en un module TLA+, nous pouvons vérifier ces propriétés grâce au prouveur de théorèmes Isabelle. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|