Modélisation des systèmes informatiques

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. Cette unité vise à acquérir les concepts et les techniques de modélisation au travers de méthodes s’appuyant sur un cadre formel comme Event-B et sur sur un savoir-faire acquis au cours d’études de cas. Il s’appuie sur le triptyque D,S->R où D est le domaine du problème, R désigne les exigences et S correspond au système à concevoir. 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 s’appuie sur des études de cas d’applications réelles comme le pacemaker ou les CPS (cyber-physical systems).

Pré-requis

  • Connaissances de base en logique, algorithmique, programmation et systèmes informatiques.

Acquis d’apprentissage

  • Apprentissage d’une méthode formelle Event-B et de son environnement Rodin.
  • Familiarisation à un environnement formel de développement comme Rodin, Atelier-B.
  • Maîtrise de la technique de raffinement de modèles.
  • Principe de conception correcte par construction.
  • Gestion de projet de modélisation par raffinement.
  • Éléments d’ingénierie système formelle.

Compétences visées

  • Modéliser un algorithme ou système concurrent, ou réparti éventuellement temporisé.
  • Organiser, analyser et développer un système informatique par raffinement et par preuve.
  • Élicitation de propriétés de correction ou d’exigences

Parcours IL / Orientation IL & MFLS