1 - DÉVELOPPEMENT DU LOGICIEL

• 1.1 - Réalisation d’une application logicielle
  Figure 1 - Étapes de réalisation d’un logiciel
• 1.2 - Processus de développement
  Figure 2 - Trois cycles de vie possibles d’une application logicielle Figure 3 - Cycle en « V » Figure 4 - Cycle en « V » incluant la spécification des tests
• 1.3 - Avantages/désavantages
  Figure 5 - Cycle de gestion des anomalies
• 1.4 - Vérification et validation
  Figure 6 - Problématique du développement logiciel Figure 7 - Vérification et validation sur le cycle en « V » Figure 8 - Vérification Figure 9 - Validation Figure 10 - Identification, modélisation et analyse Tableau 1 - Table A.5 de la norme CENELEC EN 50128:2011

2 - NORMES FERROVIAIRES

• 2.1 - Référentiel CENELEC
  Figure 11 - Normes applicables aux systèmes ferroviaires
• 2.2 - Choix du SSIL
• 2.3 - Structure de la norme CENELEC EN 50128
  Figure 12 - Structure de la norme CENELEC EN 50128:2011
• 2.4 - Cycle de développement de la norme CENELEC EN 50128
  Figure 13 - Cycle en « V » de la norme CENELEC EN 50128
• 2.5 - Bilan

3 - MÉTHODES FORMELLES, SEMI-FORMELLES, STRUCTURÉES ET TECHNIQUES FORMELLES

• 3.1 - Définitions
  Figure 14 - Exemple de modèle Simulink Tableau 2 - Nouvelle version de la norme CENELEC 50128:2011 – table A.17
• 3.2 - Méthode formelle versus technique formelle

4 - MISE EN ŒUVRE DES MÉTHODES FORMELLES LORS DE LA RÉALISATION D’UNE APPLICATION LOGICIELLE

• 4.1 - Spécification des exigences du logiciel
  Figure 15 - Environnement de l’application logicielle Figure 16 - Différents états applicables au logiciel Figure 17 - Élaboration de la spécification Figure 18 - Des exigences au code Figure 19 - Exemple de statique introduisant différents types de communication Figure 20 - Modèle B explicitant la propriété P Figure 21 - Formalisation des exigences Figure 22 - Formalisation des exigences Figure 23 - Exigences, modèle et vérification Tableau 3 - CENELEC EN 50128 – table A.2
• 4.2 - Architecture
  Figure 24 - Exemple d’architecture d’une application logicielle Figure 25 - Exemple de modèle UML Figure 26 - Exigences de l’architecture
• 4.3 - Codage
  Figure 27 - Exemple de code Ada Figure 28 - Exemple de faute en C Tableau 4 - CENELEC 50128:2001 – table A.15 Tableau 5 - Nouvelle version de la norme CENELEC 50128:2011 – table A.15 (partielle) Tableau 6 - Quelques règles MISRA-C:2004 Tableau 7 - CENELEC EN 50128:2011 – table A.12 Tableau 8 - CENELEC EN 50128:2011 – table A.23 Tableau 9 - IEC 61508 [IEC 98 – partie 3] – table A.3
• 4.4 - Génération de code
  Figure 29 - Analyse formelle d’un code Figure 30 - Activité de vérification formelle du code
• 4.5 - Interprétation abstraite
  Figure 31 - Analyse formelle d’un code

5 - RÉALISATION METTANT EN ŒUVRE LES APPROCHES FORMELLES

• 5.1 - Intégration des méthodes formelles dans le cycle de réalisation d’une application logicielle
  Figure 32 - Processus classique Figure 33 - Processus formel dès la spécification Figure 34 - Processus formel débutant au niveau conception Figure 35 - Processus formel débutant au niveau conception Figure 36 - Remplacement des tests par des simulations
• 5.2 - Vers une approche centrée modèle
  Figure 37 - Processus prenant en compte les modèles

6 - LOGICIEL PARAMÉTRABLE

Tableau 11 - Table A.11 de la norme CENELEC EN 50128:2011 Tableau 12 - Combinaisons pour réaliser un processus de production des données

7 - QUALIFICATION

• 7.1 - Besoins
• 7.2 - Difficultés
  Figure 46 - Preuve de conformité d’un outil

8 - CONCLUSION

9 - GLOSSAIRE