Méthodes formelles
Introduction au cours de L. MARCÉ, documents sur LOTREC (logiciel utilisé en TP), rapports de TD et TP et examen de 2003
Le fondement mathématique est la caractéristique essentielle des méthodes dites « formelles » qui font l’objet de ce cours.
Tout d’abord, quelques éléments permettant de caractériser ce qu’est une méthode formelle sont donnés ainsi que des indications sur les courants majeurs dans ce domaine.
Deux activités fondamentales entrent dans la constitution d’une méthode formelle : la spécification et la vérification formelles qui d’après Harwood [Harwood96] doivent être considérées comme deux phases distinctes.
La spécification formelle est l’expression, au moyen d’un langage formel, d’un résultat attendu.
La vérification formelle est la production d’une preuve démontrant que le produit respecte effectivement la spécification formelle dont il "prétend" être la réalisation.
Une méthode formelle peut être définie comme étant le processus intégrant ces tâches caractéristiques ainsi que certaines tâches induites comme, par exemple, la génération des preuves à effectuer ultérieurement lors de la vérification formelle, à partir des spécifications.
But du cours : Familiariser les étudiants avec des logiques formelles non classiques, avec les appro-ches axiomatique et syntaxique, introduire les concepts de consistance et de validité. Applications liées aux systèmes réactifs, épistémiques ou bases de données.
Documents joints à l'article
Cours Magistraux de Logique Modale
Cours de Lionel Marcé - Documents réalisés par des étudiants [année 2004-2005] - Taille du fichier: 535 ko
Documentation sur Lotrec
Proposée par son développeur, l’Université de Toulouse - Taille du fichier: 340 ko
Examen Méthodes formelles
[Année 2003] 2nd Semestre - Auteur : Lionel Marcé - Taille du fichier: 193.3 koExamen Méthodes formelles
[Année 2005] 2nd Semestre - Auteur : Lionel Marcé - Taille du fichier: 385 koExamen de Logique Modale
[Année 2003] 1er Semestre - Auteur : Lionel Marcé - Taille du fichier: 386.6 koExamen de Logique temporelle
[Année 2003] 2nd Semestre - Auteur : Lionel Marcé - Taille du fichier: 420.1 koLotrec et la méthode des tableaux
Documentation intéressante pour réaliser les TPs [en anglais] - Taille du fichier: 513.2 ko
Outil Kronos [version Linux]
Outil utilisé en 2ème partie des TP - Taille du fichier: 921.1 koOutil Kronos [version Windows]
Outil utilisé en 2ème partie des TP - Taille du fichier: 427.6 koOutil Lotrec [version Linux]
Outil utilisé en 1ère partie des TP - Java nécesssaire - Taille du fichier: 277 koOutil Lotrec [version Windows]
Outil utilisé en 1ère partie des TP - Java nécesssaire - Taille du fichier: 964 koRapport des TP de Logique Modale
Utilisation de Lotrec pour réaliser les TPs - Taille du fichier: 732.6 koRapport des TP de Logique Temporelle
- Taille du fichier: 336.8 ko
Introduction à UNIX
