Current position
I'm currently in post-doc (ingénieur de recherhce) in the AOSTE team of INRIA Sophia-Antipolis. My current research projects are:
- Generation of multi-threaded code from data-flow applications to MPPA platform.
- Explicit routing of data-flow applications through a network on chip.
- Verification of control design against scenarios using a synchronous approach.
- Verification of the traceability between design and requirement in an SPL context.
Research interests
Modeling, Analysis, and optimization of embedded system with real-time constraint
My PhD thesis [M2008] was about static scheduling of Marked/Event Graph (MG). We have design an algorithm to statically schedule any MG with the best achievable throughput and the minimal token accumulation.
This work extends the theory of Latency Insensitive Design (LID). This last tackles the problem of latency on long interconnection wires in a System-on-Chip (SoC). A long latency breaks the synchronous hypothesis where communications are supposed to be instantaneous. In our first attempt [BMS2007], we tried to reduce the overhead of communication buffering required by the solution proposed by Luca Carloni in his thesis. To do so, we used the predictability of the MG. During my PhD, I have improved this method so that it always returns the optimal solution.
During my second Post-Doc, back to INRIA, I start to work on the modeling of highly parallel application. The goal is to ease the mapping of such an application on a parallel platform. Such mapping will be done ether at compile time or while refining our model in a language that explicit the structure of the targeted architecture including the computation elements but also the communication elements.
Formal Analysis of Software Product Line (SPL)
During my Post-Doc at India Science Lab, General Motors R\&D, Bangalore, India, I focus my interest on the representation of the variability in the SPL. Variability is the heart of an SPL but is not always considered as a first class citizen. It appears at every level of the software engineering flow (Requirement, Design, Implementation, and Test).
In a first work [MSR2010], we have extracted variability from every level of representation (feature diagram, architecture, behavioral model) and integrated it in a coherent framework across level. Thus we ran many analyzes based on consistency checking.
In a second work [MSR2012], we have focused our interest on the traceability across requirement and design still in the context of SPL.
In a third one [MRKG2013], we have proposed a design verification method that limits the combinatorial explosion of the complexity due to the presence of variability.
In the last one [MMCR2013], we propose a scenario based language to write observer in the context of SPL. The full verification framework that checks the design against the observer is provided.
top
CV
[In pdf: English]Work experiences
| 2011-2013 | Teaching assistant (200 hours) | University of Nice Sophia-Antipolis, France |
| 2011-2013 | PostDoc (2 years) | EPI Aoste, INRIA Sophia-Antipolis, France |
| 2009-2011 | PostDoc (2 years, 5 mois) | India Science Lab, General Motors R&D, Bangalore, India |
| 2006-2008 | PhD Student (3 years) | EPI Aoste, INRIA Sophia-Antipolis, France |
| 2005 | Research Engineer (10 months) | EPI Aoste, INRIA Sophia-Antipolis, France |
Diplomas
| 2008 | PhD degree on embedded systems and SoC design | University of Nice Sophia-Antipolis, France |
| « Ordonnancements périodique dans les réseaux de processus: | ||
| application à la conception insensible aux latences ». | ||
| Jury: Michel Auguin, Gaël Clavé, Marc Pouzet, | ||
| Bruno Gaujal, et Robert de Simone | ||
| 2005 | Engineering degree on embedded systems and telecom | ESIGETEL, Avon (77), France |
| 2005 | MSc degree on theoretical & applied computer science | University of Marne la Vallée, France |
| 2003 | BSc on computer science | University of Marne la Vallée, France |
| 2002 | French academic DUT on computer science | University of Nice Sophia-Antipolis, France |
| 2000 | French Baccalaureate in science (high school diploma) | Lycée Horticole d'Antibes, France |
skills
| Research topics: High level modelling of embedded and real-time system, compiler and code optimization, SoC design, scheduling, verification and validation of hardware/ software design, synchronous languages, software product line, variability management, traceability management. |
| Theoretical Sciences: Concurrency theory, Models of computation (Petri net, Kahn network, synchronous data flow…), operational research, automata theory, formal languages. |
| Standards and Languages: Java, C, C++, Latex, UML Marte, AUTOSAR, Esterel, SCADE, Lustre, Simulink/ Stateflow. |
| Languages: English: Fluent, French: Mother tong |
| Sports: Climbing, Hiking, Volley-ball, Basket-ball (Coaching and playing) |
top
Publications
[pdf] [Bibtex]PhD Thesis: | |||
| [M2008] in French | Bibtex | ||
| Jean-Vivien Millo | |||
| Ordonnancements périodique dans les réseaux de processus: application à la conception insensible aux latences. | |||
| University of Nice Sophia-Antipolis, December 2008 | |||
| My PhD thesis is available as a hard cover book [French] | |||
| My PhD results have also been published in [MdS2012] in English | |||
International peer reviewed journals: | |||
| [MS2013] | Bibtex | ||
| Jean-Vivien Millo, Robert de Simone | |||
| Explicit routing schemes for implementation of cellular automata on processor arrays | |||
| Special issues of Natural Computing Journal (NaCo) (To be published) | |||
| [MdS2012] | Bibtex | ||
| Jean-Vivien Millo, Robert de Simone | |||
| Periodic scheduling of marked graphs using balanced binary words | |||
| Theoretical Computer Science, Volume 458, pages 113-130, November 2012, Elsevier | |||
| [GDMMBG2012] | Bibtex | ||
| Calin Glitia, Julien DeAntoni, Frédéric Mallet, Jean-Vivien Millo, Pierre Boulet, Abdoulaye Gamatié | |||
| Progressive and Explicit Refinement of Scheduling for Multidimensional Data-Flow Applications using UML MARTE | |||
| Special issue of Design Automation for Embedded System, Volume 16, Issue 2, pages 137-169, 2012, Springer Netherlands | |||
| [BMS2007] | Bibtex | ||
| Julien Boucaron, Jean-Vivien Millo, Robert de Simone | |||
| Formal methods of scheduling of Latency-insensitive designs | |||
| EURASIP journal on Embedded System, Volume 2007, pages 8--8, January 2007 | |||
International peer reviewed conferences: | |||
| [MRKG2013] | Bibtex | ||
| Jean-Vivien Millo, S Ramesh, S Krishna, Ganesh N | |||
| Compositional Verification of Software Product Lines | |||
| Integrated Formal Methods 2013, Turku, Finland | |||
| [MSR2012] | Bibtex | ||
| Swarup Mohalik, Jean-Vivien Millo, S Ramesh, Krishna S, Ganesh K | |||
| Tracing SPLs Precisely and Efficiently | |||
| SPLC’2012, Salvador, Brazil, September 2012 | |||
| [MSR2011] | Bibtex | ||
| Jean-Vivien Millo, Swarup Mohalik, S Ramesh | |||
| Integrated analysis of software product lines | |||
| ISEC’2011, Trivandrum, Kerala, India, February 2011 | |||
| [BMS2006c] | Bibtex | ||
| Julien Boucaron, Jean-Vivien Millo, Robert de Simone | |||
| Latency-insensitive design and central repetitive scheduling | |||
| MEMOCODE'06, pages 175-183, Piscataway, NJ, USA, July 2006 | |||
International invited journal: | |||
| [MMCR2013] | Bibtex | ||
| Jean-Vivien Millo, Frédéric Mallet, Anthony Coadou, S Ramesh | |||
| Scenario-based verification in presence of variability using a synchronous approach | |||
| Invited paper in Frontiers of Computer Science, Springer | |||
Workshops: | |||
| [MRsqam2012] | Bibtex | Video | |
| Jean-Vivien Millo, S Ramesh | |||
| Relating Requirement and Design Variabilities | |||
| SQAM’2012, Hong Kong, December 2012 | |||
| [MS2012] | Bibtex | ||
| Jean-Vivien Millo, Robert de Simone | |||
| Refining cellular automata with routing constraints | |||
| Automata and JAC 2012, Bastia, Corsica, France, September 2012 | |||
| [BM2007] | Bibtex | ||
| Julien Boucaron, Jean-Vivien Millo | |||
| Compositionality of Statically Scheduled IP | |||
| FMGALS Workshop, Nice, France, July 2007 | |||
| [BMS2006a] | Bibtex | ||
| Julien Boucaron, Jean-Vivien Millo, Robert de Simone | |||
| Another glance at relay Stations in Latency-insensitive design | |||
| Electr. Notes Theor. Comput. Sci. Volume 146, issue 2, pages 41-59, 2006 | |||
Miscellaneous: | |||
| [BMS2006b] | Bibtex | ||
| Julien Boucaron, Jean-Vivien Millo, Robert de Simone | |||
| Latency-insensitive design: Dynamic and Static scheduling with proper formal devices | |||
| SAME'06, Sophia-Antipolis, France, October 2006 |
top
Teaching
2012-13
Advanced Object oriented programing, First year, Master miage, University of Nice Sophia-AntipolisConcurrency and parallelism, First year, International master in computer science, University of Nice Sophia-Antipolis
System, First year, Licence in computer science, University of Nice Sophia-Antipolis
2011-12
Object oriented programing and design pattern, First year, Master miage, University of Nice Sophia-AntipolisLanguages and Automata, Licence 3 in computer science, University of Nice Sophia-Antipolis
HTML and CCS, DUT computer Science, University of Nice Sophia-Antipolis
Introduction to Database Management Systems, Licence 3 in computer science, University of Nice Sophia-Antipolis
Formal Models for Network-on-Chips (Foundations and models for the design of on-chip systems and networks), Master International Ubinet 2, Polytech Nice Sophia-Antipolis engineering school
top
Tools
K-PASSA v1.1
K-PASSA stands for "K-Periodic Asap Static Schedule Analyser". K-PASSA is for modeling and analysing Marked Graph. It implements the equalization process presented in Julien Boucaron's thesis but also the balanced scheduling algorithm presented in my thesis and in [MS2012].
A stand alone version of K-PASSA available >>>>>here<<<<<.
The current version is stable.
The source files of KPassa are available here.
K-PASSA uses the lpsolve library as an LP solver.
To get it for 32/64 bit Unix/Linux and JDK 6, follow the link
Extract the two .so files from the archive and put them in /usr/lib.
Otherwise, put them where you want and set the LD_LIBRARY_PATH to this location.
Another solution is to simply put the two .so files in the installation directory of KPassa.
To get it for 64 bit windows and JDK 6, follow the link
To get it for 64 bit Mac and JDK 6, follow the link
To get the same for other archi/OS, please go on the web site of lpsolve:
http://sourceforge.net/projects/lpsolve/.
Enjoy !
An open question:
The major upgrade from K-PASSA v1 to v1.1 is the balanced scheduling algorithm presented in [MS2012].
This algorithm is applicable to strongly connected graph however, K-PASSA allows simply connected graph.
To fill the gap, simply connected graphs are over constrained in strongly connected graphs in a brute force manner.
A smarter extension of the balanced scheduling algorithm to simply connected graph is still open.
Why K-PASSA v1.1 in parallel to
K-PASSA v2?
K-PASSA v1 has been developped in 2007. In 2008 and 2009, Julien Boucaron has developped
K-PASSA v2 from scratch. In K-PASSA v2, not only Marked Graph but also Latency Insensitive Design,
Synchronous Data Flow, and K-periodic Routing Graph can be manipulated and analysed.
After my Post-Doc in India Science Lab (GM R&D), I wanted to integrate in K-PASSA
the scheduling algorithm I developped during my PhD thesis. This algorithm is very
specific to Marked Graph and it has been easier for me to exdend the v1 that I have
built than discovering the internal structure of the v2.
SPLEnD: SPL Engine for Design Verification
SPLEnD is the first compositional design verification engine for software product lines(SPLs). The SPL development exploits the reuse of common features among the products which reduces development and validation resources. The variability among different products in an SPL are managed at every stage of development and are often captured at different abstraction levels.
SPLEnD assumes that each SPL is composed of multiple features with each feature exhibiting variability. Further the variability information is captured possibly at different levels of abstractions in the design and requirement stages. The design verification involves formally checking whether the given requirements of an SPL is satisfied by the given design. One of the novel aspects of SPLEnD is that it enables compositional verification of designs against requirements. This involves first verifying the individual features separately, which provides a mapping between the variabilities at the requirement and design levels. Feature level verification essentially involves standard model checking, while for the second step, a QBF formula is synthesized and solved that checks conformance of the entire SPL in one go. The QBF formula avoids the explicit enumeration of all possible variant combinations thereby reducing the verification effort greatly. SPLEnD uses SPIN for the first step while CirQit is used for the second step. Thanks to the compositionality, SPLEnD easily handles the evolution of SPL by addition of new features and modification of existing features. Initial experimental results with SPLEnD look very promising: SPLs with several thousands of features were verified efficiently.
A demo of SPLEnD is available as a video.
The following paper presents the tool and this other paper presents the theory behind the tool.
The JAVA source file of the tool are available here along with some case studies.
top
