Publications of Matthieu Moy in 2010

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.

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.

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 [?]. Our framework can help to achieve tradeoffs between precision and analysis time.

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: Modeling, Validation, SystemC, System on Chip

SystemC is a widely used tool for prototyping Systems-on-a-Chip. 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

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ś 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.\n