Parcours IL / Orientation IL & MFLS
Le développement de systèmes informatiques requiert des techniques permettant de garantir la qualité du système produit ou maintenu et sa conformité à un cahier des charges en vue de sa certification. Ce cours vise à acquérir les concepts et les techniques de modélisation et de vérification au travers de méthodes s’appuyant sur des cadres formels comme Event-B et TLA+, et sur un savoir-faire acquis au cours d’études de cas.
Au niveau de la modélisation, deux concepts fondamentaux sont mis en avant, l’abstraction et le raffinement, et le cours montre comment les outils de preuve automatiques ou interactifs facilitent ce processus de développement et mettent en œuvre la méthodologie de développement dite incrémentale.
Le cours introduit également les principaux concepts et techniques de vérification algorithmique qui visent la vérification automatique d’algorithmes et systèmes informatiques, en particulier concurrents et distribués. S’appuyant sur des bases logiques et algorithmiques, ces techniques sont largement utilisées pour la validation de systèmes embarqués, de protocoles de réseaux et d’algorithmes répartis.
Le cours s’appuie sur des études de cas d’applications réelles comme les bases de données réparties ou les CPS (cyber-physical systems), …
Prérequis
- Connaissances de base en logique, algorithmique, programmation et systèmes informatiques.
Acquis d’apprentissage
- Familiarisation à des environnements formels de développement.
- Éléments d’ingénierie système formelle.
- Maîtrise de la technique de raffinement de modèles.
- Principe de conception correcte par construction.
- Systèmes de transitions et logiques temporelles.
- Algorithmes de vérification de formules LTL ou CTL pour des systèmes discrets et temporisés.
- Algorithmes de model checking symbolique par BDD ou techniques SAT.
Compétences visées
- Concevoir et développer des systèmes logiciels sûrs et sécurisés.
- Intégrer des méthodes et techniques formelles de modélisation, d’analyse, de vérification et de validation dans le processus de développement de logiciels critiques.
- Modéliser un algorithme ou système concurrent, ou réparti éventuellement temporisé.
- Exprimer des propriétés de ces systèmes par des formules logiques.
- Utiliser sur des cas concrets des outils mettant en œuvre la vérification algorithmique.