@incollection{fdi:010008794, title = {{L}ogique temporelle pour la sp{\'e}cification et la v{\'e}rification des syst{\`e}mes r{\'e}actifs}, author = {{M}' {G}uerroumi {F}awzi}, editor = {}, language = {{FRE}}, abstract = {{D}ans cet article, nous nous int{\'e}ressons {\`a} une classe particuli{\`e}re de syst{\`e}mes informatiques, les "syst{\`e}mes r{\'e}actifs" qui regroupent ceux dont l'objectif est plut{\^o}t le maintien d'une interaction avec un environnement que le calcul d'un r{\'e}sultat {\`a} partir de donn{\'e}es en entr{\'e}e. {P}our {\'e}noncer la correction de ces syst{\`e}mes, les formalismes de la logique classique ne peuvent {\^e}tre utilis{\'e}s : en effet, il est n{\'e}cessaire d'exprimer des propri{\'e}t{\'e}s portant sur le d{\'e}roulement m{\^e}me de leur ex{\'e}cution. {I}l est donc l{\'e}gitime de les {\'e}tudier {\`a} l'aide de techniques d{\'e}ductives formalisant des concepts temporels. {L}e propre des logiques "modales" dont fait partie la logique temporelle est de proposer de telles m{\'e}thodes. {N}ous pr{\'e}sentons ici un environnement de programmation logique mettant en oeuvre ce type de m{\'e}thodologie. {L}e mod{\`e}le de calcul sous-jacent consid{\'e}r{\'e} est celui des r{\'e}seaux de {P}etri {\`a} pr{\'e}dicats. ({R}{\'e}sum{\'e} d'auteur)}, keywords = {{MODELE} {MATHEMATIQUE} ; {SYSTEME} {INFORMATIQUE} ; {PROGRAMMATION} ; {RESEAU} {DE} {PETRI} ; {PARALLELISME}}, booktitle = {{CARI}'96 : actes du 3{\`e}me colloque africain sur la recherche en informatique = {CARI}'96 : proceedings of the 3rd {A}frican conference on research in computer science}, numero = {}, pages = {884--894}, address = {{P}aris}, publisher = {{ORSTOM}}, series = {{C}olloques et {S}{\'e}minaires}, year = {1996}, ISBN = {2-7099-1333-{X}}, ISSN = {0767-2896}, URL = {https://www.documentation.ird.fr/hor/fdi:010008794}, }