Pattern-oriented Formal Software Development

L'objectif de ce projet est de fournir une méthode pratique pour le développement efficace de logiciel correct.

Il est reconnu que ce sont les premières étapes du développement du logiciel qui sont cruciales pour parvenir à la meilleure adéquation entre les besoins exprimés et la réalisation proposée, et pour éliminer au maximum toute
source d'erreur. Ceci est particulièrement important pour les applications ``critiques'', tels que les systèmes
de contrôle des trains, où des erreurs peuvent entraîner la perte de vies humaines.

L'accent est donc mis tout d'abord sur une expression précise et non ambiguë des besoins dans les spécifications. Différentes approches sont proposées pour aller dans ce sens, avec leurs avantages et inconvénients respectifs.
Les spécifications formelles, par leur expression précise, conduisent à se poser des questions qui font progresser
dans la compréhension du problème à traiter. Un écueil demeure, c'est celui de la taille et/ou de la complexité,
qui rendent malaisée la compréhension synthétique et peuvent égarer dans la démarche. Notre approche est
d'utiliser les ``patterns'' pour aider à maîtriser la complexité des problèmes dans le démarche de spécification.
Les ``patterns'' (traduits par schémas ou patrons)proposent des familles de structures fréquemment rencontrées que
l'utilisateur est invité à ``essayer'' (quitte à les adapter) sur le problème à traiter pour ainsi bénéficier de concepts structurants en ``prêt à porter''. Les ``patterns'' [4] peuvent donc être vus comme un moyen élaboré de réutiliser des connaissances acquises par l'expérience.

Un ``problem frame''[8] est un schéma qui définit de manière intuitive une classe de problèmes identifiée en
termes de son contexte et des caractéristiques de ses domaines, de ses interfaces et des besoins.
C'est donc un ``pattern'' à utiliser dès le début de l'analyse d'un problème pour permettre de reconnaître des
structures utiles pour la compréhension.

Une méthode de développement de logiciel s'appuyant sur les ``patterns'' a été proposée dans [3] et développée également dans [2]. L'idée de cette méthode est d'associer à chaque instance de problem frame un schéma de spécification formelle correspondante qui puisse être instancié pour un problème concret.
Le langage de spécification à utiliser de préférence peut varier selon le problem frame choisi. Dans [3,2] cette idée a été illustrée en utilisant les langages de spécification formelle CASL [1], CASL-LTL [9], et LOTOS), mais
d'autres langages, tels que RSL [5] pourraient être utilisés.
RSL est un langage de spécification qui s'est avéré utile pour le développement de logiciel, car il couvre et intègre
dans un cadre uniforme un large spectre de styles de spécification. Il peut donc être utilisé pour les spécifications
des domaines des applications, pour les spécifications des besoins, et pour les spécifications associées à la
conception. Il a été utilisé pour de nombreuses applications, par exemple pour des systèmes critiques de contrôle
de trains [6].

Une alternative à un langage à large spectre tel que RSL est d'utiliser des langages spécifiques pour les domaines concernés. Un langage à large spectre utilise des éléments de langage qui sont indépendants du contexte spécifique
de l'application, tandis qu'un langage spécifique pour un domaine utilise des termes et des concepts d'un domaine d'application bien défini ce qui en facilite la compréhension et l'utilisation par les experts du domaine.
Un exemple de langage spécifique pour un domaine est donné dans [7].

L'objectif du travail proposé ici est de mettre en pratique cette méthode en fournissant des schémas de spécification pour une collection de ``problem frames'', dans le langage RSL et dans des langages spécifiques de domaines tels
que celui proposé par [7]. Les schémas proposés seront évalués sur des études de cas portant sur des applications
où la sécurité est cruciale, dans le domaine ferroviaire.
Une méthode et des guides seront fournis pour l'utilisation de cette technique et pour achever l'écriture des spécifications.

Résultats escomptés au terme de l'action

Ce travail produira des schémas de spécification associés à des ``problem frames'' pour deux types de langages de spécification utilisés pour la spécification de systèmes critiques, un langage à large spectre (RSL) et un langage spécifique pour un domaine. Des études de cas portant sur des systèmes critiques illustreront ce travail.
Une méthode sera élaborée pour guider l'utilisation conjointe des problem frames et des schémas de spécification.
Des guides seront fournis pour la complétion des schémas de spécification obtenus.

Références

[1] Michel Bidoit and Peter D. Mosses.
CASL, The Common Algebraic Specification Language - User Manual.
Springer-Verlag, 2004. To appear. Available at http://www.cofi.info/CASL\_UserManual\_DRAFT.pdf.

[2] Christine Choppy and Maritta Heisel.
Use of patterns in formal development: Systematic transition from problems to architectural designs.
In M. Wirsing, R. Hennicker, and D. Pattinson, editors, Recent Trends in Algebraic Development Techniques,
16th WADT, Selected Papers, LNCS 2755, pages 205--220. Springer Verlag, 2003.

[3] Christine Choppy and Gianna Reggio.
Using CASL to Specify the Requirements and the Design: A Problem Specific Approach.
In D. Bert, C. Choppy, and P. D. Mosses, editors, Recent Trends in Algebraic Development Techniques, 14th WADT, Selected Papers, LNCS 1827, pages 104--123. Springer Verlag, 2000.

[4] Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides.
Design Patterns -- Elements of Reusable Object-Oriented Software. Addison Wesley, Reading, 1995.

[5] C. George, P. Haff, K. Havelund, A. E. Haxthausen, R. Milne, C. B. Nielsen, S. Prehn, and K. R. Wagner.
The RAISE Specification Language. The BCS Practitioners Series. Prentice Hall Int., 1992.

[6] A. E. Haxthausen and J. Peleska.
Formal Development and Verification of a Distributed Railway Control System.
IEEE Transaction on Software Engineering, 26(8):687--701, 2000.

[7] A. E. Haxthausen and J. yPeleska.
A Domain Specific Language for Railway Control Systems.
In Proceedings of the Sixth Biennal World Conference on Integrated Design and Process Technology,
(IDPT2002), Pasadena, California, June 23-28 2002.

[8] Michael Jackson.
Problem Frames. Analyzing and structuring software development problems. Addison-Wesley, 2001.

[9] Gianna Reggio, Egidio Astesiano, and Christine Choppy.
CASL-LTL: A CASL extension for dynamic reactive systems -- version 1.0 -- summary.
Technical Report DISI-TR-03-36, Università di Genova, Italy, 2003.