Difference between revisions of "Courses/IMC"
From LRDE
(Created page with "{{Course |title=Introduction au Model checking |acronym=IMC |teacher=Adl |period=S5, Ing3 |audience=Majeure, CSI |optional course=non |module=Sciences Générales |prerequisit...") |
|||
(5 intermediate revisions by 3 users not shown) | |||
Line 1: | Line 1: | ||
{{Course |
{{Course |
||
+ | |visible=No |
||
|title=Introduction au Model checking |
|title=Introduction au Model checking |
||
|acronym=IMC |
|acronym=IMC |
||
|teacher=Adl |
|teacher=Adl |
||
|period=S5, Ing3 |
|period=S5, Ing3 |
||
− | |audience=Majeure, |
+ | |audience=Majeure, RDI |
+ | |exam type=QCM |
||
+ | |duration=14h |
||
|optional course=non |
|optional course=non |
||
|module=Sciences Générales |
|module=Sciences Générales |
||
|prerequisites=ALGO |
|prerequisites=ALGO |
||
|objectives=Ce cours introduit la vérification formelle en générale et les techniques de model checking en particulier. L'étudiant y découvre des logiques temporelles, différents automates représentant des mots des longueur infinie, ainsi que des techniques pour manipuler ces objets. |
|objectives=Ce cours introduit la vérification formelle en générale et les techniques de model checking en particulier. L'étudiant y découvre des logiques temporelles, différents automates représentant des mots des longueur infinie, ainsi que des techniques pour manipuler ces objets. |
||
+ | |content=* Introduction de la vérification formelle et du model checking* Diagrammes de décision binaires (BDD)* Logique temporelle à temps arborescent (CTL) et vérification à l'aide de BDD* Diagrammes de décision hiérarchiques (SDD)* Logique temporelle à temps linéaire (LTL) et passage vers les automates de Büchi* Test de vacuité d'un automate de Büchi* Lutte contre l'explosion combinatoire de l'espace d'état* Hypothèses d'équité et automates de Streett* Introduction à Spin. |
||
− | |content=* Introduction de la vérification formelle et du model checking |
||
⚫ | |||
− | * Diagrammes de décision binaires (BDD) |
||
− | * Logique temporelle à temps arborescent (CTL) et vérification à l'aide de BDD |
||
− | * Diagrammes de décision hiérarchiques (SDD) |
||
− | * Logique temporelle à temps linéaire (LTL) et passage vers les automates de Büchi |
||
− | * Test de vacuité d'un automate de Büchi |
||
− | * Lutte contre l'explosion combinatoire de l'espace d'état |
||
− | * Hypothèses d'équité et automates de Streett |
||
− | * Introduction à Spin. |
||
⚫ | |||
⚫ | |||
The Spin Model Checker: Primer and Reference Manual. Gerard J. Holzmann. Addison-Wesley. |
The Spin Model Checker: Primer and Reference Manual. Gerard J. Holzmann. Addison-Wesley. |
||
⚫ | |||
}} |
}} |
Latest revision as of 19:27, 4 February 2020
Titre |
Introduction au Model checking |
---|---|
Sigle |
IMC |
Enseignant | |
Période |
S5, Ing3 |
Public |
Majeure, RDI |
Contrôle |
QCM |
Durée |
14h |
Optionnel |
non |
Module |
Sciences Générales |
Prérequis |
ALGO |
Objectifs |
Ce cours introduit la vérification formelle en générale et les techniques de model checking en particulier. L'étudiant y découvre des logiques temporelles, différents automates représentant des mots des longueur infinie, ainsi que des techniques pour manipuler ces objets. |
Plan |
|
Documentation |
|
Support | |
Journaux |