Course Syllabus 2013/2014
PDF Extract Anglais
Module : IF311
Title :
Formal design of software
Number of hours :
Combined lecture and tutorial classes : 24.00 h
Individual work : 24.00 h
ECTS credits :
Evaluation :
S1: ET(1h30,E,sd,sc) x0.6 + CC x0.4; S2: ET(30m,O,sd,sc) x0.6 + rep(S1) x0.4   Detail of the nomenclature used for the creation of the evaluation code
Teacher(s) :
HERBRETEAU Frédéric - Responsible
Level :
third year module
Abstract :
Formal specification and modeling of software. Model-checking as a proof technique.
Plan :
    • Introduction to critical software
    • Formal modeling: transition systems and the high-level language PlusCal
    • Formal specification in Linear Temporal Logic (LTL)
    • Advanced specification in TLA+
    • Modeling concurrent systems: atomic actions and fairness
    • Model-checking algorithms
    • Abstraction and refinement

      Exercices with Leslie Lamport's TLA/TLC platform
Prerequisite :
    • Finite automata (IF114)
    • Logic, proof of programs (IF105)
Document(s) :
Given in classroom
Keyword(s) :
Specification, Modeling, Model-checking, Formal design of software
Online course :