Formal design

School / Prep
ENSEIRB-MATMECA

Internal code

EI9IF311

Description

The aim of this course is to learn how to use formal modeling as a tool for detecting bugs and proving computer systems or programs.

CIIntegrated Courses24h
TIIndividual work24h

Mandatory prerequisites

Finite automata, logic, graph algorithms.

Syllabus

- Introduction to critical software issues
- Formal modeling: transition systems and the PlusCal high-level language
- Formal specification in Linear Temporal Logic (LTL)
- Advanced specification in TLA+
- Modeling concurrent systems: atomicity and fairness
- Model-checking algorithms
- Abstraction and refinement

Exercises based on Leslie Lamport's TLA/TLC platform

Bibliography

Presentations and exercises (see online course)

Initial assessment / Main session - Tests

Type of assessment	Type of test	Duration (in minutes)	Number of tests	Test coefficient	Eliminatory mark in the test	Remarks
Final inspection	Written	90		0.6		without document without calculator
Continuous control	Continuous control			0.4

Second chance / Catch-up session - Tests

Type of assessment	Type of test	Duration (in minutes)	Number of tests	Test coefficient	Eliminatory mark in the test	Remarks
Final test	Written	30		0.6		without document without calculator