Objectifs

L’objectif du stage est une initiation à la modélisation, l’implantation et la validation formelle des logiciels temps réels.
La formation comporte un apprentissage :
- des concepts de modélisation de logiciels basés sur des réseaux de processus communicants. Les formalismes utilisés durant ce cours sont, d’une part, le langage SDL (Specification Description Language) et, d’autre part, un langage basé sur des automates temporisés : présentation des deux formalismes, édition des modèles, simulation, illustration sur des cas d’étude industriels.
- des concepts d’implantation des modèles sur une cible embarquée : carte équipée d’un noyau temps réel microC-OSII : étude des caractéristiques du noyau, principe de génération de code C, illustration d’implantation sur cette cible.
- des principes de vérification formelle d’exigences sur les modèles : présentation des logiques formelles temporelles, formalisation et vérification des propriétés, illustration sur de nombreux exemples.

Niveau du stage

Base

Pré-requis
Connaissance du langage C.

Pédagogie
Le stage comporte des séances de cours illustrées par de nombreux exercices et travaux pratiques sur machine.

Documents fournis aux stagiaires
Supports de cours (polycopié, sujets et corrigés des travaux pratiques).

Dispositif d’évaluation
Evaluation à chaud en fin de formation par les stagiaires. Transmission au client, du compte-rendu d’évaluation et des feuilles d’émargement en complément de la facturation. Les attestations de stage sont remises directement aux stagiaires à la fin de la session de formation. Les stagiaires ou le responsable Formation Continue sont susceptibles de recevoir par mail, un « questionnaire de satisfaction à froid » quelques mois après le déroulement de la formation.

Programme détaillé

• Principe des modèles à processus communicants
• Modélisation SDL, simulation, validation
• Principe des modèles à processus communicants temporisés
• Modélisation avec un langage à automates temporisés, simulation
• Etude du noyau microC-OSII
• Génération de code C et implantation sur carte temps réel
• Spécification d’exigences formelles, logiques temporelles
• Vérification formelle de propriétés
• Illustration avec un outil de vérification.