blondimi/igl752_a20

IGL502/712 (A20): fichiers complémentaires

IGL502/752 (A20)

Fichiers complémentaires du cours IGL502/752 – Techniques de vérification et de validation de l'Université de Sherbrooke (automne 2020).

Outils

Spin

• Page officielle
• Interface Web (Chalmers University of Technology)

NuSMV

• Page officielle

LoLA

• Page officielle

PRISM

• Page officielle

igl752_a20's Issues

Suggestions mineures pour les notes (3)

Page 83: deuxième paragraphe

où v décrit/est le contenu du reste de la pile

Page 84: deuxième ligne

mettre l’emphase sur le système dont auquel nous faisons référence

Page 84: dernier paragraphe

Par soucis souci technique

Page 85: dernier paragraphe

Un Une telle procédure

Page 88: Figure 8.3 -> Il manque une accolade pour fermer l'ensemble décrit

L'explication pour l'assertion est en contradiction avec les notes. Je crois qu'il s'agit d'une erreur d'inattention lors de l'enregistrement et que les notes sont correctes.

Suggestions mineures pour les notes

Page 11: Entre les deux encadrés

Dans le but de raisonner

Page 16: Fin de la section 2.6.1

afin de stocker une chemin

Corrections aux notes

Page 4: Dans l'encadré en bas de page, si on parle bien du système T1 de la page 1, le chemin s1->s2->s1->s2 utilise une transition non définie (s2->s1).
Page 30: Dans le premier encadré, on mentionne que

la seule manière de lire le premier a [de l'automate B] consiste à se déplacer dans l'état q

Cependant, on peut aussi se déplacer dans l'état r. Le problème pour le mot abaaa... survient plutôt après le b.

Suggestions mineures pour les notes (2)

Page 57: deuxième paragraphe

ce-dernier -> ce dernier

Page 58: deuxième paragraphe

Une formule CTL est dites

Page 59: deuxième paragraphe de la section 6.2.1

Ainsi, s0 |= ∃XΦ ssi s0 possède au moins un successeur

Page 59: premier paragraphe de la section 6.2.2. Je ne suis pas certain de la formulation exprimée mais dans la vidéo 6c on indique que s0 doit d'abord satisfaire Φ. Je ne sais pas à quoi on fait référence pour ce s mais il semble qu'il devrait aussi satisfaire Φ.

Ainsi, s ∈ T ssi s |=Φ et il existe un état s′ ∈ Post(s) [...]

Suggestion mineure pour les notes (4)

L'encadré de la page 12 semble inverser l'ordre entre les opérateurs de satisfaction d'une formule ( p |= sigma plutôt que sigma |= p). La notation pour le reste des notes du chapitre semble être un mot satisfait une formule et non l'inverse.