[fr] La vérification de programmes consiste à analyser les comportements possibles de programmes
en vue de déterminer s’ils seront toujours conformes à ce qui est attendu. Pour ce
faire, les caractéristiques souhaitées des comportements sont exprimées formellement et confrontées,
par des techniques mathématiques rigoureuses, à l’ensemble des comportements du
programme à analyser. Dans ce contexte, les automates jouent un triple rôle. Tout d’abord, ils
sont fréquemment utilisés en tant que langage de programmation simplifié pour décrire les programmes
à analyser. Ensuite, ils servent de formalisme de description de propriétés de comportements,
soit directement, soit par traduction à partir d’un langage logique. Finalement, ils
s’avèrent très utiles en tant que formalisme de description d’ensembles infinis de valeurs.
Disciplines :
Computer science
Author, co-author :
Wolper, Pierre ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données)
Language :
French
Title :
Automates et vérification
Publication date :
December 2006
Main work title :
Encyclopédie de l'informatique et des systèmes d'information
