L’utilisation des logiciels devient de plus en plus fréquente dans notre quotidien. Ces logiciels sont exposés à plusieurs risques parfois élevés lorsqu’il s’agit des applications dans un domaine critique – tel que le transport et la médecine – où une erreur pourra coûter des vies. Pour cette raison, il est important de considérer la qualité correction lors du développement de tels logiciels afin d’éliminer ces risques. Cela peut être réalisé tôt dans le cycle de développement en utilisant des méthodes formelles et dépend de la qualité du document d’exigences du client. Grâce à la technique de raffinement, l’utilisation de méthodes formelles permet l’obtention des systèmes dits corrects-par-construction. Ces méthodes favorisent l’expression des propriétés importantes telles que la vivacité ou l’absence de blocage et la terminaison. Combler l’écart entre les exigences et leurs spécifications formelles est très important pour assurer un développement homogène. Dans ce séminaire, nous élaborons les idées suivantes :
- L’importance de garder une trace des exigences des clients tout au long du processus de développement : à tout moment, l’état du développement est accessible et décrit par un triplet <Cahier des charges, Glossaire, Spécification formelle> ;
- Les avantages de l’utilisation des méthodes formelles pour le développement des systèmes critiques sans erreurs et l’importance des outils existants pour accomplir les tâches de : gestion des exigences, construction des modèles formels, leur vérification et leur validation ;
- La réutilisation des modèles génériques ou patrons pour semi-automatiser le développement en gardant des liens avec les exigences des clients et
- La validation au fur et à mesure du développement des modèles formels. C’est un processus rigoureux qui commence dès l’analyse des exigences et continue tout au long du développement.
Notre approche est appliquée sur des études de cas de systèmes critiques telles que la machine d’hémodialyse et le train d’atterrissage d’un avion. Ces deux applications ont été proposées comme études de cas dans la conférence ABZ des années 2014 et 2016. Notre présentation sera guidée par l’exemple de la machine d’hémodialyse.