Descriptif

Formal methods of system design means using mathematics to develop error-free systems. The mathematics needed is not complicated; it's just basic logic. The word "formal" means the use of a formal language, so that the system's operating logic can be machine checked.

This course is an introduction to the vast world of formal methods. It provides frameworks within which students can specify, develop, verify, and prove systems in a systematic, rather than ad hoc manner.

The course begins with review of propositional logic and predicate logic. Then we look at formal specifications, to cover set theoretic specification methods via B method, temporal specification via temporal logic and automata theory. The training includes both theoretical and practical parts. Each student will carry out an investigation of an existing formal verification system, applying it to a suitable problem of the student’s choice. Among possible projects will be the formal verification of problem solutions such as designing control systems, designing algorithms, or sophisticated data structures.