METHODES FORMELLES 1

Description

Dans la première partie, le problème de la modélisation, spécification et validation de systèmes, en particulier concurrents, est étudié. Les systèmes de transitions sont utilisés comme outil de base de modélisation. Les logiques temporelles linéaire (LTL) et arborescente (CTL) permettent de spécifier les propriétés de sûreté, vivacité et équité de tels systèmes. La seconde partie aborde la conception et expérimentation des technologies principales d'analyse statique et dynamique : approche déductive, vérification de modèles, interprétation abstraite, génération de tests, analyse de sûreté.

Bibliographie

Specifying Systems (Leslie lamport - Addison-Wesley)
  The Temporal Logic of Reactive and Concurrent Systems (Zohar Manna et Amir Pnueli - Springer Verlag)
  Principles of Program Analysis (Flemming Nielson and Hanne R. Nielson - Springer)

Organisation

• Systèmes de transition (Coefficient 50 )
• Vérification par Analyse Statique (Coefficient 50 )