Chemin à avoir en tête :

Modèle formelle (automate) représente un système \RA Extraire des scripts (C++) de tests \RA Exécuter sur un système réel

flowchart TD
    A -- Extraction (DS, UIO, W) --> B
    B -- Détection erreurs --> C
    A -- conf? --> C

A((Spécification système))
B[Scripts Tests TCCN3]
C[(SUT)]

État : Ensemble de variables valuées ou non valuées de l’ensemble du système.
État équivalent : même input = même output

Hypothèses sur l’automate

• Complet (input enable) : dans chaque état de l’automate, je dois traiter tous les inputs possibles du système (évitant le blocage).
• Déterministe : (examen)

---
title: Non-déterministe observable
---
flowchart TD
    1 -- a/x --> 2
    1 -- a/y --> 3

1((1))
2((2))
3((3))

Minimal : (examen) Il faudra fusionner des états équivalents, osef des états ; juste les mêmes sorties
Strongly connected : Dans n’importe quel état, je peux revenir à l’état initial.
\RA si on n’a pas cette propriété, il faut trouver une justification, par exemple une ATM mange une carte, on ne peut pas revenir en arrière (raison de sûreté).
Pas d’états transients : État géré par le temps (par exemple au bout d’un certain temps quand on charge une page, on a une erreur 404 si elle n’est pas trouvée)

Dans chaque exercice de l’examen, il y aura une hypothèse violée.

Type erreur \neq Verdict

Dans le système automate qui représente le système sous test, il peut être aussi moche que possible (deadlock, livelock, non déterministe, non minimal…) contrairement à la spec.

DS

état initial	suite entrée	suite sortie
s1	a	0
s2	a	1
s3	a	0
Pas distinguant \RA pcq a qui donne 0 apparaît 2x. : donc on doit essayer avec autre chose, par exemple b

état initial	suite entrée	suite sortie
s1	b	1
s2	b	1
s3	b	0
Toujours pas distinguant, on essaie ab, qui lui est distinguant (cf. slides)

Parfois, il n’existe pas.

flowchart RL
    1 -- t1: a/0 --> 1
    2 -- t2: a/0 --> 1
    2 -- t3: b/1 --> 2
    3 -- t4: b/1 --> 2
    3 -- t5: a/1 --> 3
    1 -- t6: b/0 --> 3

1((s1))
2((s2))
3((s3))

On revient tout le temps sur s1 en partant de s1 et s2, on revient tout le temps sur s2 en partant de s3 et s2, ils sont indistinguables, en commençant la séquence par a ou par b, on arrivera toujours sur un état commun indistinguable.

reset/null : démarrage du système, ce qui suit est l’état initial.

W

Existe toujours.

UIO

Parfois ils n’existent pas (cf. UIO partiel).

On cherche des cas uniques directement sans faire de tableau :
UIO(S2) = a/1
UIO(S3) = b/0
UIO(S1) = a/0 b/1