@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib matthieu_moy.bib -c year=2010 -ob 2010.bib}}
@inproceedings{causality-tacas2010,
author = {Karine Altisen and Matthieu Moy},
title = {Arrival Curves for Real-Time Calculus: the Causality Problem and its Solutions},
booktitle = {TACAS},
year = 2010,
month = {March},
pages = {358--372},
editor = {J. Esparza and R. Majumdar},
url = {http://www-verimag.imag.fr/~moy/publications/rtc-causality.pdf},
abstract = { The Real-Time Calculus (RTC) is a framework to analyze
heterogeneous real-time systems that process event streams of data.
The streams are characterized by pairs of curves, called arrival
curves, that 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.
A well-known limitation of RTC is that it cannot model systems with
states and recent works
studied how to interface RTC curves with state-based models.
Doing so, while trying, for example to generate a stream of events
that satisfies some given pair of curves, we faced a
causality problem: it can be the case
that, once having generated a finite prefix of an event stream, the
generator deadlocks, since no extension of the prefix can satisfy
the curves anymore. When trying to express the property of the
curves with state-based models, one may face the same problem.
This paper formally defines the problem on arrival curves, and gives
algebraic ways to characterize causal pairs of curves, i.e. curves
for which the problem cannot occur.
Then, we provide algorithms to compute a causal pair of curves
equivalent to a given curve, in several models. These algorithms
provide a canonical representation for a pair of curves, which is
the best pair of curves among the curves equivalent to the ones they
take as input.
},
note = {Acceptance rate: 24/110 = 21\%, Rank A CORE 2014}
}
@inproceedings{rtc-ta-granularity,
author = {Karine Altisen and Yanhong Liu and Matthieu Moy},
title = {Performance Evaluation of Components Using a Granularity-based Interface Between Real-Time Calculus and Timed Automata},
booktitle = {Eighth Workshop on Quantitative Aspects of Programming Languages (QAPL)},
publisher = {Electronic Proceedings in Theoretical Computer Science},
year = 2010,
address = {Paphos, Cyprus},
month = {March},
url = {http://www-verimag.imag.fr/~moy/publications/gran-paper.pdf},
abstract = { To analyze complex and heterogeneous real-time embedded systems,
recent works have proposed interface techniques between
real-time calculus (RTC) and timed automata (TA), in order
to take advantage of the strengths of each technique for analyzing
various components. But the time to analyze a state-based component
modeled by TA may be prohibitively high, due to the state space
explosion problem. In this paper, we propose a framework of
granularity-based interfacing to speed up the analysis of a TA
modeled component. First, we abstract fine models to work with
event streams at coarse granularity. We perform analysis of the
component at multiple coarse granularities and then based on RTC
theory, we derive lower and upper bounds on arrival patterns of
the fine output streams using the causality closure algorithm of
\cite{causality-TACAS10}. Our framework can help to achieve
tradeoffs between precision and analysis time.}
}
@inproceedings{ac2lus,
author = {Karine Altisen and Matthieu Moy},
title = {ac2lus: Bringing {SMT}-solving and Abstract Interpretation Techniques to Real-Time Calculus through the Synchronous Language {Lustre}},
booktitle = {22nd Euromicro Conference on Real-Time Systems (ECRTS)},
year = 2010,
address = {Brussels, Belgium},
month = {July},
abstract = { We present an approach to connect the Real-Time Calculus (RTC)
method to the synchronous data-flow language Lustre, and its
associated tool-chain, allowing the use of techniques like
SMT-solving and abstract interpretation which were not previously
available for use with RTC.
The approach is supported by a tool called ac2lus.
It allows to model the system to be analyzed as general Lustre
programs with inputs specified by arrival curves; the tool can
compute output arrival curves or evaluate upper and lower bounds on
any variable of the components, like buffer sizes.
Compared to existing approaches to connect RTC to other formalisms,
we believe that the use of Lustre, a real programming language, and
the synchronous hypothesis make the task easier
to write models, and we show that it allows a great flexibility of
the tool itself, with many variants to fine-tune the performances.
},
url = {http://www-verimag.imag.fr/~moy/publications/ac2lus-conf.pdf},
note = {Acceptance rate: 27/112 = 24\%, Rank A CORE 2014}
}
@inproceedings{pinavm-emsoft,
title = {{PinaVM}: a {SystemC} Front-End Based on an Executable Intermediate Representation},
author = {Marquet, Kevin and Moy, Matthieu},
abstract = {{SystemC} is the de facto standard for modeling
embedded systems. It allows system design at various
levels of ab- stractions, provides typical
object-orientation features and incorporates timing
and concurrency concepts. A {SystemC} program is
typically processed by a {SystemC} front-end in
order to verify, debug and/or optimize the
architecture. Designing a {SystemC} front-end is a
difficult task and existing approaches suffer from
limitations. In this paper, we present a new
approach that addresses most of these limitations.
We detail this approach, based on an executable
intermediate representation. We introduce
{PinaVM}, a new, open-source {SystemC} front-end
and implementation of our contributions. We give
experimental results on this tool.},
keywords = {{M}odeling, {V}alidation, {S}ystem{C}, {S}ystem on {C}hip},
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 = {International Conference on Embedded Software},
pages = {79 },
address = {{S}cottsdale, {USA}},
collaboration = {{O}pen{TLM} },
day = {24},
month = {10},
year = {2010},
hal_id = {hal-00495874},
url = {http://www-verimag.imag.fr/~moy/publications/pinavm-emsoft.pdf},
note = {Acceptance rate: 29/89 = 32\%, Rank A CORE 2014}
}
@inproceedings{review-sc-fe,
hal_id = {hal-00495886},
title = {A Theoretical and Experimental Review of {SystemC} Front-ends},
author = {Marquet, Kevin and Moy, Matthieu and Karkare, Bageshri},
booktitle = {Forum for Design Languages (FDL)},
abstract = {{SystemC} is a widely used tool for prototyping
{S}ystems-on-a-{C}hip. Being implemented as a
{C}++ library, a plain {C}++ compiler is sufficient
to compile and simulate a {SystemC} program.
However, a {SystemC} program needs to be
processed by a dedicated tool in order to visualize,
formally verify, debug and/or optimize the
architecture. In this paper we focus on the tools
(called front-ends) used in the initial stages of
processing {SystemC} programs. We describe the
challenges in developing {SystemC} front-ends and
present a survey of existing solutions. The
limitations and capabilities of these tools are
compared for various features of {SystemC} and
intended back-end applications. We present typical
examples that front-ends should ideally be able to
process, and give theoretical limitations as well as
experimental results of existing tools.},
keywords = {{SystemC}, front-end, compilation, review},
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} },
note = {{B}.1.4, {C}.3 {O}pen{TLM} ({P}rojet {M}inalogic) },
collaboration = {{O}pen{TLM} },
year = {2010},
pdf = {http://www-verimag.imag.fr/~moy/publications/revue-sc-fe-fdl.pdf}
}
@online{pinavm-software,
author = {Kevin Marquet and Matthieu Moy},
title = {{PinaVM}: {P}ina{VM} {I}s {N}ot {A} {V}irtual {M}achine},
howpublished = {Published as Free Software (LGPL License)},
year = 2010,
url = {https://forge.imag.fr/projects/pinavm/}
}
@techreport{VERIMAG-TR-2010-13,
title = {Faithfulness Considerations for Virtual Prototyping of Systems-on-Chip},
author = {Funchal, Giovanni and Moy, Matthieu and Maraninchi, Florence and Maillet-Contoz, Laurent},
institution = {VERIMAG},
url = {http://www-verimag.imag.fr/TR/TR-2010-13.pdf},
team = {SYNC},
year = {2010},
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.\r\n }
}
This file was generated by bibtex2html 1.98.