Spécifications functionnelles
Christophe Delord
http://fun.cdsoft.fr ~ https://twitter.com/CDSoftX
Dimanche 28 Février 2016
Les principaux problèmes dans la vie de tous les jours d’un ingénieur viennent souvent des spécifications logicielles. Le but de la méthode FUN de CDSoft est assez simple :
Les spécifications doivent être : |
mais aussi : |
|
|
Je suis ingénieur en informatique. Je travaille en informatique et particulièrement dans l’industrie aéronautique depuis 17 ans… à écrire des logiciels mais pas toujours dans de bonnes conditions:
J’ai ainsi accumulé quelques idées pour faire différement.
J’ai aussi une passion pour le logiciel libre et le partage des bonnes idées.
Pour en savoir plus sur moi: http://cdsoft.fr
Ce livre sera une opportunité de:
Je serais donc flatté si vous décidiez d’aider ce projet et de participer au financement de cette aventure.
J’espère pouvoir travailler à temps partiel pour avoir plus de temps pour ce projet.
En retour vous recevrez une version électronique du livre.
Mon point de vue est que la plupart des spécifications, même pour des systèmes critiques, sont écrites :
Voyons ce qui ne va pas et ce qui peut être fait pour améliorer la situation…
Un langage naturel est pratique
Mais un logiciel critique (ou non) doit être décrit de manière non ambigue. Les ambiguités conduisent à des interprétations multiples et contradictoires en pratique.
Vous ne pouvez pas maitriser un format propriétaire fermé:
Un format propriétaire est le plus mauvais choix que l’on puisse faire pour écrire un document, en particulier lorsqu’il doit être conservé pendant longtemps (par exemple 80 ans dans l’industrie aéronautique)
Certains formats, propriétaires ou non, ne sont pas adaptés, en particulier les documents issus de suites bureautiques:
Pour écrire du texte, vous avez besoin d’un éditeur de texte :
L’avantage d’écrire des spécifications functionnelles est qu’elles sont exécutables. Cela signifie qu’elles peuvent être exécutées pour :
C’est en quelque sorte la méthode formelle du pauvre…
Le concept de specifications exécutables peut être appliqué aux tests !
Parler de plans de test exécutables peut sembler étrange puisque la raison d’être d’un test est d’être exécuté pour vérifier une propriété…
Il ne devrait pas être nécessaire de dire “plan de test exécutable”.
“Plans de test exécutables” n’est pas étrange. Cela devrait être naturel pour tout le monde… Mais les testeurs procèdent la plupart du temps de cette manière:
Je vais montrer dans ce livre combien il est facile d’atteindre le même objectif avec des plans de test functionnels qui sont auto-exécutables et qui génèrent les rapports de tests eux-mêmes.
La suite présente une roadmap prévisionnelle, un plan du livre.
Le but principal est de montrer comment Haskell (et la programmation functionnelle en général) peut servir de langage de formalisation à plusieurs niveaux :
Et être appliqué à différents domaines :
Il sera utile de commencer par une introduction à la programmation fonctionnelle. Cette introduction sera très légère car il existe de nombreux cours et documentations sur le sujet.
Le livre insistera sur les points suivants et leurs intérêts :
Les systèmes temps réels de type réactif sont souvent des automates dont la principale activité est de modifier son état courant en fonction de stimuli externes.
La modélisation de tels systèmes dans un langage fonctionnel pur (sans effets de bord) peut sembler impossible mais nous verrons comment représenter le temps et les changements qu’il provoque sur un système réactif.
Cet exemple montrera les avantages d’un langage fonctionnel pur pour représenter des états, et surtout pour faire des raisonnements sur l’évolution des états dans le temps.
Applications avec un modèle temps réel :
Une autre modélisation de système réactif donnera lieu à une réalisation concrète : un robot arduino capable de percevoir son environnement et de réagir à quelques stimuli.
Modélisation d’un système complet : exemple classique du feux tricolore et de la circulation.
Ce projet est une réécriture d’une calculatrice écrite précédemment en Lua par CDSoft. L’idée est de réimplémenter cette calculatrice en Haskell proprement :
La norme ARINC 665 défini un standard pour le format de données chargeables sur un équipement. Cette norme est très utilisée en aéronautique.
La génération de ces loads est très critique puisqu’ils contiennent des exécutables et des données pour les calculateurs embarqués dans l’avion.
Une spécification functionnelle permet de :
L’idée clé est de décrire une exigence avec ses propriétés pour rendre l’implémentation directement testable à partir du formalisme de l’exigence.
À qui s’adresse ce livre et la méthode qu’il décrit ?
Cette méthode n’a ni la puissance de méthodes formelles comme Event-B ni la richesse (encore ?) d’outils comme SCADE ou Matlab Simulink. Ses intérêts sont :
Elle s’adresse donc à quiconque cherche un bon compromis entre puissance, efficacité, simplicité et coût.
Votre aide est la bienvenue…
Je pense que le financement participatif est une solution :
Suivez moi