 |
 |
 |
 |
 |
 |
 |
 |
 |
Validation formelle de la spécification d'un logiciel
OBJECTIFS DE LA METHODE 
La méthode de Validation Formelle de la spécification permet au Maître d'Ouvrage ou au Maître d'Œuvre d'avoir au plus tôt l'assurance de la complétude et de la cohérence des fonctionnalités portées par le logiciel décrites dans les spécifications du logiciel. Cette assurance est apportée par l'établissement du modèle formel de ces fonctionnalités et la démonstration sous forme de preuves mathématiques du respect des propriétés de sûreté des fonctions du logiciel dans le système.
(Cette démarche est "Hautement Recommandée" (HR) pour les logiciels de niveau SIL 4 dans la norme CEI 61508).
DEMARCHE
1- A partir de la documentation du système et du logiciel, mise en œuvre de l'outil AGFL® pour obtenir le modèle fonctionnel orienté sûreté (chemins fonctionnels et modèle des flux).
2- A l'aide de l'outil AGFL® (inversion des chemins du modèle fonctionnel orienté sûreté), réalisation du modèle formel en langage PVS.
3 - A partir de la documentation du système et du logiciel, identification des propriétés de sûreté à valider et traduire ces propriétés en langage PVS.
4 - A l'aide de l'outil PVS, réalisation de la preuve des propriétés de sûreté sur le modèle formel.
RESULTATS
- Ensemble de remarques, sous la forme de Fiches d'Avis, sur la complétude et la cohérence des spécifications,
- Modèle formel des fonctionnalités du logiciel, pour la définition des scénarios de tests de Validation (tests fonctionnels, de tolérance aux fautes),
- Dossier de Preuve formelle mathématique des propriétés de sûreté respectées par le logiciel.
