001020823
100  $a20120326                 y50      
101  $afre
2001 $aVérification formelle des machines à états abstraits par la logique temporelle des actions$bressource électronique
210  $aUniversité d'Oran1 - Ahmed Ben Bella : Département d'Informatique$cUniversité d'Oran1 - Ahmed Ben Bella$d2010
215  $a147F.$d30 cm
328 1$bDoctorat$cInformatique$eDépartement d'Informatique , Université d'Oran1 - Ahmed Ben Bella$d2010
330  $aLe Travail présenté dans cette thèse porte sur la formalisation et la vérification formelle des modèles ASM en utilisant la logique temporelle des actions(TLA). L'approche de formalisation proposée avec la logique TLA, s'appuit sur la définition d'un ensemble de règles de traduction permettant de formaliser les aspects structurels et comportementales d'un modèle (ou une spécification) ASM, en des expressions logiques de leur sémantique dans le langage de spécification formelle TLA+. Ces règles de traduction sont proposées comme des directives permettant de guider l'interprétation formelle des concepts d'un modèle ASM, en termes des concepts logique du langage de spécification TLA+.En ce sens, l'objectif principal de cette approche de formalisation est de pouvoir traduire des spécifications ASM en des spécifications temporelles TLA+ supportant des techniques de preuves axiomatiques associées à la logique TLA, permettant d'établir la preuve de  correction qu'une spécification ASM donnée satisfait les propriétés temporelles initialement exigées par le système modélisé en terme du formalisme ASM.
337  $a BIBLIOG.143-147F.
610  $aLa Logique Temporelle des Actions (TLA)
610  $a Machines à Etats Abstraits(ASMs)
610  $a Algèbres Dynamiques
610  $a Spécifications Temporelles
610  $a Comportements  (Séquences d'Etats d'Exécution)
610  $a Propriétés Temporelles(Propriétés d'Invariance ou de Sureté)
610  $a Vérification Formelle (Preuve de Correction).
700  $aEL HABIB DAHO, Hocine
701  $aArray
801 0$aDZ$bCERIST PNST
901$ac
990  $aTH3230