Lionel Morel - iBrarian.net
Contents
1. e Les entr es sorties modes d entr e sortie mode programm mode par interruptions acc s direct m moire instructions d entr e sortie traitement des interruptions par le processeur priorit masquage commuta tion de contexte Projet A partir de la sp cification d un processeur simple par son jeu d instructions les tudiants doivent concevoir un prototype de ce processeur sur un circuit programmable Le projet est accompagn d un ensei gnement flot de conception qui donne une vue d ensemble sur les m thodes et outils utilis s J ai particip cet enseignement e en donnant des s ances de TD la fois pour des tudiants de premi re ann e de la fili re TELECOM et pour des tudiants de premi re ann e de l ENSIMAG e pour l encadrement des s ances de TPs propos es dans le cadre du projet en premi re ann e de la fili re TELECOM 2 2 Langages Compilation 2 2 1 Informatique Langages Expression relationnelle Pendant 2 ann es universitaires cons cutives 2001 2002 et 2002 2003 j ai pris en charge un groupe de TD dans le cadre de l enseignement d informatique de second semestre de deuxi me ann e de DEUG MIAS l UJF Ce enseignement se d roulait sous la responsabilit de Mme Catherine Parent Vigouroux et Mme Marie Christine Fauvet et comportait pour chaque groupe une s ance de TD 1h30 et une s ance de TP 1h45 par semaine pendant 11 semaines Contenu Les objecti2. CMS02 CSO1 dAH01 FF00 GAPT85 Gau03 HB02 HCRP91 Hoa69 Hoa89 H0100 Mat98 McM97 Mey92 MM04a MM04b Mor02 M Abadi and L Lamport Composing specification ACM Transactions on Programming Languages and Systems 15 1 73 132 January 1993 M Abadi and L Lamport Conjoining Specifications ACM Transactions on Programming Languages and Systems 17 3 507 534 1995 G Berry and G Gonthier The ESTEREL synchronous programming language design semantics implementation Science of Computer Programming 19 2 87 152 november 1992 R S Bird Lectures on constructive functional programming In M Broy editor Constructive Methods in Computer Science pages 151 216 Springer Verlag 1988 NATO ASI Series F55 P Caspi Embedded control From asynchrony to synchrony and back In Embedded Software EMSOFT 01 volume 2211 Lecture Notes in Computer Science 2001 M Calder S Maharaj and C Shankland A modal logic for full LOTOS based on symbolic transition systems The Computer Journal 45 1 55 61 2002 M Calder and C Shankland A symbolic semantics and bisimulation for full lotos In Kluwer Academic Publishers editor FORTE 01 International Conference on Formal Description Techniques for Networked and Distributed Systems pages 184 200 2001 L de Alfaro and T A Henzinger Interface theories for component based design Lecture Notes in Computer Science
3. Activit s de Recherche A partir d un noeud contrat on peut g n rer des obligations de preuve pour chacune de ces questions La r solution de ces obligations de preuves peut ensuite tre d l gu e aux outils de validation standard Un outils de pr traitement de programmes LUSTRE pour la validation D une mani re g n rale nous proposons un ensemble d algorithmes de transformations de programmes atour des structures d it rations et par contrats des programmes LUSTRE L ensemble de ces algorithmes a t impl ment dans un outils de pr traitement des objectifs de preuve LUSTRE L interface graphique permet de visualiser le programme en cours de traitement et d appliquer sur les noeuds de ce programme les manipulations que nous avons indiqu plus haut 1 concernant les it rations et 2 concernant les contrats de noeuds Ces transformations g n re des objectifs de preuve sous la forme de noeuds LUSTRE qui peuvent ensuite tre transmis aux outils de model checking ou de test pour LUSTRE Le travail r alis pendant cette th se a d j fait l objet de 2 publications La premi re MM04a porte sur l utilit des it rations et de la sp cification par contrats dans le d veloppement des syst mes r guliers Nous pr sentons les avantages de la m thodologie d velopp e en l illustrant avec une des tudes de cas tudi e dans la th se La seconde MM04b pr sente la notion de contrat pour les syst mes r ac
4. Adresse professionelle Age 26 ans Laboratoire Verimag Date de Naissance 15 Mai 1978 Centre Equation Lieu de Naissance La Mure 38 France 2 Av de Vignate Nationalit Fran aise 38610 Gi res FRANCE Adresse personnelle 12 rue Linn e mail Lionel Morel imag fr 38000 Grenoble web http www verimag imag fr Imorel FRANCE Attach Temporaire l Enseignement et la Recherche poste de 1 2 ATER Institut National Polytech nique de Grenoble et laboratoire Verimag Centre d int r t de recherche M thodes formelles syst mes r actifs embarqu s langages synchrones verifica tion model checking theorem proving sp cification par contrats langages de programmation compilation Activit s d enseignement Architecture des ordinateurs ENSIMAG et D partement Telecom 1 re ann e 2001 2005 Th se de Doctorat en Informatique Verimag INPG Titre Exploitation des structures r guli res et des sp cifications locales pour le d veloppement correct de syst mes r actifs de grande taille Jury Pr sident Mr Jacques Chassin de Kergommeaux ENSIMAG LSR Grenoble _ Rapporteurs Mr Marc Pouzet LIP6 Univ Pierre et Marie Curie Paris 6 Mr Patrice Quinton Antenne Bretagne de 17 ENS Cachan Examinateur Mr Jean Louis Cola o Soci t Esterel Technologies Directrice Mme Florence Maraninchi Juillet 4 Septembre 2001 Stage de Magist re D partement d Informatique et de Math matiqu
5. 2211 148 2001 R B Findler and M Felleisen Behavioral interface contracts for Java Technical Report CS TRO0 366 Department of Computer Science Rice University Houston TX August 2000 PL Guernic A Benveniste P Bournai and T Gauthier Signal A data flow oriented language for signal processing Tech nical Report IRISA report 246 IRISA 1985 F Gaucher Etude du d bogage des syst mes r actifs et application au langage LUSTRE PhD thesis Institut National Polytechnique de Grenoble 2003 N Halbwachs and S Baghdadi Synchronous modeling of asynchronous systems In EMSOFT 02 Grenoble October 2002 LNCS 2491 Springer Verlag N Halbwachs P Caspi P Raymond and D Pilaud The synchronous data flow programming language LUSTRE Pro ceedings of the IEEE 79 9 1305 1320 septempber 1991 C A R Hoare An Axiomatic Basis of Computer Programming Communications of the ACM 12 576 580 1969 C A R Hoare Communicating sequential processes In C A A Hoare and C B Jones Ed Essays in Computing Science Prentice Hall 1989 L Holenderski Compositional verification of synchronous networks In FTRTFTS Formal Techniques in Real Time and Fault Tolerant Systems International Symposium Organized Jointly with the Working Group Provably Correct Systems ProCoS LNCS Springer Verlag 2000 R Matesscu V rification des propri t s temporelles des programmes parall les PhD thesis Institut National Polyt
6. une axiomatisation des transformations d encha nements d it rations Un algorithme d op timisation a t propos qui impl mente ces transformations Une impl mentation a t r alis e comme un 8 Chapitre 1 Activit s de Recherche f g gof O HO H FO O FO O FO O O O0 O Ce po O T T T T T Fic 1 2 Lenchainement map f Fic 1 3 L encha nement d it rations suivi de map g apr s optimisation module externe au prototype de compilateur voqu plus haut Pour cela j ai utilis un outil g n ral de trans formations de programmes Stratego dans lequel j ai pu exprimer les axiomes de transformations comme des r gles de r critures bas es sur le langage de terme de Stratego Cette approche nous a permis de valider rapide ment nos propositions Notre prototype n ayant pas pour but de servir de base pour un compilateur acad mique il tait plus rapide de d crire par des r gles de r criture telles que celle utilis es dans Stratego des versions simplifi es de l algorithme d optimisation que d impl menter algorithme lui m me Durant tout ce travail j ai tudi un nombre important d exemples pour certains tir s d une tude de cas sur laquelle l quipe travaillait pour Airbus L int gralit de ce travail est d crit dans mon rapport de DEA disponible en lig
7. Les tudiants r alisent en g n ral la grande utilit d un code clair bien crit avec des variables aux noms vocateurs des sp cifications des commentaires D un point de vue encadrement l aspect humain est essentiel tant pour r soudre d ventuels conflits au sein des groupes que pour jouer un r le de garde fous aupr s des tudiants Je me suis toujours pr sent eux non comme une critique ensei gnante de leur travail mais comme une aide tant technique qu organisationnelle et comme un chef de projet soucieux que le travail soit men a bien et de la qualit du d veloppement 2 3 2 Projet C Cet enseignement se d roule dans le cadre de la premi re ann e de ENSIMAG l INPG J ai particip l encadrement du projet pendant l ann e 2002 2003 sous la responsabilit de Mr Sylvain Boulm Pr sentation Le projet consiste 4 crire en partie un assembleur pour mini pentium compatible Gnu Linux Elf Les tudiants utilisent le langage C et sont livr s eux m mes pendant une semaine avec un support humain assur par une quipe de tuteurs dont je faisais partie L valuation de ce projet se fait sur une pr sentation d une demi heure avec d monstration Les principaux objectifs de l enseignement sont 1 l apprentissage du langage C 2 de fournir une introduction au g nie logiciel d veloppement d un projet de taille importante 3 la mise en pratique des enseignements
8. approximation du temps d ex cution D un point de vue interne l hypoth se de synchronisme tablit que le d lai de communication entre les com posants d un programme est nul La s mantique de composition dans un langage synchrone est donc simple on peut composer une multitude de programmes sans changer le temps de r ponse global On ne cherche pas produire partir de programmes synchrones des programmes parall les auquel cas cet aspect de l hypoth se de synchronisme serait en parfaite contradiction avec la r alit de l ex cution du programme Les langages syn chrones sont au contraire destin s tre compil s vers du code s quentiel centralis la composition parall le et le m canisme de communication entre composants ne sont que des m canismes de description au niveau du langage Les programmes sont compil s vers du code s quentiel et n impliquent ni parall lisme explicite ni communication au moment de l ex cution Enfin les langages synchrones ne sont pas seulement des langages de sp cification mais permettent r ellement la programmation des syst mes Leurs environnements de programmation fournissent des compilateurs effi caces pour diff rentes cibles logicielles ou mat rielles Bas s sur des s mantiques bien d finies formellement il est facile de les connecter des outils de validation tels que d bogueurs g n rateurs de cas de test prou veurs Le code typique pour un programme synchrone es
9. canismes de composition modulaires utilisables aussi bien dans les programmes dans leurs sp cifications dans la description des environnements validation pr coce des assemblages de composants validation pr coce du comportement dynamique des syst mes par simulation des programmes et des sp cifications tout au long des phases de d veloppement la possibilit d ex cuter des programmes incomplets est un des objectifs prioritaires3 Les contrats tels que nous les introduisons dans cette th se devraient aider r pondre plusieurs de ces crit res Les contrats seront aussi tudi s dans le cadre du projet europ en Assert Automated proof based System and Software Engineering for Real Time4 qui d marre lui aussi en septembre 2004 pour une dur e de 3 ans Ce projet regroupe plusieurs industriels de l avionique et du transport l Agence Spatiale Europ enne Alcatel Space EADS Dassault Esterel Technologies Prover ainsi que plu sieurs laboratoires universitaires europ ens ETH Zurich INRIA CNRS LAAS Verimag et a comme objectif global de mutualiser les efforts des participants en terme de sp cification correcte des Une s mantique commune pour les diff rents formalismes autour de LUSTRE En tudiant les contrats pour LUSTRE nous nous sommes trouv devant la n cessit de d finir une forme de description commune pour la s mantique des noeuds ef des contrats Par la suite nous avons trouv int ressant d
10. cialis les documentations certaines contenaient beaucoup d informations qui s av raient parasites dans le contexte du projet J ai du aussi isol les parties du code que les tudiants devraient r aliser et faire en sorte de leur fournir une base de projet claire fonctionnelle et o les points d int r ts taient clairement identifi s L encadrement du projet lui m me m a beaucoup int ress notamment par les cultures diff rentes des tudiants de cette troisi me ann e sp ciale de l ENSIMAG Ce sont en g n ral des tudiants motiv s qui ont une capacit d abstraction plus importante au m me titre que par exemple les tudiants des DESS double comp tence L valuation finale s est faite sur d monstration des fonctionnalit s impl ment es par leur logiciel Cette valuation orale a t nouvelle pour moi aussi Les syst mes embarqu s prennent une place de plus en plus importante Que ce soit en informatique person nelle en domotique ou dans des domaines fort crit re de s ret on d l gue de plus en plus de t ches im portantes des ordinateurs Cette utilisation grandissante doit ind niablement s accompagner d une volution dans la mani re de concevoir les syst mes informatiques afin qu ils r pondent ces crit res de s ret Globalement il faut distinguer diff rents niveaux de conception Il nous faut tout d abord des techniques de sp cification et de concept
11. de 1 re ann e algorithmique logiciel de base th orie des langages 4 enfin une pr paration aux enseignements de 2i me ann e compilation projet G nie Logiciel et syst me d exploitation Commentaires Le projet dure 1 semaine pendant laquelle mon r le a consist principalement r pondre aux questions des tudiants Ces questions portaient aussi bien sur l utilisation du langage C ou des aspects de d veloppement du logiciel que sur des probl me li s l assembleur d velopp sur le codage des instructions etc 2 3 3 Projet de Compilation En 2002 2003 j ai remplac Mme Catherine Oriat pour organiser et encadrer le projet de compilation pour l ann e sp ciale de l ENSIMAG Ce projet dure une semaine pendant laquelle les tudiants travaillent en bi n me temps complet en libre service sur les machines de l cole Le projet concerne la trentaine d tudiants de l ann e sp ciale Pr sentation N ayant pu avoir de contact avec Mme Oriat absente cette ann e l pour des raisons per sonnelles j ai du mettre en place un projet qui permettrai aux tudiants de valider leurs acquis du module compilation Pour cela j ai repris le projet C propos en premi re ann e l ENSIMAG dans lequel les tu diants doivent crire un assembleur pour mini pentium Je l ai orient afin de permettre aux tudiants de voir toutes les tapes importantes du processus de compilation analyse lexicale anal
12. imp ratif en langage d assemblage 2 Le codage des instructions du langage d assemblage en mots binaires directement interpr tables par les circuits logiques qui constituent le processeur Commentaires En licence d informatique les s ances de TD contiennent toutes une partie importante de cours puisque le cours magistral d ALM ne pr sente pas en d tail les notions sp cifiques au TD logiciel Cela n cessite une pr paration plus importante et une coordination particuli re entre les enseignants des diff rents groupes Il est par contre plus facile d organiser les s ances et d adapter les points traiter en fonction des difficult s rencontr es par les tudiants En RICM par contre les s ances de TD compl te un cours magistral J ai tout de m me rencontr comme le reste de l quipe de TD la n cessit de rappels assez cons quents sur les notions vues en cours D enseigner la m me mati re dans deux cadres diff rents m a beaucoup appris sur les tudiants et les diff rences qui existent dans les fa ons qu ils ont d aborder une mati re J ai not un int r t plus syst matique chez les tudiants de RICM qui h sitent moins s investir dans le travail qu on leur demande On doit alors r pondre de v ritables avalanches de questions mais qui reste au niveau du cours En licence l int r t apport la mati re enseign e est plus disparate dans un groupe de TD Par contre lor
13. rence ETAPS 02 Grenoble Surveillance d examens Pour la quasi totalit des enseignements d taill s au chapitre 2 4 2 Formations compl mentaires Formatoins G n rales Journalisme scientifique les 23 24 et 25 Avril 2002 Volume horaire 24h Histoire des Sciences du 07 Mars au 02 Mai 2002 Volume horaire 24h 12 s ances de 2h Formations Sp cialis es Specification par mod les et d veloppement rigoureux Cours de DEA Informatique Syst mes et Communications UJF Du 15 octobre au 05 d cembre 2001 24h 6 s ances Basic SPIN Tutorial Tutorial de la Conf rence ETAPS 02 Avril 2002 Volume horaire 6h Strategies for Program Transformations Tutorial de la conf rence ETAPS 02 Avril 2002 Volume horaire 6h Workshops International Workshop on Synchronous Programming 2001 du 3 au 7 d cembre 2001 2002 du 25 au 29 novembre 2002 2003 du ler au 5 d cembre 2003 Volume horaire 3 24 heures sur 3 1 semaine Ecoles Ecole S mantique des Langages de Programmation Du 24 au 29 Mars 2002 Agay France Volume horaire 30h sur 1 semaine Ecole Jeunes Chercheurs en Programmation EJC 02 Du 20 au 30 Mai 2002 Rennes France Volume horaire 50h sur 2 semaines Ecole Types Theory and Practice of Formal Proofs Du 2 au 13 Septembre 2002 Giens France Volume horaire 50h sur 2 semaines 21 Bibliographie AL93 AL95 BG92 Bir88 Cas01
14. tie TP Exp rimentation autour d un analyseur d expressions La partie Expression relationnelle comprend 1 Pour la partie TD ensembles et relations alg bre relationnelle introduction au langage SQL 2 Pour la partie TP Exp rimentation autour de l interrogation de bases de donn es Commentaires Un des buts de cet enseignement en compl ment avec les enseignements sur les langages fonctionnels est de montrer aux tudiants les diff rentes formes de programmation et de faire ressortir leurs utilit s respectives Le module permet de mettre en parall le dans un temps assez court 2 de ces formes Gr ce aux TP on arrive faire sentir aux tudiants que l on ne pourrait par exemple pas g rer facilement une base de donn e avec un langage imp ratif L organisation TD TP est b n fique car elle permet d accompagner l tudiant depuis les concepts formels jusqu la r alisation et l ex cution d un programme Une des difficult s li es cet enseignement est le fait qu une partie des tudiants ne se destinent pas des tudes en informatiques et qu ils ont du mal s int resser et s investir dans l apprentissage de la mati re Il faut alors adapter le discours chacun ne pas perdre les tudiants les moins motiv s en approfondissant trop certaines notions avec les tudiants plus motiv s Cet enseignement m a aussi donn l occasion d apprendre corriger des travaux crits Pendant le se
15. 1 2 D Octobre 2001 Mars 2005 j ai effectu une th se toujours sous la direction de Mme Maraninchi th se pour laquelle j ai re u une Bourse de Docteur Ing nieur BDI du CNRS Pr sentant une certaine continuit avec mon travail de DEA mon sujet de th se consistait tudier en quelles mesures certaines formes de structurations des programmes r actifs synchrones particuli rement pour le langage LUSTRE peuvent tre peuvent tre exploi t es pour la validation des syst mes r actifs La section 1 1 3 pr sentent ce travail son contexte les r alisations pratiques qui en ont d coul ainsi que des perspectives que je suis l heure actuelle en train d explorer 1 1 1 Contexte G n ral Le cadre g n ral de ce travail est celui du d veloppement des syst mes r actifs Les syst mes r actifs ont une interaction constante avec leur environnement leur temps de r ponse doit correspondre aux n cessit s de ce dernier On les diff rencie notamment des syst mes transformationnels qui disposent de toutes leurs entr es leur initialisation et d livrent leurs sorties leur terminaison comme un compilateur Beaucoup de syst mes r actifs sont aussi critiques leur dysfonctionnement ayant un impact direct n faste sur leur environnement En particulier toute erreur dynamique est proscrire Ces syst mes sont utilis s dans le domaine du transport avions trains o de l industrie centrales nucl aires Ap
16. EUG tal es sur des p riodes de 3 mois De mani re orthogonale j ai souhait participer l encadrement de projets dans lesquels les tudiants s investissent temps plein pendant des p riodes allant d une semaine 1 mois Je consid re ces deux facettes comme indispensables tout ensei gnement de l informatique les projets permettant aux tudiants de mettre en pratique dans des situations plus r elles les formalismes et les m thodologies qu ils apprennent durant les phases plus th oriques de leur cursus Dans les pages qui suivent j ai d taill les contenus niveau d tudes volume horaire de ces enseignements r partis en 3 cat gories e Architectures Logicielles et Mat rielles e Langages Compilation e P dagogie par Projets Pour chaque enseignement j ai aussi indiqu quelques remarques sur la fa on dont je le per ois tant d un point de vu personnel que p dagogique 2 1 Architectures Logicielles et Mat rielles 2 1 1 ALM UFRIMA et fili re RICM Polytech Grenoble En 2002 2003 j ai donn des s ances de Travaux Dirig s logiciel du module ALM en licence d informatique sous la responsabilit de Mr Paul Amblard responsable du module et de Mme Fabienne Lagnier responsable des TD logiciel En 2003 2004 j ai donn des s ances de TD similaires pour leur contenu mais cette fois ci des tudiants en 1 re ann e de fili re RICM de Polytech Grenoble sous l
17. a responsabilit de Mr Pascal Sicard Chaque ann e j avais la charge d un groupe de TD d une trentaine d tudiants pour 11 s ances de 1h30 chacune Contenu L enseignement d architecture logicielle et mat rielle que ce soit en licence d informatique ou en l re ann e de la fili re RICM vise fournir aux tudiants les bases conceptuelles pour la compr hension du R seaux Informatiques et Communication Multim dia cole Polytechnique de l Universit Grenoble I 13 14 Chapitre 2 Activit s d enseignement fonctionnement d un ordinateur On s int resse principalement 2 th mes 1 Le fonctionnement du mat riel pr sent dans un ordinateur principalement le processeur et les diff rentes formes de m moires ainsi que les communications existant entre ces mat riels 2 la traduction d un programme de haut niveau crit par l utilisateur en des instructions de bas niveau directement interpr tables par le mat riel Pour ces 2 ann es j ai enseign des Travaux Dirig s portant sur le second th me On cherche montrer aux tudiants comment les instructions qu ils utilisent dans leur programmes principalement structure de contr les et appels de proc dures sont traduites par un compilateur en des instructions dans un langage d assemblage et comment le processeur interpr te ces instructions On distingue pour cela 2 niveaux de traduction 1 La traduction des instructions d un programme
18. as des tableaux Afin d viter toute erreur dynamique l introduction des tableaux dans le langage lui m me doit r pondre aux crit res de s ret suivant e les tailles doivent tre connues statiquement e on ne doit pas pouvoir acc der des l ments d un tableau par des indices dynamiques Les tableaux ont t introduits dans LUSTRE V4 pour la description de syst mes mat riels Les techniques de compilation mises en place expansion des tableaux en variables ind pendantes sont particuli rement adapt es la programmation de circuits Puis LUSTRE a t utilis pour le d veloppement de syst mes logiciels Il s est alors av r qu la fois l expan sion et les primitives de manipulation de tableaux concat nation extraction de tranches r cursivit statique ne sont pas pratiques pour le d veloppement logiciel L quipe synchrone de VERIMAG a alors propos lin troduction dans le langage de 4 nouveaux op rateurs appel s it rateurs de tableaux Le but tait de fournir des op rateurs plus s rs plus faciles manipuler et pour lesquels le code g n r serait plus efficace code avec tableaux et boucles de parcours sur ces tableaux Apports et r alisations Le travail effectu durant ce DEA a consist tudier la compilation vers du code efficace de programmes LUSTRE manipulant ces op rateurs tableaux A partir des it rateurs inspir s d op ra teurs it ratifs qu on trouve dans les lan
19. des contrats dans le cadre du d bogage La th se de Mr Fabien Gaucher Gau03 portait sur l tude du d bogage algorithmique de programmes synchrones et a vu notamment la naissance de outil Ludic Le travail de M Vareille consistait augmenter I interpr teur du d bo gueur LUSTRE afin de pouvoir v rifier qu un contrat est bien satisfait pendant la simulation d un programme Manipulations de contrats aide 4 la conception Dans cette th se nous avons repris les d finitions des contrats pr sent e dans Var02 et nous nous sommes int ress s tout d abord a leur s mantique Puis nous avons propos une s rie de propri t s standards associ es a la notion de contrat est ce qu un composant satisfait le contrat qu on lui a associ Est ce que dans un contexte donn le contrat d un composant est satisfait On a montr aussi comment construire le contrat d une composition de composants tant donn les contrats des composants eux m mes Faisant le lien avec la probl matique que nous avons expos plus t t sur l utilisation des tableaux nous avons aussi tudi les questions suivantes 1 Etant donn le contrat d un composant on peut construire de mani re au tomatique un contrat pour une it ration de ce composant 2 On peut aussi d terminer si le contrat est compatible avec l utilisation qu on en fait dans une it ration notion de branchabilit d un composant avec lui m me 10 Chapitre 1
20. e former les ing nieurs de demain ces nouvelles approches puisque ce sont eux qui vont pour en tirer partie dans leur travail Les cursus menant ces m tiers doivent donner les connaissances n cessaires pour la description haut niveau et s mantique des syst mes 1 m thodes de conception haut niveau 2 la construction des syst mes la fois mat riels ou logiciels 3 la compr hension des mod les parall les et temporels des syst mes embarqu s ainsi que pour les m thodes de traductions vers des syst mes ex cutables 1 compilation 2 th ories des langages Il est pour moi tout fait essentiel de d finir des parall les importants entre recherche et enseignement car chacun peut apporter l autre l enseignement peut aussi nourrir la recherche il nous aide prendre du recul par rapport notre th matique Evidement ce parall le tablir est plus difficile lorsqu on enseigne en premier cycle universitaire o le public n a pas forc ment vocation poursuivre des tudes en informatique Mais l informatique doit mon avis tre pr sent tr s t t sous cet aspect formel pour montrer aux tudiants qu il repr sente une fa on int ressante d aborder et de r soudre des probl mes complexes Le travail fournir d un point de vue purement p dagogique est alors plus important mais tellement int ressant 20 4 1 Responsabilit s collectives Avril 2002 Aide l organisation pour la conf
21. ech nique de Grenoble 1998 K L McMillan A compositional rule for hardware design refinement In Proc 9th International Computer Aided Verifi cation Conference pages 24 35 1997 B Meyer Applying design by contract Computer 25 10 40 51 October 1992 F Maraninchi and L Morel Arrays and contracts for the specification and analysis of regular systems In Fourth Interna tional Conference on Application of Concurrency to System Design ACSD Hamilton Ontario Canada June 2004 F Maraninchi and L Morel Logical time contracts for the development of reactive embedded software In 30th Euromicro Conference Component Based Software Engineering Track ECBSE Rennes France September 2004 L Morel Efficient compilation of array iterators for lustre In Florence Maraninchi Alain Girault and ric Rutten editors Electronic Notes in Theoretical Computer Science volume 65 Elsevier 2002 22 BIBLIOGRAPHIE 23 OM92 SBM04 Var02 Wad84 Wad90 WB93 WB94 J P Sansonnet O Michel D De Vito 8_1 2 Data parallelism and data flow Technical report LRI CNRS Universit Paris Sud 1992 C Shankland J Bryans and L Morel Expressing iterative properties logically in a symbolic setting In 70th International Conference on Algebraic Methodology And Software Technology AMAST 2004 2004 M Vareille Extension du concept de programmation par contrats aux syst me synchrones r actifse a tra
22. es Universit de Stirling Ecosse GB Sujet Extension d une logique la HML avec des op rateurs Directrice Dr Carron Shankland 2000 2001 DEA en Informatique Verimag Universit Joseph Fourier Grenoble Titre Compilation efficace des it rateurs de tableaux LUSTRE Directrice Pr F Maraninchi Mention Bien 1999 2000 Maitrise d Informatique Universit Joseph Fourier Grenoble Mention Assez Bien 1999 2000 Licence d Informatique Universit Joseph Fourier Grenoble Mention Passable 1999 2000 DEUG MIAS Universit Joseph Fourier Grenoble Mention Passable Doctorat Dates 2001 2004 Lieu quipe Langages synchrones et Syst mes R actifs Laboratoire Verimag Titre Extraction d obligations de preuve d apr s la structure des programmes Application au langage LUSTRE Directrice Pr Florence Maraninchi R sum Le travail entreprit dans cette th se s inscrit dans le contexte du d veloppement et de la validation des syst mes r actifs synchrones Il vise tirer parti de certaines formes de structuration des programmes durant le processus de d veloppement et de validation Nous tudions premi rement l utilisation d op rateurs r gu liers de types it rateurs qui permettent d exprimer assez facilement des programmes r guliers manipulant des tableaux Nous montrons aussi comment au moment de la validation on peut tirer partie de ces structures r guli re
23. essayer d exprimer les s mantiques d autres formes de sp cifications utilis es dans l quipe A l heure actuelle nous sommes 11 toujours en train d explorer cette voie qui nous permet aussi de comparer les pouvoirs d expressions de ces diff rentes formes de sp cification Ex cution de contrats Une fois d finie dans un cadre commun les s mantiques de diff rentes formes de sp cification noeuds lustre d terministes comportements non d terministes nous pouvons imaginer avoir simuler des r seaux de composants dont certains sont d crits sous la forme de noeuds lustre d autres ne poss dent qu un contrat sans noeud d terministe associ d autres encore prennent d autres formes Il est alors n cessaire de d terminer dans quel ordre effectuer les calculs permettant la simulation des diff rents composants et comment effectuer ces calculs lorsque le comportement est d crit par un contrat C est le but d un travail que nous avons d but r cemment avec F Maraninchi N Halbwachs et P Raymond Contrats pour les syst mes GALS Les GALS Cas01 sont des syst mes Globalement Asynchrones Loca lement Synchrones ils sont constitu s de composants synchrones crit par exemple en LUSTRE qui commu niquent par des moyens asynchrones files d attente rendez vous Dans HB02 N Halbwachs et S Baghadi ont tudi comment les communications asynchrones pouvaient mod lis l aide du syst mes d horl
24. fficile voir impossible r aliser 2 la structuration du programme est perdue mais d une part cette information est peut tre importante pour la validation d autre part en cas de r ponse n gative du v rificateur pour une propri t donn e le retour d information sur les origines potentielles typiquement extraction de contre exemple de l erreur d tect e est impossible assurer Extraction de sous objectifs de validation Sch matiquement on a donc une structuration particuli re des programmes de haut niveau que nous perdons bas niveau lors du processus de validation L id e principale de ce travail a consist proposer une s rie de pr traitement sur des programmes avec it rations qui permettent partir d un objectif de validation portant sur des tableaux d extraire des sous objectifs de validation portant sur des l ments de tableaux que l on peut ensuite d charg aux outils standard de validation LUSTRE Consid rons par exemple le cas d un programme calculant la valeur d un tableau T a l aide d un map f o f est un noeud et sur lequel on souhaite prouver que tous les l ments de T sont positifs Pour cela il est suffisant de prouver que l application de la noeud f produit une valeur toujours positive videmment ce cas est trivial la propri t est un invariant de la boucle map f Dans le cas g n ral on proc de en fait un renforcement de la propri t prouver On va s
25. fs de cet enseignement sont les suivants On cherche expliciter la perception des aspects syntaxiques des langages outils de description ad quats criture d analyseurs On tente de sensibiliser les tudiants un mode d expression d clarative fond sur le mod le relationnel On tablit aussi le lien entre divers styles d expression fonctionnel actionnel relationnel On aide les tudiants renforcer leur savoir faire de 3Math matiques Informatique et Application aux Sciences Universit Joseph Fourier 16 Chapitre 2 Activit s d enseignement programmation en ce qui concerne le codage m thodique des algorithmes la structuration et la documentation des programmes la modification des programmes et l utilisation de tests Enfin on leur permet de concr tiser par l exp rimentation la compr hension des principes et techniques de param trisation et de modularit L enseignement est d coup en 2 parties distinctes Automates et grammaires et Expression relationnelle Chaque partie comporte une part d exp rimentation importante r alis e en TP encadr s qui permet aux tu diants de concr tiser les notions formelles aborder en cours et en TD La partie Automates et grammaires comprend 1 Pour les s ances TD tude des expressions r guli res analyse lexicale d un langage automates reconnaisseurs grammaires analyse syntaxique d un langage analyseurs r cursifs descendants 2 Pour la par
26. gages fonctionnels tels que fold ou map Bir88 OM92 on cherche g n rer du code imp ratif avec une boucle de type for pour chacune des it rations utilis es dans le programme LUSTRE Lorsque par exemple un map qui consiste appliquer le m me noeud tous les l ments d un tableau est appliqu un tableau T pour calculer un tableau T on obtient dans le code imp ratif g n r une boucle de type for dont le corps est constitu d une application du noeud it r sur un l ment du tableau T pour calculer l l ment correspondant du tableau T Un algorithme de g n ration de code a t propos et impl ment dans un prototype de compilateur Parall lement nous nous sommes aussi int ress s optimisation des enchainements des it rations Consid rons l exemple de la figure 1 2 qui montre graphiquement un enchainement de 2 op rateurs map Le premier map f it re le noeud f sur T c est dire applique f tous les l ments de T pour calculer T Le second map g it re g sur T pour calculer T Intuitivement si T n est pas utilis ailleurs que comme interm diaire dans cet enchainement d it rations on pourrait l liminer et remplacer ces deux it rations par une seule it ra tion d une composition de f et g figure 1 3 Ces transformations sont inspir es des notions de listlessness et de d forestation introduite par Mr P Wadler Wad84 Wad90 Nous avons donn
27. ion Efficace d It rateurs de Tableaux LUSTRE R sum Les tableaux ont t introduits dans le langage LUSTRE partir de la version V4 destin e princi palement la compilation vers du mat riel Les op rateurs de manipulation de tableaux alors propos s taient particuli rement adapt une cible mat riel notamment sur des cartes programmables Xilinx Pour une uti lisation dans un cadre purement logiciel plusieurs inconv nients ont t associ s aux tableaux de Luste V4 notamment concernant l efficacit du code produit les tableaux sont expans s en variables ind pendantes Dans ce travail nous pr sentons de nouveaux op rateurs adapt s des it rateurs utilis s dans les langages fonc tionnels pour lesquels nous proposons un sch ma de compilation vers du code imp ratif efficace Un prototype de compilateur a galement t d velopp qui impl mente la solution pr sent e Directrice Pr Florence Maraninchi Mots clefs Syst mes embarqu s compilation it rateurs code efficace boucles programmation synchrone Conf rences Internationales avec Actes et Comit de Lecture e Logical Time Contracts for Reactive Embedded Components F Maraninchi and L Morel 30th EU ROMICRO Conference on Component Based Software Engineering Track ECBSE 04 Rennes France Sep tember 2004 Auteur principal L Morel Pr sent par L Morel e Arrays and Contracts for the Specification and Analysis of Regular Syste
28. ion haut niveau qui soient fond e math matiquement et dont on peut d crire une s mantique formelle Le besoin pour cette s mantique formelle des syst mes se fait ressentir lorsque l on veut v rifier des propri t s sur les syst mes on doit pouvoir d finir la fois les syst mes et leur propri t s de la fa on la plus pr cise possible L aspect haut niveau est indispensable si l on veut que les personnes d veloppant les applications puissent s approprier ces techniques le plus facilement possible Il faut donc fournir des langages la fois clairs et assez expressif pour r pondre aux besoins Cette partition langage haut niveau s mantique for melle n cessite videment des technologies de transformation efficaces qui permettent de g n rer des syst mes ex cutables partir des langage haut niveau et garantissant la conservation de la s mantique Cette volution dans la conception des syst mes doit se faire mon sens selon deux voix parall les et compl mentaires que sont la recherche et l enseignement D un point de vue recherche la communaut scientifique acad mique travaillant dans le domaine des syst mes embarqu s et de leur s ret doit r pondre aux attentes technologiques des applications finales en proposant de nouveaux formalismes nouvelles technologies et nou velles m thodologies qui permettent de mieux appr hender les probl mes mis en jeu D un point de vue enseignement il para t crucial d
29. l Workshop on Synchronous Programming Dagshtul 2001 e Efficient compilation of array iterators for the synchronous data flow language lustre S minaire du d partement d informatique et de math matiques de l Universit de Stirling Ecosse Septembre 2001 http www cs stir ac uk seminars aut01 html Le tableau ci dessous synth tise mes activit s d enseignement par ordre chronologique Lorsqu un enseigne ment est indiqu pour deux ann es scolaires le volume horaire correspond une seule ann e A ce jour le cumul des heures effectu es atteint approximativement 200h quivalent TD Chaque enseignement est d taill plus loin dans le chapitre 2 Ann e s Statut Intitul Public concern tablissement Volume Horaire Soutien x 3 2000 01 Vacataire Th mes D couverte d UNIX DEUG MIAS lere Annee TD 12h UJF BAC 1 programmation avec C 2001 02 Vas Langages et Grammaires DEUG MIAS 2 me Ann e TD 15h et 2002 03 acataire Expression Relationnelle SQL UJF BAC 2 TP 18h E Ann e Sp ciale BAC 5 Cours 3h 2001 02 Vacataire Projet de Compilation ENSIMAG INPG TP 24h Architectures Licence d Informatique BAC 3 ae Vacataite ele et Mat rielle UFRIMA UJF TD 18h Premi re Ann e BAC 3 2002 03 Vacataire Projet C ENSIMAG INPG TD 18h 2002 03 Licence d informatique BAC 3 et 2003 04 Vacataire Projet de Programmation UFRIMA UJF TD 18h x Architectu
30. m de chose sur le fonctionnement du compilateur lui m me Ce module est d ailleurs con u comme une introduction certaines notions formelles qui sont approfondis en seconde ann e dans le module compilation Dans cet enseignement j ai eu la charge d un groupe de TD J ai ainsi assur 9 s ances de 1h30 J ai aussi corrig une partie des copies d examen 2 2 3 Programmation et Algorithmique de base En 2000 2001 j ai assur 12 heures de soutien pour des tudiants de DEUG MIAS 1 re ann e DSU Univer sit Joseph Fourier Mon travail consistait assurer une permanences de 1h30 2h par semaine pendant 8 semaines et de r pondre aux questions pos es par les tudiants Mon int r t pour cet enseignement a principa lement r sid dans le fait que les tudiants ne me consid raient pas vraiment comme un enseignant je n tais jamais l pour les juger et arrivaient plus facilement me poser des questions Les th mes principalement abord s taient la programmation imp rative et l utilisation du langage et du compilateur C Ces 8 s ances ont t tr s importantes pour moi elles ont constitu ma premi re exp rience d enseignant et ont consolid la motivation que j avais a priori pour ce m tier 2 3 P dagogie par Projets Depuis le d but de ma th se j ai pris coeur de participer l encadrement de projets pendant lesquels les tudiants doivent programmer des logiciels de taille imp
31. mestre les tudiants ont du 1 rendre deux comptes rendus de TP r dig un pour chaque th me abord 2 rendre un examen blanc donn mis parcours comme devoir la maison reprenant g n ralement le sujet de l ann e pr c dente J ai ainsi du corriger des comptes rendus de TP ainsi qu un examen complet m me si la note ne comptait pas dans l valuation finale des tudiants J ai par ailleurs toujours sollicit les tudiants pour qu ils me rendent des exercices de leur propre chef 2 2 2 Automates et Applications En 2002 2003 j ai donn des s ances de Travaux Dirig s dans le cadre du cours Automates et Applications pour des tudiants de premi re ann e du d partement T l com de l ENSIMAG Cet enseignement se d roulait sous la direction de Mme Florence Maraninchi et comprenait 9 cours magistraux donn s par Mme Maraninchi et 9 s ances de TD de 1h30 par groupe J avais la charge d un groupe d a peu pr s 30 tudiants Contenu Le but du module consiste fournir des tudiants visant plut t un m tier dans le domaine des t l communications une formation de base sur les langages et les moyens de description des langages ainsi que sur les automates qui permettent de d crire le comportement d un syst me informatique La continuit est assur e en 2 me ann e dans le cours de compilation du module G nie Logiciel L enseignement est d coup en 2 parties Dans la partie Langages on co
32. mmence par montrer comment d crire des langages l aide du formalisme des expressions r guli res ER On insiste ensuite sur les limitations des ER dont l expressivit est trop faible dans la pratique On introduit ensuite les grammaires hors contexte sur lesquelles on pr sente la notion d ambigu t On pr sente aussi diff rentes notations possibles pour d crire les grammaires BNF EBNF diagrammes syntaxiques Dans la partie Automates on commence par tudier les automates reconnaisseurs et leur relation avec les ER On d crit les transformations classiques sur ces automates minimisation limination des e transitions d terminisation etc Ensuite on introduit les automates transducteurs suivant les mod les de Moore et de Mealy On explique enfin les notions de d terminisme et de r activit sur ces mod les 17 Commentaires La place de ce module dans la formation globale des tudiants en fili re TELECOM est par ticuli re Ces tudiants ne se destinent pas un travail d informaticien et il n est pas vident de leur montrer l utilit des formalismes pr sent s dans leur contexte Pourtant ces notions font partie des bases de l infor matique pratique avec laquelle ils devront certainement travailler compilateur langage de programmation notion de machine J ai tent d appuyer mon discours sur cette id e il me para t important pour une personne utilisant un compila teur de savoir un minimu
33. ms F Maraninchi and L Morel 4th International Conference on Application of Concurrency to System Design ACSD 04 Hamilton Ontario Canada June 2004 Auteur principal L Morel Pr sent par L Morel e Expressing Iterative Properties Logically in a Symbolic Setting C Shankland J Bryans and L Morel 10th International Conference on Algebraic Methodology And Software Technology AMAST 04 Stirling Scotland July 2004 Auteur principal C Shankland Pr sent pour C Shankland e Efficient Compilation of Array Iterators for LUSTRE L Morel 1st Workshop on Synchronous Lan guages Applications and Programs SLAP02 Grenoble April 2002 Pr sent par L Morel Rapports e Exploitation des structures r guli res et des sp cifications locales pour le d veloppement correct de syst mes r actifs de grande taille L Morel Th se de Doctorat Mars 2005 e Une logique modale temporelle bas e sur une s mantique symbolique de Full LOTOS L Morel Rap port de Magist re Septembre 2001 e Compilation Efficace d It rateurs de Tableaux Lustre L Morel M moire de DEA June 2001 Pr sentations dans des S minaires e Contrats pour LUSTRE S minaire de l quipe Langages Synchrones de Verimag F vrier 2004 e First Steps In Extracting Proof Obligations from Data Structures of LUSTRE Programs Synchron 02 La Londe Les Maures 2002 e Efficient Compilation of Array Iterators for LUSTRE Synchron 01 8th Internationa
34. n s jour j ai fait un expos sur le travail r alis l bas et un expos sur mes travaux de DEA Cette section pr sente en d tails les enseignements auxquels j ai particip depuis mon DEA durant ma th se et derni rement dans le cadre de mes fonctions d ATER Pendant ma th se j ai effectu des enseignements aussi bien au sein de l Universit scientifique Joseph Fourier de Grenoble et de l Institut National Polytechnique de Grenoble Mon ATER s est d roul au sein de l ENSIMAG Jusqu pr sent mes enseignements se sont orient s selon deux th mes principaux e l tude des architectures des ordinateurs e l tude des langages de programmation et des formalismes associ s videmment un tel choix n a pas t fait dans l id e d viter d autres th mes mais dans celle d approfondir deux th mes pour lesquels j ai une sensibilit particuli re et pour lesquels je me sentais pr s sur une p riode courte assumer des enseignements J ai particip des enseignements pour ces deux th mes des niveaux diff rents principalement premier et second cycles et une fois en troisi me cycle et pour des publics diff rents tudiants universitaires l ves ing nieurs voir m me ing nieurs non informaticiens en formation double comp tence Ces enseignements se font sous la forme de s ances de travaux dirig s parfois augment es de s ances de tra vaux pratiques surtout au niveau D
35. ne l adresse http www verimag imag fr lmorel Transfert Directement apr s ce DEA une impl mentation compl te des algorithmes de transformations et de g n ration de code a t d velopp par Jean Louis Cola o de la soci t Esterel Technologie qui d veloppe l outil Scade version industriel du langage LUSTRE Depuis d but 2003 une nouvelle version du langage et du compilateur acad mique est d velopp au laboratoire Verimag par Mr N Halbwachs P Raymond et Y Bouzouzou Ce compilateur prend en compte les it rateurs de tableaux et traite les encha nements d it rateurs de la mani re d crite plus haut 1 1 3 Utilisation de la structure des programmes pour la validation Probl matique originale Dans la continuit de mon travail de DEA principalement centr sur des consid rations de compilation la question suivante s est pos dans quelle mesure est il possible de tirer partie des structures r guli res de programmes impliqu es par l utilisation des it rateurs de tableaux pour la validation Dans le processus de v rification que ce soit pour du test ou pour de la v rification par model checking les tableaux taient jusque l expans en variables ind pendante comme pour la compilation en LUSTRE V4 Nous pouvons identifier deux principaux inconv nients cette approche 1 la taille du programme explose lors de l expansion des tableaux Le model checking de tels programmes est alors plus di
36. ntique tend la s mantique standard en donnant un sens aux comportement param tr s par des donn es jusque 1a oubli par les approches classiques et fournit une repr sentation finie de ces comportements Une bisimulation symbolique a aussi t d finie Une partie de ce projet a consist au d veloppement d une logique modale pour I expression de propri t s sur les STSs Cette logique nomm e FULL permet l expression de propri t s manipulant les donn es gr ce des op rateurs classiques de quantifications sur ces donn e pour tout et il existe CMS02 d crit cette logique et montre qu elle est ad quate vis vis de la bisimulation sur les STSs Une des limitations de la logique FULL est qu elle ne peut exprimer que des propri t s sur des chemins des STSs d une longueur fixe et connue Pourtant les propri t s les plus int ressantes en validation s ret et vivacit manipulent n cessairement des chemins de longueurs arbitrairement grande voir infinie Les propri t s de s ret permettent d exprimer le fait que quelque chose de mauvais en g n ral n arrivera jamais quelque soit le cheminement suivi dans le parcours du STS Les propri t s de vivacit elles expriment le fait que quelque chose de bon arrivera n cessairement un jour Mon travail dans ce contexte a consist tudier les possibilit s de d finitions d op rateurs permettant l criture de telles propri t s J ai pr
37. oge du lan gage LUSTRE Dans un avenir plus lointain nous aimerions tudier la s mantique et l utilit des contrats de composants dans le cadre des syst mes GALS 1 2 Stage de magist re Extension temporelle de la logique modale FULL A la suite de mon DEA et avant d entreprendre ma th se Verimag j ai effectu mon stage de troisi me ann e de magist re d informatique au sein du D partement d Informatique et de Math matiques sous la direction de Mme Carron Shankland Le cadre g n ral reste la validation des syst mes Nous ne nous int ressons plus des syst mes r actifs mais des syst mes distribu s ou concurrents Le sujet de ce travail n avait pas t d cid l avance je me suis int gr l quipe du projet DIET comprenant Mme C Shankland Mme Savi Maharaj ainsi que Mr Jeremy Bryans en proposant moi m me un avancement dans une direction que les membres de l quipe n avait pas encore pu explorer Le projet DIET pour Developing Implementation and Extending Theory a pour but le d veloppement th o rique et l impl mentation d une approche symbolique pour le raisonnement autour du langage LOTOS LOTOS est un langage formel inspir de CSP Hoa89 utilis pour la description des syst mes distribu s et concurrents Dans CS01 C Shankland et Mme Muffy Calder ont propos une s mantique symbolique du langage sous la forme de Syst mes de Transitions Symboliques STSs Cette s ma
38. opos une extension FULL nomm e sobrement FULL pour laquelle j ai d fini des op rateurs similaires ceux des expressions r guli res concat nation de comportements et r p titions ventuellement vides partiellement inspir de ceux qu on trouve dans la logique XTL Mat98 de l outil CADP Les choix de ces op rateurs a t le fruit d une longue r flexion pour trouver un compromis entre le pouvoir d expression de la logique et la facilit d criture De nombreuses logiques parmi lesquelles la plus connue 12 Chapitre 1 Activit s de Recherche est certainement ACTL ont ainsi t tudi es Une impl mentation partielle de cette extension a t faite en utilisant le langage XTL De nombreux exemples de propri t s ont t d velopp s tout au long de ce travail Ce travail a fait l objet d une publication SBM04 dans la conf rence AMAST 04 International Conference on Algebraic Methods And Software Technology Le papier sera pr sent par Mme C Shankland au mois de Juillet 2004 Note personnelle Cette exp rience a t tr s enrichissante tant d un point de vue scientifique que personnel outre le fait de travailler avec une nouvelle quipe sur un sujet nouveau pour moi et d avoir la possibilit d explorer une partie de l informatique que je n avais encore pas tudi j ai du apprendre travailler dans une autre langue que je ma trise par ailleurs et communiquer mon travail lors de mo
39. ortante en groupe Cet aspect de l enseignement o les tudiants sont plong dans une vie de programmeur est indispensable mes yeux afin que chaque tudiant per oive les aspects organisationnels li s leur futur m tier Dans ces projets il doivent toujours travailler en groupe g n ralement 4 personnes ou plus ce qui impliquent qu ils doivent e organiser leur travail mise en pratique indispensable des notions de g nie logiciel sur les sp cification haut niveau de leurs programmes e g rer le cot humain d un travail d quipe Bien videment ces s ances de programmation intense permettent aussi d encrer les notions fondamentales apprises pendant l ann e et de leur faire prendre les bonnes habitudes de programmation clart du code commentaires etc 2 3 1 Projet de Programmation en Licence d Informatique Durant deux ann es 2002 2003 et 2003 2004 j ai particip l encadrement du projet de fin d ann e de la troisi me ann e de licence d informatique sous la responsabilit de Mr Laurent Mounier En 2002 2003 j ai encadr 2 groupes de 6 tudiants Malheureusement suite des fermetures prolong es des b timent de P UFRIMA dues des gr ves des personnels ITA de l Universit le projet n a pas pu tre termin En 2003 2004 j ai encadr 3 groupes de 6 tudiants J ai aussi particip l amphi de pr sentation des jeux Pr sentation Le projet se d ro
40. otion de contrat est tudi e pour diff rentes formes de composants Elle a t propos par Mr Bertrand Meyer Mey92 puis par exemple FF00 dans le cadre de la programmation orient e objet particuli rement le langage Eiffel Des approches similaires la notre ont t propos e pour le d veloppement des syst mes purement mat riel WB93 WB94 Parall lement les m thodes compositionnelles ont propos d tudier les raisonnements circulaires li s la composition des composants Si l on consid re 2 composants P et Q qui communiquent entre eux et qu on veut prouver que P satisfait une propri t sous une hypoth se a et que Q satisfait une propri t 4 sous l hypoth se 5 nous devons prouver que 4 la propri t v rifi e par Q implique a l hypoth se de P et inversement que implique 5 Dans ce domaine on peut noter principalement les travaux de Mr Abadi et Mr L Lamport AL93 AL95 et de Mr K McMillan McM97 Dans le cadre des syst mes r actifs on peut noter le travail de Mr De Alfaro et Mr Henzinger dAH01 qui s int ressent plus la synth se de contr leurs depuis des sp cifications par contrat ainsi qu au travail de Mr Holenderski Hol00 qui s int resse a la v rification compositionelle de r seaux de composants synchrones Programmation d fensive L tude des contrats pour LUSTRE a d but avec le stage de magist re de Mr Marc Vareille Var02 dans lequel il tudiait l interpr tation
41. proche synchrone La famille des langages et formalismes synchrones a repr sent un contribution im portante dans le domaine de la programmation des syst mes r actifs Cette approche est la base des langages Esterel BG92 Signal GAPT85 et LUSTRE HCRP91 Elle repose sur l hypoth se de synchronisme qui 6 Chapitre 1 Activit s de Recherche tablit que le temps de r action d un syst me est nul D un point de vue externe cela veut dire que les sorties sont produites de fa on simultan e avec la r ception des entr es Ceci est clairement impossible impl men ter N anmoins un syst me synchrone fonctionne parfaitement du moment qu il r agit assez rapidement par rapport la vitesse impos e par son environnement Par exemple si les modifications significatives dans les entr es du syst me arrivent au plus toutes les secondes alors le syst me doit pouvoir r pondre en au plus une seconde Lorsqu on sp cifie un syst me r actif l aide d un langage synchrone on doit donc v rifier que le code produit par compilation ex cute bien une r action suffisamment rapidement On calcule donc un temps d ex cution au pire Ce calcul est habituellement rendu difficile par les constructions r cursives ou de boucles pr sentes dans les langages de programmation Mais ces constructions n apparaissent pas dans les langages synchrones La structure du code produit est telle qu on peut toujours fournir une sur
42. ption formelle des syst mes distribu s et concurrents Depuis quelques ann es le d partement d informatique de l univer sit de Stirling travaille sur une s mantique symbolique de LOTOS centr e sur les Syst mes de Transitions Symboliques STSs et sur des techniques de validation associ es En particulier une logique a t d velopp e FULL permettant d exprimer des propri t s sur les STSs Une des restrictions majeures de cette logique r side dans l impossibilit d exprimer des propri t s portant sur des comportements arbitrairement longs Parmi ces propri t s on retiendra les propri t s de s ret quelque chose de mauvais n arrivera jamais et de vivacit quelque chose de bon arrivera s rement un jour qui jouent un r le central dans la validation des syst mes Notre travail dans ce contexte a t de proposer une extension la logique nomm e FULL permettant d ex primer de telles propri t s Nous avons aussi tudi l expressivit de la logique notamment par rapport aux propri t s de s ret et de vivacit Ce travail fait l objet d une publication la conf rence AMAST 04 et sera pr sent en juillet 2004 Mots clefs LOTOS V rification Formelle Logique Temporelle Syst mes d tats Infinis Repr sentation Symbolique Dipl me d tudes Approfondies Dates 2000 2001 Lieu quipe Langages synchrones et Syst mes R actifs Laboratoire Verimag Titre Compilat
43. res Premi re Ann e RICM BAC 3 200303 Vacataire I ogicielle et Mat rielle EPUG ee Architectures Premi re Ann e BAC 3 2003 04 1 2 ATER Logicielle et Mat rielle ENSIMAG et D partement Telecom AD ooh Abr viations utilis es dans le reste du document pour d signer des tablissements ou des fili res d enseigne ments UJF Universit Joseph Fourier Grenoble I UFRIMA UFR Informatique Math matiques Appliqu es MIAS Fili re Math matiques Informatique et Applications aux Sciences ENSIMAG cole Nationale Sup rieure d Informatique et Math matiques Appliqu es de Grenoble INPG cole Nationale Polytechnique de Grenoble RICM Fili re R seaux Informatiques et Communication Multim dia EPUG cole Polytechnique de l Universit Joseph Fourier de Grenoble ex ISTG Le contexte g n ral de mes travaux de recherche est celui de la sp cification et de la validation formelles des syst mes informatiques En 2000 2001 j ai effectu mon DEA au sein du laboratoire Verimag sur le th me de la compilation efficace des it rateurs de tableaux LUSTRE D Octobre 2001 Mars 2005 j ai effectu une th se Verimag pendant laquelle j ai tudi les possibilit s de prise en compte de la structure des programmes notamment pour le langage LUSTRE dans la validation des programmes La section 1 1 d crit ces 2 travaux Jusqu en Aout 2005 je suis ATER l ENSIMAG et Verimag o je po
44. rtie Un syst me est n cessairement d fini l aide d au moins un noeud qui repr sente son comportement global La soci t Esterel Technologies commercialise un environnement de programmation appel SCADE bas sur LUSTRE De nombreuses applications industrielles ont lieu gr ce aux liens qu entretient l quipe avec des soci t s telles que Schneider Electrics A rospatiale la RATP o encore la SNCF 1 1 2 Compilation efficace des it rateurs de tableaux Lustre Cette partie pr sente le travail effectu durant mon DEA L article Mor02 publi en 2001 au Premier Work shop International sur les Langages Applications et Programmes Synchrones synth tise ces travaux Structures de donn es LUSTRE permet la manipulation de structures de donn es au travers de langages h tes comme C La d finition dans LUSTRE de types complexes ne semble pas toujours n cessaire puisque ces types ne servent fr quemment qu v hiculer des informations structur es L inconv nient est que la ma nipulation de telles structures n est pas ma tris e par les outils LUSTRE En particulier on ne peut pas esp rer prouver des propri t s li es la structuration des donn es si celle ci n est pas d crite en LUSTRE L quipe synchrone a donc propos d introduire dans LUSTRE les structures de donn es les plus fr quemment utilis es telles que les types champs multiples appel s usuellement records et les tableaux C
45. s minimisation e Electronique semi conducteurs transistor bipolaire transistors MOS bascules et portes Circuits combinatoires portes multiplexeurs logique programmable ROM PLA FPGA et m thodes de synth se e Arithm tique binaire circuits it ratifs et cellulaires e Circuits s quentiels bascules registres automates et m thodes de synth se 15 e Synth se de circuits complexes comportant un contr leur et une partie op rative Un ensemble de six s ances de travaux pratiques illustre et compl te cet enseignement l objectif est de r aliser diff rents types de circuits partir de bo tiers de faible complexit et ou d observer leur comportement J ai particip cet enseignement e pour l ecandrement des s ances de TPs 2 1 2 2 Computer Design Objectifs de l enseignement Cet enseignement pr sente les notions de base de l architecture des ordinateurs la structure interne d un processeur son jeu d instructions et son ex cution ainsi que les dispositifs d entr e sortie et illustre les principes de la conception moderne de circuits complexes par un projet qui consitse r aliser un processeur Contenu e Le processeur sp cification notion de programme machine jeu d instructions tude de cas conception d un processeur simple choix de la partie op rative sp cification et conception de la partie contr le les diff rents types de processeurs CISC RISC
46. s pour rendre la preuve d une propri t plus simple Nous nous int ressons ensuite la sp cification dite par contrat o un couple assume guarantee est associ chaque composant pour sp cifier les hypo th ses sur l environnement et les propri t s satisfaites par le composant sous ces hypoth ses Nous montrons l int r t de tels contrats la fois en terme de sp cification et de v rification pour le cas particulier des syst mes synchrones Nous proposons une s rie d algorithmes de transformations de programmes aussi bien autour de l utilisation des it rateurs que des contrats utilisable comme pre processeur d objectifs de preuve pour les ou tils de validation Nos propositions notamment sur l aspect langage des it rateurs ont r pondu des besoins rencontr s dans les applications industrielles particuli rement autour du langage Lustre auquel nous appli quons nos r sultat Ces propositions seront bient t incluses dans la version industrielle du langage Mots cl s programmation synchrone Lustre contrats assume guarantee it rateurs de tableaux validation Magist re Dates Juillet Septembre 2001 Lieu Department of Computing Science and Mathematics at the University of Stirling Scotland Titre Extension de la logique FULL avec des op rations it ratives Directrice Dr Carron Shankland R sum LOTOS Language Of Temporal Ordering Specification est une technique de descri
47. sque cet int r t existe il est plus profond on d c le des tudiants plus autonomes et plus pr s approfondir les questions soulev es Pendant le semestre les tudiants taient valu s sur des travaux pratiques dans lesquelles ils devaient coder en langage assembleur quelques algorithmes classiques J ai ainsi eu corriger des comptes rendus de TP durant ces 2 ann es 1 ou 2 s ances sur machines encadr es ont t mise en place dans lesquelles nous montrons aux tudiants l utilisation de base des logiciels tels que compilateur et d bogueur 2 1 2 2004 05 1 2 ATER ENSIMAG Depuis Septembre 2004 et jusqu fin aout 2005 je suis ATER l ENSIMAG INPG Grenoble Mes acti viti s d enseignement portent essentiellement sur l architecture des ordinateurs Je donne des TDs et encadre des s ances de TPs dans plusieurs modules d taill s ci dessous la fois pour des tudiants en premi re an n e l ENSIMAG et pour des tudiants en premi re au d partement TELECOM joint entre l ENSIMAG et l ENSERG l cole Nationale Sup rieur d Electronique et Radio lectricit de Grenoble 2 1 2 1 Digital Circuits Objectifs de l enseignement Cet enseignement a pour but de donner les l ments n cessaires la compr hension du fonctionnement du mat riel informatique travers tude de la conception des circuits digitaux Contenu e Alg bre de Boole calcul bool en fonctions bool enne
48. t constitu d une boucle infinie A chaque tour de cette boucle le programme re oit ses entr es calcule ses sorties et m morise les valeurs n cessaires la suite de son ex cution voir figure 1 1 lt Initialiser la m moire gt Pour toujours faire lt lire les entr es gt lt calculer les sorties gt lt mettre a jour la m moire gt FIG 1 1 code s quentiel pour un programme synchrone Lustre LUSTRE est un langage flot de donn es synchrone d di la programmation des syst mes r actifs Il est d velopp depuis le milieu des ann es 80 partir d une id e de Paul Caspi et Nicolas Halbwachs Le but est de fournir un cadre formel de d veloppement de logiciels s rs et efficaces A ce titre certaines caract ristiques de langages plus g n raux ne sont pas inclus dans LUSTRE manipulation explicite de la m moire allocation dynamique de donn es etc On cherche ainsi viter tout erreur dynamique Par contre le langage contient des m canismes de description sp cifiques la programmation synchrone flot de donn es notamment la ma nipulation explicite des flots et des horloges Le langage LUSTRE permet de d crire des programmes r actifs partir de noeuds Les noeuds sont des composants d terministes et r actifs que l on d finit en Lustre par des ensembles de variables d entr es de sorties et des variables locales ainsi que des quations d finissant les comportement des variables locales et de so
49. tif et compare notre approche celles utilis es aussi bien dans le monde de la programmation orient e objet que dans celui du d veloppement de syst mes mat riel 1 1 4 Perspectives Les paragraphes suivants abordent quelques th matiques de recherche qui d coulent directement du travail effectu durant cette th se Nous en tudions actuellement un partie Vers une notion de composants embarqu s La notion de contrat que nous avons introduit dans ce travail est r pandue depuis de nombreuses ann es dans le domaine du g nie logiciel orient objet Par contre elle est assez r cente dans le cadre des syst mes r actifs Elle semble prometteuse notamment au regard des tudes de cas que nous pr sentons dans les chapitres 6 et 7 Le projet Alidecs Langages et Atelier Int gr pour le D veloppement de Composants Embarqu s S rs d marre en septembre 2004 pour une dur e de 2 ans dans le cadre de l ACI2 s curit Plusieurs laboratoires quipe S mantique Preuve et Impl mentation du LIP 6 quipe Synchrone de Verimag projets INRIA Pop Art et Mimosa quipe CMOS du LaMD tentent de mettre en commun leurs efforts afin d tudier les syst mes embarqu s critiques de grande taille pour lesquels la r utilisation devient un probl me crucial gt Le projet privil gie une approche langage des aspects suivants support au cycle de vie depuis les phases initiales de sp cification jusqu au code embarqu efficace m
50. ule sur 4 semaines et temps complet pendant lesquelles les tudiants r partis en groupe de 6 doivent d velopper un logiciel de taille importante Le logiciel produire est un jeu 2 joueurs choisis parmi une quinzaine de jeu propos s par l quipe enseignante Il doit contenir 1 Une interface graphique 2 Un algorithme classique non trivial pour faire jouer la machine 3 Un arbitre g rant les parties tour de jeu d signation du gagnant des coups interdits 18 Chapitre 2 Activit s d enseignement Les trois premiers jours du projet sont consacr s la programmation d un jeu simple identique pour tous les groupes qui leur permet d talonner leurs m thodes d valuer l ampleur du travail et la n cessit de mieux s organiser Puis le vrai projet commence Il est ponctu de plusieurs cours magistraux expliquant certains points g n raux ou techniques utiles la r alisation du logiciel 2 cours d Interface Homme Machine 1 cours de strat gie de jeu Chaque groupe se voit assign un tuteur membre de l quipe enseignante qui sert avant tout de conseiller et d aide L valuation se fait sur pr sentation oral avec d monstration ainsi que sur plusieurs documents produire pendant le projet manuel d utilisateur livret de conception Commentaires Les difficult s principales de ce projet r sident dans la taille du logiciel demand et dans la n cessit de travailler en quipe
51. ursuis mes travaux de recherches dans la continuit de ma th se Pendant l t 2001 juillet septembre compris j ai effectu mon stage de magist re au sein du D partement d Informatique et Math matiques de l Universit de Stirling en cosse La section 1 2 d crit ce travail et en donne quelques perspectives 1 1 Sp cification et Validation des Syst mes R actifs Verimag est une unit mixte de recherche affili e au CNRS l UJF et INPG dirig e par Mr Joseph Si fakis Depuis sa cr ation en 1993 le laboratoire m nent des travaux visant produire des outils th oriques et techniques pour permettre le d veloppement de syst mes embarqu s de qualit ma tris e Pendant les 10 derni res ann es Verimag a contribu activement au d veloppement de l tat de l art dans les domaines des langages synchrones de la v rification par model checking du test et de la mod lisation des syst mes Les r sultats du laboratoire trouvent de nombreuses applications industrielles notamment dans des outils pour le d veloppement des logiciels et syst mes embarqu s En 2000 2001 j ai effectu mon DEA au sein du laboratoire plus pr cis ment dans l quipe Langages Syn chrones et Syst mes R actifs dirig e par Mr Nicolas Halbwachs sous la direction de Mme Florence Mara ninchi Durant cette ann e j ai tudi la g n ration de code efficace partir des it rateurs de tableaux LUSTRE voir section 1
52. vers le langage synchrone lustre Master s thesis UFRIMA UJF Grenoble 2002 P Wadler Listlessness is better than laziness In Conference Record of the 1984 ACM Symposium on Lisp and Functional Programming pages 45 52 ACM ACM august 1984 P Wadler Deforestation transforming programs to eliminate trees Theoretical Computer Science 73 231 248 90 H Y Wang and R K Brayton Input Don t Care Sequences in FSM Networks In IEEE ACM International Conference on CAD pages 321 329 Santa Clara California November 1993 ACM IEEE IEEE Computer Society Press H Y Wang and R K Brayton Permissible observability relations in FSM networks In Michael Lorenzetti editor Pro ceedings of the 31st Conference on Design Automation pages 677 683 New York NY USA June 1994 ACM Press
53. yse syntaxique et g n ration de code A partir d un squelette d assembleur j ai isol les parties qui me paraissaient pertinentes pour comprendre ces 3 tapes et j ai demand aux tudiants de les d velopper tant donn e la dur e courte du projet seulement 19 une semaine j ai videment insist pour qu ils r alisent l ensemble de la cha ne de compilation pour quelques instructions seulement L extension au jeu d instruction entier ne pr sente en effet aucun probl me fondamental une fois qu on a compris comment faire pour une instruction Ce projet a aussi compris une partie cours 3h durant laquelle j ai rappel aux tudiants les notions fondamentales des th mes suivants 1 analyse lexicale expressions r guli res leur reconnaissance 2 analyse syntaxique grammaires ambiguit s 3 construction d une table des symboles 4 langage d assemblage qui devaient leur permettre d accomplir leur projet L va luation s est faite par une d monstration du logiciel d velopp par chaque bin me Commentaires Cet enseignement m a permis d appr hender les difficult s principales li es ce type d acti vit J ai pr par un cours d introduction dans lequel j ai synth tis plusieurs th mes larges faisant tous partie du domaine de la compilation Bien qu utilisant les bases d un projet pr existant j ai eu l occasion de pr parer un projet de taille raisonnable Il a fallu sp
54. yst matiquement consid rer que cette propri t est un invariant Suivant les m thodes classiques de la logique de Hoare Hoa69 il est alors suffisant de prouver la propri t est vrai avant le passage dans la boucle et qu elle est pr serv e par un passage dans celle ci Une r ponse positive indique toujours que la propri t est satisfaite Par contre une r ponse n gative ne peut tre interpr t e soit la propri t est un invariant et n est pas v rifi e soit la propri t n est pas un invariant Nous nous int ressons ensuite l extension de cette m thode aux programmes manipulant des encha nements d it rations comme d crit plus haut Nous montrons que la transformation d crite ci dessus se propage facile ment ces encha nements d it rations Contrats pour des syst mes r actifs En essayant d largir la r flexion engag e au d but de la th se nous avons consid r la forme la plus simple de structuration des programmes en LUSTRE celle de noeud Pour cela nous avons commenc tudier la notion de contrats dans le cadre des syst mes r actifs Un contrat sp cifie comment un composant interagit avec son environnement Il est constitu d une clause assume ou require qui correspond aux hypoth ses que fait le composant sur son environnement et d une clause guarantee qui sp cifie quels comportements le composant assure lorsque plac dans un environnement satisfaisant la clause assume La n
Download Pdf Manuals
Related Search