PolyTech Course: Verification and Validation
("Vérification et Validation")
Cours:
This course gives an introduction to verification and validation techniques used in (large) software processes. It starts with techniques to combine conventional UML models with formal modeling techniques (covering invariants, pre- and postconditions). The latter were applied/exploited in techniques involving (black-box) unit tests, program-based tests, and deductive program verification based on Hoare-Floyd-calculi. In the lab-courses, the techniques were applied with concrete tools.
Goal: Getting practical experience with basic formal methods in modeling, verification and validation of software.
The course is given in english.
Links:
ecampus site
ecampus cours visio link (default)
group I visio link (default)
group II visio link (default)
jitsi visio link (reserve)
Material:
The material drawn from the course 2020 is tentative !
- C1 - 28.1.22 [13-30 - 15:30]: Introduction to SE, A Revision of the UML
- C2 - 2.2.22 [13:30 - 15:30]: Modeling Invariants and Contracts in UML and MOAL
- C3 - 2.2.22 [13:30 - 16:30]: Test I : Generalities, Dynamic Unit Test, Specification-based Test
- C4 - 09.2.22 [13:30 - 15:30]: White-Box Testing
- C5 - 23.2.22 [8:30 - 10:30]: Verification I (Hoare-Calculus)
- C6 - 16.3.22 [13:30 - 15:30]: Verification II (wp Calculus, Verifying Compilers),
TD groupes : (Dates: TBA)
- TD1 : Exercise 1
- TD2 : Exercise 2
- TD3 : Exercise 3
- TD4 : Exercise 4
- TD5 : Exercise 5
TP groupe : (Dates: TBA)
- TP1 : 16/02/2022 Exercise 1
- TP2 : 16/03/2022 Exercise 2