Commentaires

Diaporama

Plan

1	Exploration implicite et explicite de l’espace d’états atteignables de circuits logiques Esterel
2	Plan
3	L’approche réactive synchrone
4	Esterel
5	Automates explicites
6	Circuits
7	Automates vs. Circuits
8	Automates vs. Circuits
9	Vérification formelle par observateur
10	Calcul d’espace d’états atteignables
11	Calcul d’espace d’états atteignables
12	Diagrammes de Décisions Binaires (BDDs)
13	Diagrammes de Décisions Binaires (BDDs)
14	Diagrammes de Décisions Binaires (BDDs)
15	Diagrammes de Décisions Binaires (BDDs)
16	Diagrammes de Décisions Binaires (BDDs)
17	Calcul d’espace d’états avec des BDDs
18	Plan
19	Réduction du nombre de variables
20	Inputization et abstraction : exemple
21	Sur-approximation
22	Sur-approximation
23	L’arbre de sélection Esterel
24	Notre vérificateur formel : evcl
25	Plan
26	Calcul d’espace d’états atteignables
27	Calcul d’espace d’états par énumération
28	Génération d’automates
29	Génération d’automates
30	Application à la vérification formelle
31	Vérification formelle – expérimentations
32	Génération de séquences de tests exhaustives
33	Génération de séquences de tests exhaustives
34	Couverture d’états – Expérimentations
35	Conclusion
36	Perspectives