Vérification de spécifications de logiciel à l'aide d'un modèle et de propriétés de sécurité
BIED-CHARRETON ; CHOPARD-GUILLAUMOT
Type de document
COMMUNICATION AVEC ACTES NATIONAL (ACTN)
Langue
francais
Auteur
BIED-CHARRETON ; CHOPARD-GUILLAUMOT
Résumé / Abstract
LES SPECIFICATIONS D'UN LOGICIEL DOIVENT IMPERATIVEMENT ETRE SANS ERREUR CE QUI IMPLIQUE QU'ELLES DOIVENT ETRE VERIFIEES AVANT LES PHASES DE DEVELOPPEMENT ET DE CODAGE. L'INRETS A CONSTATE QUE LE LANGAGE SYNCHRONE LUSTRE PERMET TRES FACILEMENT DE TRADUIRE LES SPECIFICATIONS DES LOGICIELS DES SYSTEMES DE CONTROLE-COMMANDE FERROVIAIRES; ON OBTIENT AINSI UN MODELE AUQUEL ON ADJOINT DES PROPRIETES DE SECURITE. IL CONVIENT ALORS D'EFFECTUER UNE CAMPAGNE INTENSIVE DE SIMULATION CORRESPONDANT A UN MAXIMUM DE CAS DE FONCTIONNEMENT NOMINAUX OU DEGRADES DE L'ENVIRONNEMENT. L'INRETS A DONC DEVELOPPE UN OUTIL QUI ENVOIE DES SCENARIOS A L'ENTREE DU MODELE. CETTE METHODE ET CES OUTILS ONT ETE APPLIQUES A UNE FONCTION D'UN LOGICIEL DE SYSTEME DE SIGNALISATION FERROVIAIRE. L'OUTIL A PERMIS DE VERIFIER QUELQUES PROPRIETES FONDAMENTALES ET D'ASSISTER L'EXPERT DANS LA RECHERCHE DE SCENARIOS COMPLEXES.
