Interprétation d'un modèle de sécurité

Cet article decrit une application des methodes formelles dans le cadre du developpement d'un produit de securite. Le travail realise vise a permettre une evaluation de la securite selon les criteres ITSEC. Pour cela un modele formel de securite a ete developpe. Ce modele a ete decrit et verifie a l'aide de la methode B. Puis il a ete mis en correspondance avec les specifications du produit. Ce travail d'interpretation du modele a permis de guider la conception des fonctions de securite du produit.