- 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