Search Log in FR EN

Vérification formelleEA Sécurité Fondamentale (STI)

FISEFISA STI Semester 8 EA Fundamental Security Machine translation

Formal Verification

Teaching unit EA Fundamental Security · S08T_SFO1  |  EC Code S08A_SF1-2
Course on Celene
6ECTS (EU)
1Coefficient
21:20Hours

Séquencement

C TD C TD C TD C TD C TD C TD C TD C TD

Learning objectives

  • Mastering and understanding a verification technique
  • Logically model the expected properties of a system.

Prerequisites

ModuleTeaching unitSemester
LogicProgramming PrinciplesS5
Language TheoryProgramming PrinciplesS5

Program

  1. Systems modeling and Kripke structure,
  2. Linear time logic (LTL) and automatons on infinite words,
  3. Tree Time Logics (CTL) and Fixed Point Calculation.
  4. Python implementation and resolution (using the tools provided)

Assessment

Final examination:

Authorized document: A sheet A4 R/V Physically handwritten individual.

The documents produced on a tablet and printed are acceptable only if the density of information is similar to what would have been obtained with paper and pencil.

Interros surprises / continuous control:

Any course session/TD/TP may give rise to a marked check. Absence not justified => 0/20.

References

  • Polycopy: link.

  • Schnoebelen, Philippe, "Software verification: techniques and tools of model-checking", Vuibert

Skills

4
Ref.VerbDescriptionLevel
C1_1recognizemodelable problems1
C1_1calculatepossible behaviour of the system2
C1_2describeformal system2
C2_1provecorrection of a system3

SecNumEdu Skills

SkillLecture hoursPractical hoursEntry levelExit level
Fundamentals4401
Security elements of functioning from the point of view of formal analysis: understand, express, and formalize absence of critical conflicts, famines, and other safety properties
Software development and software engineering (from a security perspective)4402
Formal analysis of competing programs: modeling systems, expressing specifications, and proving safety and security properties (Model-checking CTL, LTL)