Course Syllabus 2012/2013
 
PDF Extract Anglais
 Français
 index
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 :
2.00
Teacher(s) :
HERBRETEAU Frédéric - Responsible
WALUKIEWICZ Igor
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)
Evaluation :
Homework + academic defense in english
Document(s) :
Given in classroom
Keyword(s) :
Specification, Modeling, Model-checking, Formal design of software
Online course :
http://www.enseirb.fr/~herbrete/IF311/