Research | People | Tool | Teaching | Publications | Misc
Research themes
Formal verification of real-time systems in the context of a preemptive scheduling policy
I study Scheduling Time Petri Nets as introduced by Roux and Déplanche: this extension consists in mapping into the Petri net model the way the different schedulers of the system activate or suspend the tasks (stopwatches).
I work on an extension (based on polyhedral computation) of the classical state class graph for this model.
Time Petri nets with discrete time semantics
Study of a new type of data-structure adapted to the computation of the state class graph of a T-Time Petri Net with discrete semantics. We currently seek to extend the state class graph method to time Petri nets with inhibitor arcs (and hyperarcs) with a discrete time approach. This work is based on the research of the real-time systems team about extensions of BDD (Binary Decision Diagrams), e.g. VDD (Vector Decision Diagram).
Scientific community
I work with:
Member of the program committee of RJCITR05.
- Didier Lime
- Jean-Pierre Elloy, my PhD adviser
- Guillaume Gardey
- Olivier (H.) Roux, co-adviser
- Pierre Molinaro, co-adviser
Member of the program committee of RJCITR05.
Tool
I am involved in the development of Romeo, a software studio for Time Petri Net analysis: Romeo performs analysis on T-Time Petri nets and on one of their extension to scheduling. It is composed of a GUI (written in Tcl/Tk) and of two modules (written in C++) for computing the state space.
Romeo is a free software, distributed under GPL License, for Windows, Linux and MacOS X platforms.
Romeo is a free software, distributed under GPL License, for Windows, Linux and MacOS X platforms.
Teaching
I teach at the Mathematics and Informatics Department of the engineering school Ecole Centrale de Nantes. I supervise courses, directed works and lab works in:
Information Technology and Communication
Algorithmics and Programming (C)
Programming methods (object-oriented programming, data structure, Java)
Real-time systems
Publications
Book chapter
| [AM08] | Alexandre David and Morgan Magnin. Outils pour l'analyse des modèles temporisés. In Systèmes embarqués communicants - Approches formelles, Traité IC2 (Hermès), 30 pages, To appear in 2008. [bib] |
International conference papers
| [MLR08] | Morgan Magnin, Didier Lime and Olivier H. Roux, Symbolic state space of Stopwatch Petri nets with discrete-time semantics. To appear in the 29th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (ATPN 2008), Xi'an, China. [bib] |
| [MMR06a] | Morgan Magnin, Pierre Molinaro and Olivier H. Roux. Decidability, expressivity and state-space computation of Stopwatch Petri nets with discrete-time semantics. To appear in the 8th International Workshop on Discrete Event Systems (WODES 2006), Ann Arbor, USA, july 2006. [bib] |
| [MLR05a] | Morgan Magnin, Didier Lime and Olivier H. Roux. An efficient method for computing exact state space of Petri nets with stopwatches. In the 3rd International Workshop on Software Model-Checking (SoftMC 2005), Edinburgh, Scotland, UK, july 2005. Elsevier. [slides] [bib] |
| [GLMR05] | Guillaume Gardey, Didier Lime, Morgan Magnin and Olivier H. Roux. Roméo: A Tool for Analyzing Time Petri Nets. To appear in the 17th International Conference on Computer-Aided Verification (CAV 2005), Edinburgh, Scotland, UK, july 2005. Copyright Springer-Verlag. [bib] |
National conference papers
| [SLRM06] | Charlotte Seidner, Jean-Philippe Lerat, Olivier H. Roux and Morgan Magnin. Vérification dynamique et formelle d'un système décrit par son architecture fonctionnelle à l'aide de réseaux de Petri temporels : promesses et perspectives. In the 4th AFIS Conference, may 2006, Toulouse, France. To appear. [bib] |
Technical reports
| [MMR06b] | Morgan Magnin, Pierre Molinaro and Olivier H. Roux. How to deal efficiently with Petri nets with stopwatches in discrete-time? IRCCyN Technical report number R2006_1, 2006. [pdf] |
| [MLR05b] | Morgan Magnin, Didier Lime and Olivier H. Roux. Improved algorithm for computing exact state space of Petri nets with stopwatches. IRCCyN Technical report number R2005_15, 2005 [pdf] |
Other
| [M06] | Morgan Magnin. Comment vérifier a priori le bon fonctionnement des systèmes électroniques et informatiques dans une voiture ? Poster for an exhibition at the so-called Champs Libres, Rennes, France, may 2006. [pdf] |
| [MEMR06] | Morgan Magnin, Jean-Pierre Elloy, Pierre Molinaro and Olivier H. Roux. Why discrete-time Petri nets with stopwatches ? Poster for the 6th PhD Students JDOC meetings, St Nazaire, april 2006. [pdf] |
| [MAG04a] | Morgan Magnin. Vérification de réseaux de Petri temporels étendus à l'aide de polyèdres. Master Thesis, Ecole Centrale de Nantes, France, 2004 |
| [MAG04b] | Morgan Magnin. Etude de la Vérification des Automates Hybrides. Master Bibliography, Ecole Centrale de Nantes, France, 2004 (in french) |
General courses
| [RMM05] | Olivier Roux, Guillaume Moreau et Morgan Magnin. Méthodes Logicielles (i.e. Programming methods). General engineer training programme. Ecole Centrale de Nantes, France, september 2005. [pdf] |
Electronic courses
| [M05] | Morgan Magnin. Initiation à Linux (i.e. Tutorial to Linux). General engineer training programme. Ecole Centrale de Nantes. |
Misc
Informatics
I am very interested in all studies about the use of new concepts like weblogs, wiki, syndication, social networks, ... I have a personal weblog (in french) since 2001.
- In 2003, I was involved in a project for determining how weblogs and syndication could be used in the context of an engineering school.
- In 2004, I supervised a project led by two students from Ecole Centrale Nantes about the wiki concept and its possible applications in an universitary framework.
- In 2005, I initiated and led personnaly a project that aimed to install a SPIP publishing system on the collaborative learning environment of Centrale Nantes. I worked with Guillaume Moreau, Teaching and Learning Information Technologies manager.
In september 05, the official release of Central'Info (this new publishing SPIP platform) came with an electronic tutorial to Linux I wrote. I'm in charge of the animation of Central'Info. - In 2006, I have been invited to talk at the 5th CRITE workshop about my work on Central'Info. This workshop focused on the various ways teachers and professors may create interactive courses with the help of different kinds of collaborators.
Media
I was involved in the creation of a french professional magazine about japanese pop culture (mangas, animated series, music). During two years, I regularly wrote in it as freelance journalist.
Morgan Magnin

