58 lines
2 KiB
Markdown
58 lines
2 KiB
Markdown
- modèle : représentation mathématique
|
|
- vérification : algorithme fournissant une preuve adaptée
|
|
|
|
## modèle
|
|
|
|
- système de transitions
|
|
- machine à état, avec des états non désirés
|
|
|
|
- synchronicité
|
|
- synchrone
|
|
- opérations sur tous les circuits sont organisées par une seule horloge de manière granulaire
|
|
- physiquement, le temps de propagation des signaux est bien inférieur à la période de l'horloge
|
|
|
|
- asynchrone
|
|
- des signaux peuvent se propager entre circuits avant la fin d'un changement d'état d'un circuit
|
|
- comporte des signaux indépendants et des verroux de synchronisation
|
|
- exemple : échanges réseau, composants à plusieurs horloges
|
|
|
|
- transition
|
|
- synchrone : une transition change tous les circuits
|
|
- asynchrone : une transition ne concerne et change qu'un circuit
|
|
|
|
### automate fini
|
|
|
|
- ensemble d'état
|
|
- ensemble de transitions
|
|
- un 'langage' qui sert d'entrées système
|
|
- une phrase qui est une entrée précise
|
|
|
|
- les état finaux serviront de cas d'erreurs, nous cherchons donc à vérifier que l'état final ne peut pas être atteint
|
|
|
|
- on peut différencier des langages pour analyser un sous ensemble de cas à vérifier lorsqu'on intègre de nouvelles entrées
|
|
- faire le produit d'automates A et B, c'est former l'automate qui prends comme transition les tuples des entrées de A et B
|
|
|
|
#### Exemple
|
|
|
|
propriété : tout A est suivi d'un B dans le langage (b+ab)*
|
|
|
|
|
|
### structure de kripke
|
|
- défini par une liste de propositions
|
|
- ensemble de variables propositionnelles (équation booléennes)
|
|
- ensemble d'états
|
|
- ensemble de transitions
|
|
- pour chaque état, l'ensemble des propositions qui sont vérifiées par cet état
|
|
|
|
#### traces
|
|
- suite d'évènements / états
|
|
|
|
- est un ensemble mathématique de la forme:
|
|
- toutes les suites avec :
|
|
- e_0 est un état de départ
|
|
- (e_n, e_n+1) est une transition existante
|
|
|
|
- arborescence
|
|
- arbre des états possibles en arrivant à chaque état en partant de l'état initial
|
|
- racine : état de départ
|
|
- enfants d'un neud : états accessibles depuis cet état
|