Méthodes formelles pour le développement et la vérification de logiciels

Cet article présente les différents composants d'une méthode de développement de logiciel intégrée. Nous soulignerons la nécessité de fournir un cadre cohérent l'intégration des activités de spécification, d'implémentation et de vérification. L'usage de méthodes formelles sera étudié en montrant, l'importance de la sémantique dans la formalisation des techniques de développement ainsi que la nécessité de supporter un développement incrémental. L'incrémentalité est située au niveau de l'élaboration de la spécification et au niveau de la construction des programmes. Finalement nous présenterons une réalisation concrète de système de développement basé sur le formalisme CO-OPN que nous avons mené à l'EPFL, dont une partie est supportée par des outils intégrés dans l'environnement SANDS