M' Guerroumi Fawzi. (1996). Logique temporelle pour la spécification et la vérification des systèmes réactifs. In :
Moukeli P. (ed.). CARI'96 : actes du 3ème colloque africain sur la recherche en informatique = CARI'96 : proceedings of the 3rd African conference on research in computer science. Paris : ORSTOM, p. 884-894. (Colloques et Séminaires). CARI'96 : Colloque Africain sur la Recherche en Informatique = CARI'96 : African Conference on Research in Computer Science, 3., Libreville (GAB), 1996/10/09-16. ISBN 2-7099-1333-X. ISSN 0767-2896.
Titre du document
Logique temporelle pour la spécification et la vérification des systèmes réactifs
Année de publication
1996
Type de document
Partie d'ouvrage
Auteurs
M' Guerroumi Fawzi
In
Moukeli P. (ed.), CARI'96 : actes du 3ème colloque africain sur la recherche en informatique = CARI'96 : proceedings of the 3rd African conference on research in computer science
Source
Paris : ORSTOM, 1996,
p. 884-894 (Colloques et Séminaires). ISBN 2-7099-1333-X ISSN 0767-2896
Colloque
CARI'96 : Colloque Africain sur la Recherche en Informatique = CARI'96 : African Conference on Research in Computer Science, 3., Libreville (GAB), 1996/10/09-16
Dans cet article, nous nous intéressons à une classe particulière de systèmes informatiques, les "systèmes réactifs" qui regroupent ceux dont l'objectif est plutôt le maintien d'une interaction avec un environnement que le calcul d'un résultat à partir de données en entrée. Pour énoncer la correction de ces systèmes, les formalismes de la logique classique ne peuvent être utilisés : en effet, il est nécessaire d'exprimer des propriétés portant sur le déroulement même de leur exécution. Il est donc légitime de les étudier à l'aide de techniques déductives formalisant des concepts temporels. Le propre des logiques "modales" dont fait partie la logique temporelle est de proposer de telles méthodes. Nous présentons ici un environnement de programmation logique mettant en oeuvre ce type de méthodologie. Le modèle de calcul sous-jacent considéré est celui des réseaux de Petri à prédicats. (Résumé d'auteur)
Plan de classement
Logiciel [122LOGIC]
Descripteurs
MODELE MATHEMATIQUE ; SYSTEME INFORMATIQUE ; PROGRAMMATION ; RESEAU DE PETRI ; PARALLELISME
