Séminaire QSL du Pôle ``Intelligence Logicielle'' du LORIA L'ingénierie formelle des systèmes System Engineering 2-3 avril 2003 LORIA Amphi 8 (A008 on 3rd April) UFR STMIA (LORIA on 3rd April) Campus Scientifique Vandoeuvre-les-Nancy (directions)

Program:   Dominique Cansell (INRIA). Thanks to Michel Sintzoff for this original idea ;-)
Inscription au séminaire (Gratuite mais obligatoire) Registration (free, but required)
Mercredi 2 avril / Wednesday 2nd April
9:30	Accueil des participants / Welcome
10:00	La part de la créativité dans le développement et la vérification de programmes concurrents. Pascal Gribomont, professeur à l'Université de Liège (Belgique) Les grands progrès accomplis depuis dix ans dans le domaine de la déduction automatique augmentent l'intérêt des méthodes formelles de spécification, de développement et de vérification de programmes. Le développeur peut, en principe, se concentrer sur l'aspect créatif de sa tâche, les autres aspects étant pris en charge par un système spécialisé. En pratique pourtant, il n'est pas commode d'isoler les aspects créatifs de la programmation. Un point crucial de la démarche de spécification-développement-vérification d'un programme est l'élaboration d'une structure formelle qui résume sa sémantique de manière statique, déclarative. L'exemple le plus commun d'une telle structure est l'invariant (inductif) qui est une formule de logique classique; c'est suffisant pour les propriétés de sûreté. Des graphes de preuve ou structures similaires peuvent être utilisés quand on s'intéresse aussi aux propriétés de vivacité. Le second point important de la démarche est la validation (automatique) de la structure. Si elle est valide, elle constitue une documentation concise et précise du programme. L'exposé visera à montrer, sur des exemples concrets classiques, dans quelle mesure l'élaboration de la structure requiert de la créativité. On donnera aussi des conditions suffisantes pour que des conditions de vérification soient validables automatiquement. REFERENCES P. Gribomont, Development of concurrent systems by incremental transformation, European Symposium on Programming (Copenhague), Lecture Notes in Computer Science, vol. 432, pp. 161-176, Springer, 1990. P. Gribomont, Stepwise refinement and concurrency: the finite-state case, Science of Computer Programming, vol. 14, pp. 185-228, 1990. P. Gribomont, Design, verification and documentation of concurrent systems, Workshop BCS-FACS on Refinement (Cambridge, England), in ``4th Refinement Workshop'', J. Morris and R. Shaw (Eds.), pp. 360-37, Workshops in Computing Series, Springer, 1991. P. Gribomont, Concurrency without toil: a systematic method for parallel program design, Science of Computer Programming, vol. 21, pp. 1-56, 1993. P. Gochet et P. Gribomont, Logique 2, méthodes formelles pour l'étude des programmes. Hermès, Paris, 1994. P. Gribomont et G. Zenner, Automated Verification of Szymanski's algorithm, Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (Lisbonne), Lecture Notes in Computer Science, vol. 1384, pp. 424-438, Springer, 1998. P. Fontaine et P. Gribomont, Decidability of invariant validation for parameterized systems, Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (Varsovie), to appear in Lecture Notes in Computer Science, Springer, 2003.
10:50	Pause
11:20	Validation a priori de besoins utilisateur. Application aux IHM. Yamine Ait-Ameur, professeur à l'Université de Poitiers Le développement de systèmes interactifs, et en particulier les IHM, fait intervenir différents métiers: informaticiens, ergonomes, psychologues, etc. Chaque métier apporte ses propres notations, en particulier pour la description des besoins des utilisateurs. L'hétérogénéité de ces notations conduit le plus souvent à une validation a posteriori par le test. Nous proposons une approche formelle consistant à valider, les descriptions centrées utilisateurs des IHM, dès les premières étapes de la conception. Notre approche est fondée sur l'utilisation du raffinement et de la preuve pour représenter le système mais aussi les tâches ou scénarii d'utilisation. La méthode B constitue le support de ces développements.
12:10	Domain Facets, Domain Requirements and Software Components Dines Bjørner, professeur à l'Université Technique du Danemark (Danemark) We identify separate concerns of modelling "actual worlds": Their (i) intrinsics, (ii) supporting technologies, (iii) management & organisation, (iv) rules & regulations, and (v) human behaviour: The latter diligent, sloppy, negligent or outright criminal. We then identify "an algebra" of "conversions" From domain facets, as listed above (i-v), to domain requirements: (a) projection, (b) determination, (c) instantiation, (c) extension, (d) fitting, (e) initialisation, etc. Similar, but at this stage of research, so far unformalised notions of machine requirements are shown, for some typical examples (system accessibility, availability and adapt- ability) to lead, it is suggested, to certain kinds of software components. Thus the talk present some research that is well under way, and some more that needs much more work !
13:00	Lunch
14:20	Diagrammes de prédicats Dominique Méry, professeur à l'Université Henri Poincaré Nous présentons le formalisme des diagrammes de prédicats que nous avons développé en collaboration avec Dominique Cansell et Stéphane Merz. Un diagramme de prédicats est un abstraction d'un système modélisé en TLA+. Un diagramme de prédicats sert à donner une vue abstraite et simple d'un système plus complexe; on doit montrer que le diagramme de prédicats est une bonne abstraction du système. L'avantage principal du diagramme de prédicats est d'être un graphe fini de prédicats et on peut donc étudier ce graphe considéré comme un système fini avec des techniques de model checking. En outre, on peut développer des digrammes de prédicats en utilisant une relation de raffinement dont l'objectif est de produire in fine un système conforme à cette abstraction. Nous présenterons ce concept à l'aide d'exemples et nous présenterons un outil en construction permettant de représenter les diagrammes de prédicats.
15:10	Event System Decomposition Jean-Raymond Abrial, consultant, Marseille After a short presentation of the concept of "event system" (as encoded within B), I shall formally express the way such systems can be decomposed into several sub-systems which can be freely refined independently of each other.
16:00	Pause
16:30	Rely/Guarantee-conditions and their relevance to error-tolerance Cliff Jones, professeur à l'Université de Newcastle (Royaume Uni) There are well documented methods for developing programs from their specifications; a formal method identifies proof obligations at each step of development; if all such proof obligations are discharged, there is a precise notion of errors which cannot be present in the final program. For a class of ``closed'' systems such methods offer a gold standard against which one can measure less formal approaches. For the interesting class of systems which interact --via sensors and actuators-- with the physical world, the issue of how to obtain a starting specification can be as challenging as how to derive a program from that specification. Being confident that the specification is appropriate is yet more challenging for systems which should tolerate (certain classes of) errors in, say, the sensors. This talk argues that widening the notion of system to specify first the behaviour of the physical system provides a route to deriving the specification of a control system and recording precisely assumptions made about physical components.
17:20	Closing / Fin de la journée
Jeudi 3 avril / Thursday 3rd April
9:00	Comment enseigner l'introduction à la programmation Bertrand Meyer, professeur à l'ETH de Zürich (Suisse) & Eiffel Software L'enseignement d'initiation à la programmation est une source constante de polémique. À l'ETH (École Polytechnique Fédérale de Zürich), l'initiation à la programmation est en cours de refonte, utilisant la technologie objets et les idées de "cursus inversé" et de réutilisation, le tout avec renfort d'applications graphiques, de bibliothèques, d'Eiffel et autres idées novatrices, sur un fond de réorganisation de l'enseignement pour s'adapter au processus de Bologne. L'exposé discute les problèmes classiques d'enseignement de la programmation -- y compris les tensions entre présentation de concepts et présentation de techniques directement utiles, entre le long terme et le court terme, entre les besoins de l'industrie et les choix pédagogiques -- sans oublier la question du choix de langage de programmation. Bertrand Meyer is professor of software engineering at ETH Zürich, founder of Eiffel Software, and author of several books including "Object-Oriented Software Construction". Bertrand Meyer est professeur de Génie Logiciel à l'École Polytechnique Fédérale de Zürich (ETH), fondateur d'Eiffel Software, et auteur de plusieurs livres.
10:00	Closing / Fin de la journée
Soutenance d'Habilitation à Diriger des Recherches de l'Université Henri Poincaré (Nancy I)
10:00	Assistance au développement incrémental et à sa preuve Dominique Cansell, Composition du jury Rapporteurs: Pascal Gribomont, professeur à l'Université de Liège (Belgique), Dines Björner, professeur à l'Université Technique du Danemark (Danemark), Yamine Aït Ameur, professeur à l'Université de Poitiers (France), Bertrand Meyer, professeur à l'ETH de Zürich (Suisse), Examinateurs: Jean-Raymond Abrial, consultant, Marseille (France), Cliff Jones, professeur à l'Université de Newcastle (Royaume Uni), Dominique Méry, professeur à l'Université Henri Poincaré (France) Résumé: Ce travail résume nos activités sur le développement incrémental de systèmes entièrement prouvés, en utilisant le raffinement, afin de simplifier aussi bien la compréhension du système que sa preuve. Notre souci principal est de ``démocratiser'' l'utilisation des méthodes formelles. A titre d'exemple, en collaboration avec Jean-Raymond Abrial et Dominique Méry, nous avons modélisé et prouvé entièrement le protocole d'élection d'un leader dans un réseau (IEEE 1394 du FireWire) par développement incrémental. A partir d'une abstraction, qui élit le leader et l'arbre de recouvrement en un seul coup, nous avons construit plusieurs raffinements dont le dernier est proche de l'algorithme effectivement implémenté où chaque noeud du réseau prend ses décisions localement. Pour simplifier les preuves et surtout pour réaliser des preuves "abstraites", comme les mathématiciens, nous avons défini avec Jean-Raymond Abrial, un langage qui permet de définir des structures mathématiques et leurs théorèmes associés. Nous avons également développé un outil qui traduit des structures en machine B. Nous pouvons, ainsi, utiliser l'Atelier B pour prouver les théorèmes de ces structures. Grâce à l'Atelier B, pour tous ces travaux et bien d'autres, nous avons acquis une certaine expérience de la preuve interactive. Cela nous a permis de travailler, avec Jean-Raymond Abrial, à la réalisation d'une nouvelle interface du prouveur interactif. L'activité de preuve est facilitée en présentant à l'utilisateur des boutons spécifiques associés à des hypothèses et au but pour exécuter un pas de preuve. Le raffinement et la preuve sont donc au centre de nos préoccupations. Il permet de développer des systèmes de façon incrémentale en ajoutant de plus en plus de détails dans le modèle concret. Il permet donc une meilleure compréhension du système car la première abstraction est simple de valider le système en cours de développement car on valide les détails introduits dans le modèle concret, de distribuer la complexité de la preuve car en général les preuves compliquées sont faites dans les premiers modèles qui ne contiennent pas tous les détails, d'expliquer plus facilement le système à d'autres (collègues ou étudiants) Il y aura un pot au LORIA à 18h30

Inscription au séminaire (Gratuite mais obligatoire)