Systèmes de transition
- Teaching language : français
- Code : N8EN08A
In brief
Objectives
- Formally represent an isolated / autonomous computer system and its executions through the notion of transition system.
- Specify the behavioral properties of such a system in a temporal logic.
- Understand the relation of refinement between specification and implementation, through the notion of module.
- Use a formal modeling and automatic verification tool (TLA+) to illustrate these concepts and verify the properties of the systems.
Description
- Transition systems. Traces and executions.
- Concept of fairness in executions
- Specification in temporal logics: Linear Temporal Logic and Computational Tree Logic.
- Introduction to model verification techniques
Bibliography
Specifying Systems (L. Lamport - Addison-Wesley)
Pre-requisites
Mathematical Tools for Computer Science. Concurrent Systems. Automata. Logic and proofs
Session 1 ou session unique - Contrôle des connaissances
| Modalité | Nature | Coefficient | Remarques |
|---|---|---|---|
| CT (contrôle terminal) | Oral/Ecrit | 100% | Examen Systèmes de transitions |
Session 2 - Contrôle des connaissances
| Modalité | Nature | Coefficient | Remarques |
|---|---|---|---|
| CT (contrôle terminal) | Oral/Ecrit | 100% | Examen Systèmes de transitions |
Contact(s)
QUEINNEC PHILIPPEPlaces
- Toulouse
