Search

Multiprocessor mapping and scheduling is a long-old difficult problem. In this work we propose a new methodology to perform mapping and scheduling along with buffer memory optimization using an SMT solver. We target split-join graphs, a formalism inspired by synchronous data-flow (SDF) which provides a compact symbolic representation of data-parallelism. Unlike the traditional design flow for SDF which involves splitting of a big problem into smaller heuristic sub-problems, we deal with this problem as a whole and try to compute exact Pareto-optimal solutions for it. We introduce symmetry breaking constraints in order to reduce the run-times of the solver. We have tested our work on a number of SDF graphs and demonstrated the practicality of our method. We validate our models by running an image decoding application on the Tilera multicore platform.

Multi-Processor Systems-on-Chip (MPSoC) are going to be the leading hardware platform featured in embedded systems, if they aren't already. This article deals with the performance estimation problem on these systems. We present in this paper, a new approach of performance estimation of migration software task to hardware component for MPSoC systems with Synchronous Data Flow (SDF) Graphs. This approach is structured on four steps: 1) annotation Kahn Process Network (KPN) model, 2) transformation the annotated KPN model to SDF model, 3) synthesis under constraints and 4) comparison of results. We have using the SDF3 tool to determine performance estimation of migration software task to hardware component. Experiments on MJPEG decoder are made to illustrate the efficiency of our approach of performance estimation.

Coarse Grained Reconfigurable Array (CGRA) architectures give high throughput and data reuse for regular algorithms while providing flexibility to execute multiple algorithms on the same architecture. This paper investigates systolic mapping techniques for mapping biosignal processing algorithms to CGRA architectures. A novel methodology using synchronous data flow (SDF) graphs and control and data flow (CDF) graphs for mapping is presented. Mapping signal processing algorithms in this manner is shown to give up to a 88% reduction in memory accesses and significant savings in fetch and decode operations while providing high throughput.

We apply three different modeling frameworks -- timed automata ( Uppaal ), colored Petri nets and synchronous data flow -- to model a challenging industrial case study that involves an existing state-of-the-art image processing pipeline. Each of the resulting models is used to derive schedules for multiple concurrent jobs in the presence of limited resources (processing units, memory, USB bandwidth,..). The three models and corresponding analysis results are compared.

Techniques for the rapid deployment and architectural exploration of complex digital signal processing algorithms on embedded processor platforms are gaining popularity. These become significantly more complicated when dedicated hardware components need to be integrated. The models on which such design methodologies and tools are based highlight the system level inflexibility with both pre-designed intellectual property cores and most customized component creation techniques. This paper presents a technique for overcoming these deficiencies using a dataflow model of computation, by allowing flexible circuit architectures to be created that can be optimized as desired, providing increased throughput with no extra resource usage in some situations.

Engineers are faced nowadays with the challenge of designing strongly distributed control systems, with complex interactions. There is little theory and tool support to address this recent challenge. Control engineering and telecom engineering have dedicated but unrelated techniques, each for their specific domain. In this paper, we explore an approach where we combine two complementary formal methods, with good tool support and industrial acceptance:SCADE/Lustre from the Control Engineering domain, and SDL, from the Telecom domain.

In this talk we try to explain why synchronous data-flow languages have been successful in programming critical control systems. A tentative explanation is that these languages have their background in both computer and control sciences. This supports our opinion that such a common background would be useful for other related topics, for instance formal methods and distributed programming. Furthermore, we believe that computer based control of critical systems requires engineers trained in both sciences, and finding such engineers is difficult. A common cultural background, which the hybrid community tries to establish, may help in this issue.

International audience; We present a methodology for the verification of reactive systems, and its application to a case study. Systems are specified using the synchronous data flow language Signal. As this language is based on an equational approach (i.e. Signal programs are constraint equations between signals), it is natural to translate its Boolean part into a system of polynomial equations over three values denoting true, false and absent. Using operations in algebraic geometry on the polynomials, it is possible to check properties concerning the system, such as liveness, invariance, reachability and attractivity. We apply this method to the verification of the automatic circuit breaking control system of an electric power transformer station. This system handles the reaction to electrical defects on high voltage lines.

The paper addresses the issue of testing programs written in the synchronous data flow language LUSTRE. We define a mixed strategy which combines statistical testing and deterministic extremal values testing. Statistical testing involves exercising a program with random inputs, the input distribution and the number of test data being determined according to test criteria. Three criteria based on the finite state automaton produced by the LUSTRE compiler are studied, the feasibility of the method for designing test sets according to them being exemplified on a real-case study. Then, mutation analysis (here, specific to LUSTRE) is used to assess the efficiency of the test sets. The results allow us (i) to define the most cost-effective criterion for designing efficient statistical test sets of reasonable size, and (ii) to show the high fault revealing power of the corresponding mixed strategy, killing the whole set of 310 mutants involved in the experiments.