%0 Book Section
%9 OS CH : Chapitres d'ouvrages scientifiques
%A M' Guerroumi Fawzi
%T Logique temporelle pour la spécification et la vérification des systèmes réactifs
%B 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
%C Paris
%D 1996
%E Moukeli, P.
%L fdi:010008794
%G FRE
%I ORSTOM
%@ 2-7099-1333-X
%K MODELE MATHEMATIQUE ; SYSTEME INFORMATIQUE ; PROGRAMMATION
%K RESEAU DE PETRI ; PARALLELISME
%P 884-894
%U https://www.documentation.ird.fr/hor/fdi:010008794
%> https://horizon.documentation.ird.fr/exl-doc/pleins_textes/pleins_textes_6/colloques2/010008794.pdf
%W Horizon (IRD)
%X 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)
%S Colloques et Séminaires
%B CARI'96 : Colloque Africain sur la Recherche en Informatique = CARI'96 : African Conference on Research in Computer Science
%8 1996/10/09-16
%$ 122LOGIC