Code
IGSE CSC 7204
Level
MSc
Graduate
PostGraduate
Semester
Spring
Domain
Informatique
Program
Master of Science
Language
Anglais/English
ECTS Credits
2
Class hours
24
Workload
48
Program Manager(s)
Department
- Réseaux et Services de Télécom
Organisation
Cours/TD/TP/projet/examen : 24Learning objectives
The purpose of formal methods is to enable the construction of large, highly reliable software. Formal Methods is a generic term for system design, analysis, implementation and verification methods that are described and used with mathematical rigor.
In particular formal specification techniques allow for the construction of automated verification tools that can perform tests on specifications and corresponding code to find errors in implementations (and also in requirements and models)
The course will focus on verification by testing and by proving.
Prerequisites
A standard background on programming and logics (helpful but not required)
Keywords
software engineering – formal methods – design by contract – specification - verification – proof – structural testing – conformance testing -
Content
Introduction to software engineering and formal methods
Propositional and first order logics (syntax, semantics, deduction) – Notion of contract – Axiomatic specification – Hoare logics – Verification of functional properties Introduction to model based verification and design
Structural testing: path predicates – coverage – generation of test cases -oracles - Model based testing - Conformance testing
Evaluation
Project or exam