@inproceedings{lussy, author = {Matthieu Moy and Florence Maraninchi and Laurent Maillet-Contoz}, title = {{LusSy}: A Toolbox for the Analysis of Systems-on-a-Chip at the Transactional Level}, booktitle = {International Conference on Application of Concurrency to System Design}, year = 2005, month = {June}, url = {http://www-verimag.imag.fr/~moy/publications/acsd05.pdf}, pages = {26--35}, abstract = {We describe a toolbox for the analysis of Systems-on-a-chip described in {SystemC} at the transactional level. The tools are able to extract information from {SystemC} code, and to build a set of parallel automata that capture the semantics of a {SystemC} design, including the transaction-level specific constructs. As far as we know, this provides the first executable formal semantics of {SystemC}. Being implemented as a traditional compiler front-end, it is able to deal with general {SystemC} designs. The intermediate representation is now connected to existing formal verification tools via appropriate encodings. The toolbox is open and other tools will be used in the future.}, note = {Acceptance rate: 23/45 = 51\%} }
@inproceedings{pinapa, author = {Matthieu Moy and Florence Maraninchi and Laurent Maillet-Contoz}, title = {{Pinapa}: An Extraction Tool for {SystemC} descriptions of Systems-on-a-Chip}, booktitle = {EMSOFT}, year = 2005, month = {September}, url = {http://www-verimag.imag.fr/~moy/publications/sc-compil.pdf}, code = {http://greensocs.sourceforge.net/pinapa/}, pages = {317--324}, abstract = {{SystemC} is becoming a de-facto standard for the description of complex systems-on-a-chip. It enables system-level descriptions of SoCs: the same language is used for the description of the architecture, software and hardware parts. A tool like pinapa is compulsory to work on realistic SoCs designs for anything else than simulation: it is able to extract both architecture and behavior information from {SystemC} code, with very few limitations. pinapa can be used as a front-end for various analysis tools, ranging from ``superlint'' to model-checking. It is open source and available from http://greensocs.sourceforge.net/pinapa/. There exists no equivalent tool for {SystemC} up to now.}, note = {25/88 = 28\% accepted as regular papers, Rank A CORE 2014} }
@incollection{tlm-book-chap5, author = {Matthieu Moy}, title = {Chapter 5.9, Formal Verification}, booktitle = {Transaction-Level Modeling with {SystemC}. {TLM} Concepts and Applications for Embedded Systems}, pages = {190--206}, publisher = {Springer}, year = 2005, editor = {Frank Ghenassia}, url = {http://www.springer.com/engineering/electronics/book/978-0-387-26232-1} }
@article{lussy-journal, author = {Matthieu Moy and Florence Maraninchi and Laurent Maillet-Contoz}, title = {{LusSy}: an open Tool for the Analysis of Systems-on-a-Chip at the Transaction Level}, journal = {Design Automation for Embedded Systems}, year = 2006, note = {special issue on {SystemC}-based systems}, url = {http://www-verimag.imag.fr/~moy/publications/springer.pdf}, abstract = {We describe a toolbox for the analysis of Systems-on-a-chip written in {SystemC} at the transaction level. The tool is able to extract information from {SystemC} code, and to build a set of parallel automata that capture the semantics of a {SystemC} design, including the transaction-level specific constructs. As far as we know, this provides the first executable formal semantics of {SystemC}. Being implemented as a traditional compiler front-end, it is able to deal with general {SystemC} designs. The intermediate representation is now connected to existing formal verification tools via appropriate encodings. The toolbox is open and other tools will be used in the future.} }
@online{framogr-software, author = {Matthieu Moy and V. H. Gupta and K. Gopinath}, title = {{Framogr}: a {FRAMework} for the {MOdeling} and simulation of {GRoup} protocols}, howpublished = {Published as Free Software (LGPL License)}, year = 2006, note = {\url{http://download.gna.org/framogr/}} }
@phdthesis{these-moy, author = {Matthieu Moy}, title = {Techniques and Tools for the Verification of Systems-on-a-Chip at the Transaction Level}, school = {INPG, Grenoble, France}, year = 2005, url = {http://www-verimag.imag.fr/~moy/phd/}, month = {December}, abstract = { The work presented in this document deals with the formal verification models of Systems-on-a-Chip at the transaction level (TLM). We present the transaction level and its variants, and remind how this new level of abstraction is today necessary in addition to the register transfer level (RTL) to accommodate the growing constraints of productivity and quality, and how it integrates in the design flow. We present a new tool, called {LusSy}, that allows property-checking on transactional models written in {SystemC}. Its structure is similar to the one of a compiler: A front-end, {Pinapa}, that reads the source program, a semantic extractor, {Bise}, into our intermediate formalism {HPIOM}, a number of optimizations in the component {Birth}, and code generators for provers like {Lustre} and {SMV}. {LusSy} has been designed to have as few limitation as possible regarding the way the input program is written. {Pinapa} uses a novel approach to extract the information from the {SystemC} program, and the semantic extraction implements several TLM constructs that have not been implemented in any other {SystemC} verification tool as of now. It doesn't require any manual annotation. The tool chain is completely automated. {LusSy} is currently able to prove properties on small platforms. Its components are reusable to build compositional verification tools, or static code analyzers using techniques other than model-checking that can scale up more efficiently. We present the theoretical principles for each step of the transformation, as well as our implementation. The results are given for small examples, and for a medium size case-study called EASY. Experimenting with {LusSy} allowed us to compare the various tools we used as provers, and to evaluate the effects of the optimizations we implemented. } }
@inproceedings{systemc-to-spin, author = {Claus Traulsen and J\'er\^ome Cornet and Matthieu Moy and Florence Maraninchi}, title = {A {SystemC}/{TLM} semantics in {Promela} and its possible applications}, booktitle = {14th Workshop on Model Checking Software SPIN}, year = 2007, month = {July}, url = {http://www-verimag.imag.fr/~moy/publications/MicMacToSpin.pdf}, abstract = {{SystemC} has become a de-facto standard for the modeling of systems-on-a-chip, at various levels of abstraction, including the so-called transaction level (TL). Verifying properties of a TL model requires that {SystemC} be translated into some formally defined language for which there exist verification back-ends. Since {SystemC} has no formal semantics, this includes a careful encoding of the {SystemC} scheduler, which has both synchronous and asynchronous features, and a notion of time. In a previous work, we described LusSy a complete chain from {SystemC} to a synchronous formalism and its associated verification tools. In this paper, we describe the encoding of the {SystemC} scheduler into a asynchronous formalism, namely Promela (the input language for {Spin}). We comment on the possible uses of this new encoding, and compare it with the synchronous encoding.} }
@article{helmstet:fmcad06, author = {Claude Helmstetter and Florence Maraninchi and Laurent Maillet-Contoz and Matthieu Moy}, title = {Automatic Generation of Schedulings for Improving the Test Coverage of Systems-on-a-Chip}, journal = {{FMCAD}}, year = {2006}, isbn = {0-7695-2707-8}, pages = {171-178}, doi = {http://doi.ieeecomputersociety.org/10.1109/FMCAD.2006.10}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, url = {http://www-verimag.imag.fr/~moy/publications/Helmstetter_FMCAD06.pdf}, abstract = {{SystemC} is becoming a de-facto standard for the early simulation of Systems-on-a-chip (SoCs). It is a parallel language with a scheduler. Testing a SoC written in {SystemC} implies that we execute it, for some well chosen data. We are bound to use a particular deterministic implementation of the scheduler, whose specification is non-deterministic. Consequently, we may fail to discover bugs that would have appeared using another valid implementation of the scheduler. Current methods for testings SoCs concentrate on the generation of the inputs, and do not address this problem at all. We assume that the selection of relevant data is already done, and we generate several schedulings allowed by the scheduler specification. We use dynamic partial-order reduction techniques to avoid the generation of two schedulings that have the same effect on the system’s behavior. Exploring alternative schedulings during testing is a way of guaranteeing that the SoC description, and in particular the embedded software, is scheduler-independent, hence more robust. The technique extends to the exploration of other non-fully specified aspects of SoC descriptions, like timing.}, note = {Acceptance rate: 21/90 = 23\%} }
@inproceedings{MARANINCHI:2008:HAL-00311011:1, title = {{S}ystem{C}/{TLM} {S}emantics for {H}eterogeneous {S}ystem-on-{C}hip {V}alidation}, author = {Maraninchi, Florence and Moy, Matthieu and Cornet, J{\'e}r{\^o}me and Maillet-Contoz, Laurent and Helmstetter, Claude and Traulsen, Claus}, abstract = {{S}ystem{C} has become a de facto standard for the system-level description of systems-on-a-chip. {S}ystem{C}/{TLM} is a library dedicated to transaction level modeling. {I}t allows to define a virtual prototype of a hardware platform, on which the embedded software can be tested. {A}pplying formal validation techniques to {S}ystem{C} descriptions of {S}o{C}s requires that the semantics of the language be formalized. {T}he model of time and concurrency underlying the {S}ystem{C} definition is intermediate between pure synchrony and pure asynchrony. {W}e list the available solutions for the semantics of {S}ystem{C}/{TLM}, and explain how to connect {S}ystem{C} to existing formal validation tools.}, keywords = {{S}ystem{C}; {TLM}; lustre; spin; promela; semantics; model-checking; verification; model; {S}o{C}; {S}ystem-on-a-{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} - {STM}icroelectronics ({G}renoble) - {ST}-{GRENOBLE} - {STM}icroelectronics - {STM}icroelectronics ({C}rolles) - {ST}-{CROLLES} - {STM}icroelectronics - {L}aboratoire {F}ranco-{C}hinois d'{I}nformatique, d'{A}utomatique et de {M}ath{\'e}matiques {A}ppliqu{\'e}es - {LIAMA} - {I}nstitute of {A}utomation, {C}hinese {A}cademy of {S}ciences - {C}hinese {A}cademy of {S}cience - {INRA} - {INRIA} - {BRGM} - {CIRAD} - {CNRS} - {FORMES} - {LIAMA} - {INRIA} - {T}singhua {U}niversity / {B}eijing - {LIAMA} - {I}nformatic {K}iel {U}niversity - {C}hristian-{A}lbrechts-{U}niversit{\"a}t, {K}iel }, booktitle = {2008 {J}oint {IEEE}-{NEWCAS} and {TAISA} {C}onference 2008 {J}oint {IEEE}-{NEWCAS} and {TAISA} {C}onference }, address = {{M}ontr{\'e}al {C}anada }, editor = {{IEEE} }, note = {{B}.6.3, {D}.2.4, {D}.3.1, {F}.4.3, {F}.3.1, {B}.8.1 }, audience = {internationale }, month = {June}, year = {2008}, url = {http://hal.archives-ouvertes.fr/hal-00311011/en/} }
@inproceedings{besnard09:ssa-to-signal, author = {{B}esnard, {L}o{\"i}c and {G}autier, {T}hierry and {M}oy, Matthieu and {T}alpin, {J}ean-{P}ierre and {J}ohnson, {K}enneth and {M}araninchi, {F}lorence}, title = {{A}utomatic translation of {C}/{C}++ parallel code into synchronous formalism using an {SSA} intermediate form}, booktitle = {Ninth International Workshop on Automated Verification of Critical Systems (AVOCS'09)}, year = 2009, month = {September}, publisher = {Electronic Communications of the EASST}, url = {http://www-verimag.imag.fr/~moy/publications/ssa-sig.pdf}, abstract = {We present an approach for the translation of imperative code (like C, C++) into the synchronous formalism Signal, in order to use a model-checker to verify properties on the source code. The translation uses SSA as an intermediate formalism, and the GCC compiler as a front-end. The contributions of this paper with respect to previous work are a more efficient translation scheme, and the management of parallel code. It is applied successfully on simple {SystemC} examples.} }
@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} }
@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} }
@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/} }
@online{pinapa-software, author = {Matthieu Moy}, title = {{Pinapa}: {P}inapa {I}s {N}ot a {P}arser}, howpublished = {Published as Free Software (LGPL License)}, year = 2005, url = {http://greensocs.sourceforge.net/pinapa/} }
@online{sc-during-software, author = {Matthieu Moy}, title = {sc-during: tasks with duration for parallel programming in {SystemC}}, howpublished = {Published as Free Software (LGPL License)}, year = 2012, url = {https://forge.imag.fr/projects/sc-during/} }
@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 } }
@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{chamilotools-software, author = {Matthieu Moy and S\'ebastien Viardot}, title = {Chamilotools: a set of tools to interact with a Chamilo server}, howpublished = {Published as Free Software (CeciLL C License)}, year = 2016, url = {https://gitlab.com/chamilotools/chamilotools} }
@inproceedings{Henry_Monniaux_Moy_SAS2012, title = {Succinct Representations for Abstract Interpretation}, author = {Henry, Julien and Monniaux, David and Moy, Matthieu}, booktitle = {Static analysis Symposium (SAS)}, team = {SYNC}, year = {2012}, note = {Acceptance rate: 40\%, Rank A CORE 2014} }
@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/} }
@online{libtlmpwt-software, author = {Claude Helmstetter and Matthieu Moy}, title = {{LIBTLMPWT}: Model Power-Consumption and Temperature in SystemC/TLM}, howpublished = {Published as Free Software (GPL License)}, year = 2013, url = {http://www-verimag.imag.fr/~moy/?LIBTLMPWT-Model-Power-Consumption} }
@inproceedings{Henry_Monniaux_Moy_TAPAS2012, title = {{PAGAI}: a path sensitive static analyzer}, author = {Henry, Julien and Monniaux, David and Moy, Matthieu}, editor = {Bertrand Jeannet}, booktitle = {Tools for Automatic Program Analysis (TAPAS)}, team = {SYNC}, year = {2012}, abstract = {We describe the design and the implementation of PAGAI, a new static analyzer working over the LLVM compiler infrastructure, which computes inductive invariants on the numerical variables of the analyzed program. PAGAI implements various state-of-the-art algorithms combining abstract interpretation and decision procedures (SMT-solving), focusing on distinction of paths inside the control flow graph while avoiding systematic exponential enumerations. It is parametric in the abstract domain in use, the iteration algorithm, and the decision procedure. We compared the time and precision of various combinations of analysis algorithms and abstract domains, with extensive experiments both on personal benchmarks and widely available GNU programs.} }
@inproceedings{cornet:hal-00716051, title = {{Co-Simulation of a SystemC TLM Virtual Platform with a Power Simulator at the Architectural Level: Case of a Set-Top Box}}, author = {Cornet, J\'er\^ome and Maillet-Contoz, Laurent and Materic, Ilija and Kaiser, Sylvian and Boussetta, Hela and Bouhadiba, Tayeb and Moy, Matthieu and Maraninchi, Florence}, booktitle = {{Design Automation Conference}}, address = {San Francisco, US}, month = {June}, pages = {SESSION 10U: USER TRACK}, url = {http://hal.archives-ouvertes.fr/hal-00716051}, team = {SYNC}, year = {2012}, hal_id = {hal-00716051}, keywords = {power estimation; temperature; systemc; transaction-level modeling}, language = {Anglais}, affiliation = {STMicroelectronics (Grenoble) - ST-GRENOBLE , Docea Power , VERIMAG - VERIMAG - IMAG}, audience = {internationale}, abstract = {{The ability to perform power estimation early in the design flow is becoming more and more critical as power optimization requirements grow. For now, standalone power simulators allow such estimation, based on typical stimuli described in a use-case scenario. We propose a co-simulation of SystemC TLM platforms with a Power model. This way, the Power model benefits from more realistic stimuli. In addition, it is possible to provide real-time information from the Power model back to the SystemC TLM simulation, such as temperature values.}} }
@inproceedings{moy:hal-00761047, hal_id = {hal-00761047}, url = {http://hal.archives-ouvertes.fr/hal-00761047}, title = {{Parallel Programming with SystemC for Loosely Timed Models: A Non-Intrusive Approach}}, author = {Moy, Matthieu}, abstract = {{The SystemC/TLM technologies are widely accepted in the industry for fast system-level simulation. An important limitation of SystemC regarding performance is that the reference implementation is sequential, and the official semantics makes parallel executions difficult. As the number of cores in computers increase quickly, the ability to take advantage of the host parallelism during a simulation is becoming a major concern. Most existing work on parallelization of SystemC targets cycle-accurate simulation, and would be inefficient on loosely timed systems since they cannot run in parallel processes that do not execute simultaneously. We propose an approach that explicitly targets loosely timed systems, and offers the user a set of primitives to express tasks with duration, as opposed to the notion of time in SystemC which allows only instantaneous computations and time elapses without computation. Our tool exploits this notion of duration to run the simulation in parallel. It runs on top of any (unmodified) SystemC implementation, which lets legacy SystemC code continue running as-it-is. This allows the user to focus on the performance-critical parts of the program that need to be parallelized.}}, keywords = {SystemC; TLM; parallelism; multi-core; loosely-timed}, language = {Anglais}, affiliation = {VERIMAG - VERIMAG - IMAG}, booktitle = {{The Design, Automation, and Test in Europe (DATE)}}, address = {Grenoble, France}, audience = {internationale }, year = {2013}, month = mar, pdf = {http://www-verimag.imag.fr/~moy/IMG/pdf/sc-during.pdf}, note = {16.4\% accepted as long-paper, Rank A+ GDR SoC-SiP} }
@inproceedings{bmm-date-13, title = {System-Level Modeling of Energy in {TLM} for Early Validation of Power and Thermal Management}, author = {Bouhadiba, Tayeb and Moy, Matthieu and Maraninchi, Florence}, booktitle = {Design Automation and Test Europe (DATE)}, address = {Grenoble, France}, month = mar, team = {SYNC}, url = {http://hal.archives-ouvertes.fr/hal-00807048}, pdf = {http://www-verimag.imag.fr/~moy/publications/granu-date2013.pdf}, year = {2013}, note = {16.4\% accepted as long-paper, Rank A+ GDR SoC-SiP} }
@inproceedings{helmstetter:hal-00807046, title = {{Fast and Accurate TLM Simulations using Temporal Decoupling for FIFO-based Communications}}, author = {Helmstetter, Claude and Cornet, J\'er\^ome and Galil\'ee, Bruno and Moy, Matthieu and VIVET, Pascal}, booktitle = {{Design, Automation and Test in Europe (DATE)}}, address = {Grenoble, France}, month = {Mar}, pages = {1185}, url = {http://hal.archives-ouvertes.fr/hal-00807046}, team = {SYNC}, year = {2013}, hal_id = {hal-00807046}, language = {Anglais}, affiliation = {Laboratoire d'Electronique et des Technologies de l'Information - LETI , STMicroelectronics (Grenoble) - ST-GRENOBLE , VERIMAG - IMAG}, audience = {internationale}, pdf = {http://hal.archives-ouvertes.fr/hal-00807046/PDF/TDpaper.pdf}, abstract = {{Untimed models of large embedded systems, generally written using SystemC/TLM, allow the software team to start simulations before the RTL description is available, and then provide a golden reference model to the verification team. For those two purposes, only a correct functional behavior is required, but users are asking more and more for timing estimations early in the design flow. Because companies cannot afford to maintain two simulators for the same chip, only local modifications of the untimed model are considered. A known approach is to add timing annotations into the code and to reduce the number of costly context switches using temporal decoupling, meaning that a process can go ahead of the simulation time before synchronizing again. Our current goal is to apply temporal decoupling to the TLM platform of a many-core SoC dedicated to high performance computing. Part of this SoC communicates using classic memory-mapped buses, but it can be extended with hardware accelerators communicating using FIFOs. Whereas temporal decoupling for memory-based transactions has been widely studied, FIFO-based communications raise issues that have not been addressed before. In this paper, we provide an efficient solution to combine temporal decoupling and FIFO-based communications.}}, note = {acceptance rate: 302/829 = 36.4\% all categories, Rank A+ GDR SoC-SiP} }
@inproceedings{bouhadiba:hal-00807354, hal_id = {hal-00807354}, url = {http://hal.archives-ouvertes.fr/hal-00807354}, title = {{Co-Simulation of Functional SystemC TLM Models with Power/Thermal Solvers}}, author = {Bouhadiba, Tayeb and Moy, Matthieu and Maraninchi, Florence and Cornet, J{\'e}r{\^o}me and Maillet-Contoz, Laurent and Materic, Ilija}, abstract = {{Modern systems-on-chips need sophisticated power-management policies to control their power consumption and temperature. These power-management policies are usually implemented partly in software, with hardware support. They need to be validated early, hence power and temperature-aware simulation techniques at the system-level need to be developed. Existing approaches for system-level power and thermal analysis usually either completely abstract the functionality (allowing only simple scenarios to be simulated), or run the functional simulation independently from the non-functional one. The approach presented in this paper allows a coupled simulation of a SystemC/TLM model, possibly including the actual embedded software, with a power and temperature solver such as ATMI or the commercial tool ACEplorer. Power and temperature analysis is done based on the stimuli sent by the SystemC/TLM platform, which in turn can take decisions based on the non-functional simulation.}}, language = {Anglais}, affiliation = {VERIMAG - IMAG , STMicroelectronics (Grenoble), Docea Power}, booktitle = {{Virtual Prototyping of Parallel and Embedded Systems (VIPES)}}, address = {Boston, US}, audience = {internationale }, year = {2013}, month = may, pdf = {http://hal.archives-ouvertes.fr/hal-00807354/PDF/vipes2013.pdf} }
@article{moy:hal-00986536, hal_id = {hal-00986536}, url = {http://hal.archives-ouvertes.fr/hal-00986536}, title = {{Compte-rendu d'habilitation : Mod{\'e}lisation {\`a} haut niveau d'abstraction pour les syst{\`e}mes embarqu{\'e}s}}, author = {Moy, Matthieu}, abstract = {{Les syst{\`e}mes embarqu{\'e}s modernes ont atteint un niveau de complexit{\'e} qui fait qu'il n'est plus possible d'attendre les premiers prototypes physiques pour valider les d{\'e}cisions sur l'int{\'e}gration des composants mat{\'e}riels et logiciels. Il est donc n{\'e}cessaire d'utiliser des mod{\`e}les, t{\^o}t dans le flot de conception. Les travaux pr{\'e}sent{\'e}s dans ce document contribuent {\`a} l'{\'e}tat de l'art dans plusieurs domaines. Nous pr{\'e}sentons dans un premier temps de nouvelles techniques de v{\'e}rification de programmes {\'e}crits dans des langages g{\'e}n{\'e}ralistes comme C, C++ ou Java. Dans un second temps, nous utilisons des outils de v{\'e}rification formelle sur des mod{\`e}les {\'e}crits en SystemC au niveau transaction (TLM). Plusieurs approches sont pr{\'e}sent{\'e}es, la plupart d'entre elles utilisent des techniques de compilations sp{\'e}cifiques {\`a} SystemC pour transformer le programme SystemC en un format utilisable par les outils. La seconde partie du document s'int{\'e}resse aux propri{\'e}t{\'e}s non-fonctionnelles des mod{\`e}les : performances temporelles, consommation {\'e}lectrique et temp{\'e}rature. Dans le contexte de la mod{\'e}lisation TLM, nous proposons plusieurs techniques pour enrichir des mod{\`e}les fonctionnels avec des informations non-fonctionnelles. Enfin, nous pr{\'e}sentons les contributions faites {\`a} l'analyse de performance modulaire (MPA) avec le calcul temps-r{\'e}el (RTC). Nous proposons plusieurs connections entre ces mod{\`e}les analytiques et des formalismes plus expressifs comme les automates temporis{\'e}s et le langage de programmation Lustre. Ces connexion posent le probl{\`e}me th{\'e}orique de la causalit{\'e}, qui est formellement d{\'e}fini et r{\'e}solu avec un algorithme nouveau dit de " fermeture causale ".}}, language = {French}, affiliation = {VERIMAG - IMAG}, pages = {285-293}, journal = {Technique et Science Informatiques}, volume = {33}, number = {3}, year = {2014}, pdf = {http://hal.archives-ouvertes.fr/hal-00986536/PDF/hdr-matthieu-moy-fr.pdf} }
@phdthesis{hdr-moy, title = { High-level Models for Embedded Systems }, author = {Moy, Matthieu}, year = {2014}, month = {March}, address = {Verimag}, type = {Habilitation \`a Diriger des Recherches ({HDR})}, school = {{Univ. Grenoble Alpes, F-38000 Grenoble, France}}, team = {SYNC}, url = {http://www-verimag.imag.fr/~moy/?Habilitation-a-Diriger-des}, pdf = {http://www-verimag.imag.fr/~moy/IMG/pdf/hdr-matthieu-moy.pdf} }
@inproceedings{rihani:hal-01243244, title = {{WCET analysis in shared resources real-time systems with TDMA buses}}, author = {Rihani, Hamza and Moy, Matthieu and Maiza, Claire and Altmeyer, Sebastian}, url = {https://hal.archives-ouvertes.fr/hal-01243244}, booktitle = {{RTNS 2015}}, address = {Lille, France}, series = {23rd International Conference on Real-Time Networks and Systems}, year = {2015}, month = nov, doi = {10.1145/2834848.2834871}, keywords = {wcet ; tdma ; worst-case execution time ; bus ; multi-core ; smt}, pdf = {http://www-verimag.imag.fr/~moy/publications/rtns-2015.pdf}, hal_id = {hal-01243244}, hal_version = {v1}, team = {SYNC} }
@inproceedings{challenges-2015-rsp, title = {{Challenges for the Parallelization of Loosely Timed SystemC Programs}}, author = {Becker, Denis and Moy, Matthieu and Cornet, J\'er\^ome}, booktitle = {IEEE International Symposium on Rapid System Prototyping (RSP)}, url = {https://hal.archives-ouvertes.fr/hal-01214891}, pdf = {http://www-verimag.imag.fr/~moy/publications/rsp-2015.pdf}, team = {SYNC}, year = {2015} }
@inproceedings{sycview-2016-duhde, title = {{SycView: Visualize and Profile SystemC Simulations}}, author = {Becker, Denis and Cornet, J\'er\^ome and Moy, Matthieu}, booktitle = {{DUHDe}}, address = {Dresden, Germany}, month = {Mar}, series = {3rd Workshop on Design Automation for Understanding Hardware Designs}, url = {https://hal.archives-ouvertes.fr/hal-01243265}, pdf = {http://www-verimag.imag.fr/~moy/publications/duhde2016.pdf}, team = {SYNC}, year = {2016}, hal_id = {hal-01243265}, hal_version = {v1} }
@article{moy:hal-01339441, title = {{Modeling Power Consumption and Temperature in TLM Models}}, author = {Moy, Matthieu and Helmstetter, Claude and Bouhadiba, Tayeb and Maraninchi, Florence}, url = {https://hal.archives-ouvertes.fr/hal-01339441}, journal = {{Leibniz Transactions on Embedded Systems}}, publisher = {{European Design and Automation Association (EDAA) \ EMbedded Systems Special Interest Group (EMSIG) and Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik GmbH, Dagstuhl Publishing.}}, volume = {Vol 3}, number = {No 1}, pages = {03:1-03:29}, year = {2016}, month = jun, doi = {10.4230/LITES-v003-i001-a003}, keywords = {Systemc ; Tlm ; Energy ; atmi}, pdf = {http://www-verimag.imag.fr/~moy/publications/63-285-3-PB.pdf}, hal_id = {hal-01339441}, hal_version = {v1} }
@inproceedings{RMM16, title = {{Efficient Execution of Dependent Tasks on Many-Core Processors}}, author = {Rihani, Hamza and Maiza, Claire and Moy, Matthieu}, booktitle = {{RTSOPS 2016}}, address = {Toulouse, France}, month = {Jul}, series = {7th International Real-Time Scheduling Open Problems Seminar}, team = {SYNC}, year = {2016}, keywords = {WCRT Analysis; Shared Resource Interference; Dependent Tasks; Synchronous Data flow; Many-cores; Scheduling}, pdf = {http://www-verimag.imag.fr/~moy/publications/rtsops2016.pdf}, url = {https://hal.archives-ouvertes.fr/view/index/docid/1406057} }
@inproceedings{RMMDA16, title = {{Response Time Analysis of Synchronous Data Flow Programs on a Many-Core Processor}}, author = {Rihani, Hamza and Moy, Matthieu and Maiza, Claire and Davis, Robert I. and Altmeyer, Sebastian}, booktitle = {{RTNS 2016}}, address = {Brest, France}, month = {Oct}, series = {24th International Conference on Real-Time Networks and Systems}, team = {SYNC}, year = {2016}, doi = {10.1145/2997465.2997472}, keywords = {WCRT Analysis; Shared Resource Interference; Dependent Tasks; Synchronous Data flow; Many-cores; Scheduling}, url = {https://hal.archives-ouvertes.fr/view/index/docid/1406145}, pdf = {http://www-verimag.imag.fr/~moy/publications/rtns16-conf.pdf} }
@article{rtc-fmsd16, title = {Causality Problem in Real-Time Calculus}, author = {Altisen, Karine and Moy, Matthieu}, journal = {Formal Methods in System Design (Springer)}, number = {1}, pages = {1--45}, url = {https://hal.archives-ouvertes.fr/view/index/docid/1406162}, volume = {48}, team = {SYNC}, year = {2016}, doi = {10.1007/s10703-016-0250-y}, issn = {1572-8102}, pdf = {http://www-verimag.imag.fr/~moy/publications/causality-springer.pdf}, note = {Rank A CORE ERA2010} }
@article{parallel-syc-2016-electronics, title = {{Parallel Simulation of Loosely Timed SystemC/TLM Programs: Challenges Raised by an Industrial Case Study}}, author = {Becker, Denis and Moy, Matthieu and Cornet, J\'er\^ome}, editor = {Fr\'ed\'eric Rousseau and Gabriela Nicolescu and Amer Baghdadi and Mostafa Bassiouni}, journal = {MDPI Electronics}, number = {2}, pages = {22}, url = {https://hal.archives-ouvertes.fr/hal-01321055}, volume = {5}, team = {SYNC}, year = {2016}, doi = {10.3390/electronics5020022}, pdf = {http://www-verimag.imag.fr/~moy/publications/electronics-05-00022.pdf}, issn = {2079-9292} }
This file was generated by bibtex2html 1.98.