Jean-Vivien Millo

PhD in Computer Science
PostDoc in EPI AOSTE, INRIA Sophia-Antipolis
(+33)0603563330 – jvmillo[at]gmail[dot]com







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 designUniversity 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 FrenchPDFBibtex
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]PDFBibtex
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]PDFBibtex
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]PDFBibtex
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]PDFBibtex
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] PDFBibtex
Jean-Vivien Millo, S Ramesh, S Krishna, Ganesh N
Compositional Verification of Software Product Lines
Integrated Formal Methods 2013, Turku, Finland
[MSR2012]PDFBibtex
Swarup Mohalik, Jean-Vivien Millo, S Ramesh, Krishna S, Ganesh K
Tracing SPLs Precisely and Efficiently
SPLC’2012, Salvador, Brazil, September 2012
[MSR2011]PDFBibtex
Jean-Vivien Millo, Swarup Mohalik, S Ramesh
Integrated analysis of software product lines
ISEC’2011, Trivandrum, Kerala, India, February 2011
[BMS2006c]PDFBibtex
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] PDFBibtex
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]PDFBibtexVideo
Jean-Vivien Millo, S Ramesh
Relating Requirement and Design Variabilities
SQAM’2012, Hong Kong, December 2012
[MS2012]PDFBibtex
Jean-Vivien Millo, Robert de Simone
Refining cellular automata with routing constraints
Automata and JAC 2012, Bastia, Corsica, France, September 2012
[BM2007]PDFBibtex
Julien Boucaron, Jean-Vivien Millo
Compositionality of Statically Scheduled IP
FMGALS Workshop, Nice, France, July 2007
[BMS2006a]PDFBibtex
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]PDFBibtex
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-Antipolis

Concurrency 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-Antipolis

Languages 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




Last update: 19/12/2011

top