La validation dans les premières étapes du processus de développement

International audienceImproving the quality of a system begins by the requirements elicitation. Our goal is to take into account the validation since the understanding of the requirements and all along the development of their Event-B specification. Our challenge is to bridge the gap between requirements, those of the client, and the specification, that of the computer scientist. We make explicit the interactions between the requirements and the specification under construction. The validation is studied for formal models with regard to the requirements. The verification may detect incoherences and contradictions in both requirements and formal specification. The Rodin platform tools are important all along the development to improve the quality and the documentation of the system. Rodin and the ProR plugin allow us to manage the trace of the requirements and their specification. The documentation and the feedback of the different used tools for the validation and verification are available at any time of the development. We illustrate our approach to the case study of an aircraft landing system.L'amélioration de la qualité d'un système commence par l'expression de ses besoins en langage naturel. Notre objectif est de prendre en compte la validation dès la compréhension des exigences et tout au long du développement de la spécification en Event-B. Pour combler l'écart entre le cahier des charges et sa spécification formelle, nous explicitons les interactions entre ces deux mondes. La validation est étudiée pour les modèles formels relativement aux exigences. La vérification permet de détecter des incohérences et des contradictions dans le cahier des charges et dans la spécification Event-B. La place des outils disponibles, notamment avec la plateforme Rodin, est importante tout au long du développement, améliorant sa qualité et sa documentation. Rodin et le plugin ProR permettent de gérer la trace des besoins en lien avec la spécification en cours de construction. L'ensemble des documents disponibles et les retours des outils de validation et vérification sont disponibles tout au long du développement. Notre approche est illustrée par l'étude de cas d'un système de contrôle du train d'atterrissage d'un avion