@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib matthieu_moy.bib -c year=2011 -ob 2011.bib}}
@inproceedings{MARQUET:2011:HAL-00557515:1,
hal_id = {hal-00557515},
url = {http://hal.archives-ouvertes.fr/hal-00557515/en/},
title = { {E}fficient {E}ncoding of {S}ystem{C}/{TLM} in {P}romela},
author = {Marquet, Kevin and Moy, Matthieu and Jeannet, Bertrand},
abstract = {{T}o deal with the ever growing complexity of {S}ystems-on-{C}hip, designers use models early in the design flow. {S}ystem{C} is a commonly used tool to write such models. {I}n order to verify these models, one thriving approach is to encode its semantics into a formal language, and then to verify it with verification tools. {V}arious encodings of {S}ystem{C} into formal languages have already been proposed, with different performance implications. {I}n this paper, we investigate a new, automatic, asynchronous means to formalize models. {O}ur encoding supports the subset of the concurrency and communication constructs offered by {S}ystem{C} used for high-level modeling. {W}e increase the confidence in the fact that encoded programs have the same semantics as the original one by model-checking a set of properties. {W}e give experimental results on our formalization and compare with previous works.},
keywords = {{S}ystem{C}, {T}ransaction-{L}evel {M}odeling, {P}romela, {S}pin, {M}odel-checking},
booktitle = {{DATICS}-{IMECS}},
address = {{H}ong-{K}ong },
collaboration = {{P}rojet {M}inalogic {O}pen{TLM}},
day = {16},
month = {03},
year = {2011},
pdf = {http://www-verimag.imag.fr/~moy/publications/datics-imecs2011.pdf}
}
@inproceedings{FMMM-RAPIDO-11,
title = {Faithfulness Considerations for Virtual Prototyping of Systems-on-Chip },
author = {Funchal, Giovanni and Moy, Matthieu and Maillet-Contoz, Laurent and Maraninchi, Florence},
month = {jan},
year = {2011},
booktitle = {3rd Workshop on: Rapid Simulation and Performance Evaluation: Methods and Tools (RAPIDO)},
address = {Heraklion, Crete, Greece},
team = {SYNC},
abstract = {Virtual prototypes are simulators used in the consumer
electronics industry. They enable the development of
embedded software before the real, physical hardware
is available, hence providing important gains in
speed of development and time-to-market.
Transaction-level Modeling (TLM) is a widely used
technique for designing such virtual prototypes. Its
main insight is that many micro-architectural
details (i.e. caches, fifos and pipelines) can be
omitted from the model as they should not impact the
behavior perceived from a software programmer's
point-of-view. In this paper, we shall see that this
assumption is not always true, specially for
low-level software (e.g. drivers). As a result,
there may be bugs in the software which are not
observable on a TLM virtual prototype, designed
according to the current modeling practices. We call
this a "faithfulness" issue. Our experience shows
that many engineers are not aware of this issue.
Therefore, we provide an in-depth and intuitive
explanation of the sort of bugs that may be missed.
We claim that, to a certain extent, modified TLM
models can be faithful without losing the benefits
in terms of time-to-market and ease of modeling.
However, further investigation is required to
understand how this could be done in a more general
framework.},
url = {http://www-verimag.imag.fr/~moy/publications/rapido2010.pdf}
}
@inproceedings{FunchalDATE2011,
title = {{jTLM}: an Experimentation Framework for the Simulation of Transaction-Level Models of Systems-on-Chip},
author = {Funchal, Giovanni and Moy, Matthieu},
booktitle = {Design, Automation and Test in Europe (DATE)},
url = {http://www-verimag.imag.fr/PUBLIS/uploads/aexel3895.pdf},
team = {SYNC},
year = {2011},
abstract = {Virtual prototypes are simulators used in the consumer electronics industry. Transaction-level Modeling (TLM) is a widely used technique for designing such virtual prototypes. In particular, they allow for early development of embedded software.
The SystemC modeling language is the current industry standard for developing virtual prototypes. Our experience suggests that writing TLM models exclusively in SystemC leads sometimes to confusion between modeling concepts and their implementation, and may be the root of some known bad practices.
This paper introduces jTLM, an experimentation framework that allow us to study the extent to which common modeling issues come from a more fundamental constraint of the TLM approach. We focus on a discussion of the two modes of simulation scheduling: cooperative and preemptive. We confront the implications of these two modes on the way of designing TLM models, the software bugs exposed by the simulators and the performance. },
note = {acceptance rate : 314/950 = 33\%, Rank A+ GDR SoC-SiP}
}
@inproceedings{MOY:2011:HAL-00574783:1,
hal_id = {hal-00574783},
url = {http://hal.archives-ouvertes.fr/hal-00574783/en/},
title = {{E}fficient and {P}layful {T}ools to {T}each {U}nix to {N}ew {S}tudents},
author = {Moy, Matthieu},
abstract = {{T}eaching {U}nix to new students is a common tasks in many higher schools. {T}his paper presents an approach to such course where the students progress autonomously with the help of the teacher. {T}he traditional textbook is complemented with a wiki, and the main thread of the course is a game, in the form of a treasure hunt. {T}he course finishes with a lab exam, where students have to perform practical manipulations similar to the ones performed during the treasure hunt. {T}he exam is graded fully automatically. {T}his paper discusses the motivations and advantages of the approach, and gives an overall view of the tools we developed. {T}he tools are available from the web, and open-source, hence re-usable outside the {E}nsimag.},
keywords = {{U}nix, {E}ducation, {E}xam, {T}reasure {H}unt},
language = {{A}nglais},
affiliation = {{VERIMAG} - {IMAG} - {CNRS} : {UMR}5104 - {U}niversit{\'e} {J}oseph {F}ourier - {G}renoble {I} - {I}nstitut {N}ational {P}olytechnique de {G}renoble - {INPG} },
booktitle = {16th {A}nnual {C}onference on {I}nnovation and {T}echnology in {C}omputer {S}cience {E}ducation {IT}i{CSE} },
address = {{D}armstadt {A}llemagne },
audience = {internationale },
day = {27},
month = {06},
year = {2011},
pdf = {http://hal.archives-ouvertes.fr/hal-00574783/PDF/unix-course.pdf},
note = {Acceptance rate : 66/169 = 39\%, Rank A CORE 2014}
}
@inproceedings{FUNCHAL:2011:HAL-00595637:1,
hal_id = {hal-00595637},
url = {http://www-verimag.imag.fr/~moy/publications/jtlm-during.pdf},
title = { Modeling of Time in Discrete-Event Simulation of Systems-on-Chip},
author = {{F}unchal, {G}iovanni and Moy, Matthieu},
abstract = {{T}oday's consumer electronics industry uses modeling and simulation to cope with the complexity and time-to-market challenges of designing high-tech devices. {I}n such context, {T}ransaction-{L}evel {M}odeling ({TLM}) is a widely spread modeling approach often used in conjunction with the {IEEE} standard {S}ystem{C} discrete-event simulator. {I}n this paper, we present a novel approach to modeling time that distinguishes between instantaneous actions and tasks with a duration. {W}e argue that this distinction should be natural to the user. {I}n addition, we show that it gives us important insight and better comprehension of what actions can overlap in time. {W}e are able to exploit this distinction to parallelize the simulation, achieving an important speedup and exposing subtle software bugs related to parallelism. {W}e propose a set of primitives and discuss the design decisions, expressiveness and semantics in depth. {W}e present a research simulator called j{TLM} that implements all these ideas.},
keywords = {{TLM}, time, duration, {J}ava, {jTLM}},
language = {{A}nglais},
affiliation = {{VERIMAG} - {IMAG} - {CNRS} : {UMR}5104 - {U}niversit{\'e} {J}oseph {F}ourier - {G}renoble {I} - {I}nstitut {N}ational {P}olytechnique de {G}renoble - {INPG} - {STM}icroelectronics ({G}renoble) - {ST}-{GRENOBLE} - {STM}icroelectronics },
booktitle = {{ACM}/{IEEE} {N}inth {I}nternational {C}onference on {F}ormal {M}ethods and {M}odels for {C}odesign {MEMOCODE} },
address = {{C}ambridge {R}oyaume-{U}ni },
audience = {internationale },
collaboration = {{HELP} },
day = {11},
month = {07},
year = {2011},
note = {Acceptance rate : 16/43 = 37\%}
}
@inproceedings{ALTISEN:2011:HAL-00648628:1,
author = {Karine Altisen and Matthieu Moy},
hal_id = {hal-00648628},
url = {http://www-verimag.imag.fr/~moy/publications/wctt2011.pdf},
title = {Causality closure for a new class of curves in real-time calculus},
abstract = {{Real-Time Calculus (RTC) is a framework to analyze heterogeneous real-time systems that process event streams of data. The streams are characterized by arrival curves which express upper and lower bounds on the number of events that may arrive over any specified time interval. System properties may then be computed using algebraic techniques in a compositional way. The property of causality on arrival curves essentially characterizes the absence of deadlock in the corresponding generator. A mathematical operation called causality closure transforms arbitrary curves into causal ones. In this paper, we extend the existing theory on causality to the class Upac of infinite curves represented by a finite set of points plus piecewise affine functions, where existing algorithms did not apply. We show how to apply the causality closure on this class of curves, prove that this causal representative is still in the class and give algorithms to compute it. This provides the tightest pair of curves among the curves which accept the same sets of streams.}},
keywords = {algorithms, causality, real-time calculus},
language = {Anglais},
affiliation = {Verimag - IMAG},
booktitle = {{Proceedings of the 1st International Workshop on Worst-Case Traversal Time}},
publisher = {ACM},
pages = {3--10},
address = {Vienna, Autriche},
audience = {internationale},
doi = {10.1145/2071589.2071590 },
year = {2011},
pdf = {http://hal.archives-ouvertes.fr/hal-00648628/PDF/wctt2011-final.pdf}
}
@online{unix-training-software,
author = {Matthieu Moy},
title = {Unix-training: a set of tools to teach {U}nix efficiently},
howpublished = {Published as Free Software (LGPL License)},
year = 2011,
url = {http://www-verimag.imag.fr/~moy/?Unix-training-a-set-of-tools-to}
}
@online{pagai-software,
author = {Julien Henry and David Monniaux and Matthieu Moy},
title = {{PAGAI} static analyzer: Path Analysis for invariant Generation by Abstract Interpretation},
howpublished = {Published as Free Software (CECILL-C License)},
year = 2011,
url = {https://forge.imag.fr/projects/pagai/}
}
This file was generated by bibtex2html 1.98.