Abstract FR:

La méthode b est, actuellement, utilisée essentiellement pour le développement de systèmes de sécurité. De cette pratique, il ressort, surtout si l'objectif est de contrôler le respect des exigences de sécurité, le besoin d'adapter le cycle de vie, et d'y associer un support méthodique. Le logiciel critique, plus spécialement celui dédie a des systèmes de contrôle-commande doit être conçu en séparant les besoins de sécurité de ceux de fonctionnement. L'originalité de la démarche méthodique proposée dans cette thèse est de conforter cette séparation tout en s'inscrivant dans la continuité de l'analyse système. Les contraintes concernant le logiciel sont formalisées dans l'analyse préliminaire puis constituent les éléments structurants de la modélisation formelle. Cette méthode fournit la traçabilité précise correspondant aux exigences de développement du logiciel critique en tirant profit de la technique de vérification formelle inhérente a la méthode b. Un cycle de développement adapte a pu s'en déduire. De plus, l'analyse préliminaire à la spécification formelle présente l'avantage de fournir aux experts du domaine d'application, un document de support pour la validation du logiciel. L'étude de cas klv#1 intégralement formel, logiciel critique, analyse de sécurité, guide méthodique.