Sami Lazreg
email: slazreg@visteon.com

Philippe Collet
email: collet@i3s.unice.fr

Sébastien Mosser
email: mosser@i3s.unice.fr

Functional Feasibility Analysis of Variability-Intensive Data Flow-Oriented Applications over Highly-Configurable Platforms

Keywords: Validation, •Computer systems organization → Embedded systems, •Software and its engineering → Software product lines, •Theory Embedded system design engineering, variability modeling, feature model, behavioral product lines model checking

Data-flow oriented embedded systems, such as automotive systems used to render HMI (e.g., instrument clusters, infotainments), are increasingly built from highly variable specifications while targeting different constrained hardware platforms configurable in a fine-grained way. These variabilities at two different levels lead to a huge number of possible embedded system solutions, which functional feasibility is extremely complex and tedious to predetermine. In this paper, we propose a tooled approach that capture high level specifications as variable dataflows, and targeted platforms as variable component models. Dataflows can then be mapped onto platforms to express a specification of such variabilityintensive systems. The proposed solution transforms this specification into structural and behavioral variability models and reuses automated reasoning techniques to explore and assess the functional feasibility of all variants in a single run. We also report on the validation of the proposed approach. A qualitative evaluation has been conducted on an industrial case study of automotive instrument cluster, while a quantitative one is reported on large generated datasets.

CCS Concepts

•General and reference → Design

INTRODUCTION

Validating embedded systems design at early stages of development is of fundamental importance in industry. Ideally embedded system design should be modeled from high-level specifications, and then assess against possible implementations. Data-flow oriented embedded systems, such as automotive systems used to render HMI (e.g., instrument clusters, infotainments) are typically built from highly variable specifications. They are composed of a data-flow driving and feeding graphical processors to provide efficient and high-quality graphic rendering at a lower cost, while targeted hardware platforms are composed of heterogeneous and constrained hardware components. The variability is then twofold, with multiple graphic data-flow variants that can meet functional requirements, and diverse targeted hardware platform, which are highly configurable in a fine-grained way. These dimensions of variability dreadfully increase the size of the design space of these embedded systems (i.e., the number of possible embedded system implementation designs), making the feasibility assessment of these systems extremely tedious and complex.

Generally, design spaces of variable systems and protocols are assessed through variability-aware model checking on variable transition-based systems [START_REF] Asirelli | Formal description of variability in product families[END_REF][START_REF] Classen | Model checking lots of systems: efficient verification of temporal properties in software product lines[END_REF]. However these approaches are not capable of automatically map the variable data-flow specifications on configurable platform descriptions to apply their model-checking techniques. Consequently, this would imply to manually infer, model and assess embedded system design spaces from high level specifications, making this activity extremely tedious, time consuming, and error-prone.

Facing this issue, we determine three challenges to be tackled: (i) capturing and modeling from high-level specifications, structure, behavior and variability of these embedded systems (e.g., data-flow and platform alternatives, data sizes, memory capacities, graphic pipelines), (ii) inferring automatically all possible embedded system design implementations from specification models and, (iii) exploring and assessing the feasibility of all system implementations w.r.t. the predefined structural, behavioral and variability constraints. Current approaches [START_REF] Singh | Mapping on multi/many-core systems: survey of current and emerging trends[END_REF][START_REF] Gries | Methods for evaluating and covering the design space during early design development[END_REF][START_REF] Kienhuis | An approach for quantitative analysis of application-specific dataflow architectures[END_REF] assess functional feasibility of constrained data-flow-oriented embedded systems, but do not capture nor manage variability at both levels. Some Ad hoc techniques are trying to handle either platform variability (as reconfigurable architectures [START_REF] Sima | Runtime decision of hardware or software execution on a heterogeneous reconfigurable platform[END_REF][START_REF] Sigdel | System-level runtime mapping exploration of reconfigurable architectures[END_REF] [START_REF] Palermo | Variability-aware robust design space exploration of chip multiprocessor architectures[END_REF]) or functional variability (as multiple scenarios [START_REF] Schor | Scenario-based design flow for mapping streaming applications onto on-chip many-core systems[END_REF][START_REF] Van Stralen | Scenario-based design space exploration of mpsocs[END_REF] or multi-modes systems [START_REF] Wildermann | Operational mode exploration for reconfigurable systems with multiple applications[END_REF][START_REF] Palermo | Robust optimization of soc architectures: A multi-scenario approach[END_REF]). On the other hand, approaches tackling both kinds of variability [START_REF] Graf | Multi-variant-based design space exploration for automotive embedded systems[END_REF] are focusing on optimal platform selections to implement multiple functional variants at a lower cost, but they do not manage structural and behavioral properties (e.g. data sizes, memory capacities, graphic pipelines).

In this paper we propose an approach that extends these researches by supporting a complete modeling and assessment of structural, behavioral and variability properties of the targeted embedded systems by combining embedded system design engineering [START_REF] Singh | Mapping on multi/many-core systems: survey of current and emerging trends[END_REF][START_REF] Gries | Methods for evaluating and covering the design space during early design development[END_REF][START_REF] Kienhuis | An approach for quantitative analysis of application-specific dataflow architectures[END_REF] and Product line engineering techniques [START_REF] Asirelli | Formal description of variability in product families[END_REF][START_REF] Classen | Model checking lots of systems: efficient verification of temporal properties in software product lines[END_REF]. The proposed solution is model driven and i) captures high level variable data-flow and platform specifications following principles of separation of concern, ii) maps variable data-flow requirements into a description of the targeted variable hardware platform, so to infer the embedded system design space (i.e. all system implementations), iii) transforms the design space into a behavioral product line to reuse automated reasoning techniques (i.e. SAT solving, variability-aware model checking) to explore and assess the functional feasibility of all system design implementations in a single run. The framework also allows to remove invalid designs from the design space by constraining it.

This paper is an extended version from a paper published in the Variability and Software Product Line Engineering track of the SAC 2018 conference. In this extension, we detail a complete evaluation of the proposed approach with:

• complete implementation details with end-to-end sample materials,

• a qualitative evaluation on a real industrial use case in automotive systems, i.e., an instrument cluster product line,

• a quantitative evaluation on the scalability of the approach, using large generated datasets on both application and platform sides,

• a discussion on the threats to validity.

The remainder of the paper is organized as follows. Section 2 introduces the context and motivations illustrated by a running example. Section 3 presents the proposed framework, detailing each model and step. Section 4 details the qualitative and quantitative validation, and discusses threats to validity, while Section 5 concludes the paper.

MOTIVATIONS

Requirement gathering and validation of this research work have been realized in the context of an industrial collaboration with Visteon Electronics, a world class leader in automotive systems (e.g. instruments clusters, infotainment, connected vehicles). In the following we introduce one of the company case studies, extract a running example, determine requirements from them and discuss related work.

Case study

The case study is focusing on functional validation of some instrument clusters. By applying various data-flow image processing effects, such as blending, warping and scaling, an instrument cluster system improves driver experience with useful and high quality 2D/3D Human-Machine Interface (HMI). The embedded hardware platforms used to develop these systems are more and more highly configurable, but constrained in terms of architecture and capacities. Furthermore, multiple graphic data-flows variants can meet the client HMI requirements, but they also depend on the platform architectures and capacities. We consider this case study as representative of variability-intensive data-flow oriented systems. Different forms of variability, from high-level data-flows to low-level platforms lead to a huge number of possible system solutions, which feasibility is extremely complex and tedious to predetermine early in the development process.

Running Example

We now introduce a running example of a simplified instrument cluster. The data-flow on Fig. 1 represents different image flow processing that meet the HMI functional requirements. Images are processed by graphical tasks: image d2 has two different possible resolutions (e.g. 800x480, 480x320) and will be processed by task C. Image d1 can be either processed by task A or task B.

Figure 1: Functional specification

On the hardware side (cf. Fig. 2), the platform provides image processing capabilities through non programmable pipeline processors of DCU (Display Controller Unit) or GPU (Graphic Processing Unit) type, as well as data storage functionalities through RAM (Random Access Memory) and ROM (Read Only Memory). RAM and GPU are optional in the actual hardware products, so a system implementation may contain or not these components. Among variabilities in platforms, one can write data into and/or read data from RAM memory while only reading data is possible from ROM. Moreover, memory storage have limited and possibly variable (e.g. RAM) capacity. Contrary to a DCU, which renders directly processed images into display, a GPU needs to store its processing result into RAM. Graphical hardware processors are often designed as a multi-step pipeline, composed of several hardware implemented processing steps, and processor internal fifo memory buffers transferring data from one step to another. In our example, while a GPU can apply A followed by B processing on images in a single pass, a DCU can apply A, then followed by C.

Images and processing could be, respectively, stored and pro- cessed by multiple components, while images can be stored on RAM or on ROM: task A could be processed by both GPU and DCU, but a data-flow variant containing B task can only be implemented on a system containing a GPU. Finally, data mapping on memory are constrained in terms of storage capacity.

Consequently, to be valid, a system implementation has to fulfill (i) structural constraints such as not violating maximum memory capacities, (ii) behavioral constraints such as using correctly processor pipelines and memories, and (iii) variability constraints such as component dependency and exclusion. In our example, the application data-flow has 4 variants while the Platform exposes 3 architecture variants.

Even with this simplified case, this leads to 178 possible implementations, in which 58 satisfy constraints and could be developed by engineers. 1

Related Work

In the context of our work, engineers must be assisted to assess the functional feasibility of the different potential embedded system solutions, with means to capture both the high-level functional requirements and the specifications of targeted variable platforms. Ideally, a solution should be able to capture structural, behavioral and variability properties of both functional and platform specifications at a finegrained level, so to use these input models to automatically infer all possible embedded system implementation designs and assess the resulting consistent design space.

In the product line engineering, lots of approaches [START_REF] Asirelli | Formal description of variability in product families[END_REF][START_REF] Classen | Model checking lots of systems: efficient verification of temporal properties in software product lines[END_REF] are capable to model variable transition-based systems such as safety-critical systems or protocols, and to validate, through variability-aware model-checking, temporal properties and behavioral aspects. However, given high-level data-flows and platform specifications, these approaches are not capable of automatically map data-flows on platforms in order to infer and assess the resulting design space. Assessing the different mapping manually is not feasible in practice, as the activity would be tedious and error-prone.

In embedded system design engineering, most of the approaches capture high-level application and platform specifications, and map an application on hardware platforms in order to find, by design space exploration, an optimized system implementation for a single functional specification on a single platform [START_REF] Singh | Mapping on multi/many-core systems: survey of current and emerging trends[END_REF][START_REF] Gries | Methods for evaluating and covering the design space during early design development[END_REF]. Consequently, they do not capture nor manage variability at the application level and hardware platform variability is limited to component capacities (e.g. memory and bus size, processor frequency). Some other approaches try to handle some limited variability in functional specifications (e.g. optional task, alternative tasks, variable data) (as multiple scenarios [START_REF] Schor | Scenario-based design flow for mapping streaming applications onto on-chip many-core systems[END_REF][START_REF] Van Stralen | Scenario-based design space exploration of mpsocs[END_REF] or multi-modes systems [START_REF] Wildermann | Operational mode exploration for reconfigurable systems with multiple applications[END_REF][START_REF] Palermo | Robust optimization of soc architectures: A multi-scenario approach[END_REF]), but they do not manage platform variability. Some others try to handle some limited variability in platforms (e.g. optional resource, resource dependency, memories sizes) with reconfigurable architectures [21, 20] [18]. To the best of our knowledge, none of these approaches handle variability in both application and platform sides so to assess the feasibility of our class of problem.

Interestingly, the recent approach of Graf et. al. [START_REF] Graf | Ivam: Implicit variant modeling and management for automotive embedded systems[END_REF][START_REF] Graf | Robust design of e/e architecture component platforms[END_REF] manages some variability in both platform and functional specifications. On the platform variability side, resource components can be selected or not, while optional and mutually exclusive task groups are managed on the functional part. However, the approach is handling a coarse-grain form of requirements and cannot capture some of our specifications (e.g.data and memory sizes, as well as platform aspects such as processor pipelines or fifo buffers). Additionally, only structural validation of the system implementations is supported. Behavioral properties (e.g. data sizes, memory capacities, graphic pipelines) and behavioral constraints (e.g., absence of deadlock, reachability, liveness, safety etc.), which are fundamental in our case, cannot be checked.

PROPOSED FRAMEWORK

Overview

The proposed approach follows a model driven decomposition, based on the well-known robust Y-Chart pattern [START_REF] Balarin | Hardware-software co-design of embedded systems: the POLIS approach[END_REF][START_REF] Kienhuis | An approach for quantitative analysis of application-specific dataflow architectures[END_REF], which separates application and platform into different concerns. This allows modular specification and reasoning about the different parts of the specified embedded systems. Given high-level variable dataflow and platform inputs that notably captures the variability of functional and platform specifications, the framework will i) map all implementation of each data-flow variants on each platform configuration, ii) generate a Featured Transition System (FTS) [START_REF] Classen | Model checking lots of systems: efficient verification of temporal properties in software product lines[END_REF] from the system design space model, i.e. representing system implementations (cf. Fig. 3). This model consists in an extended form of automaton product line, which is then iii) checked in one run by a variability-aware model checker.

As shown on Fig. 3, our framework consists of three main models and two processes. We give here an overview while the following sections will detail and illustrate these elements.

Variable applications: a functional expert is in charge of capturing the functional requirements (cf. fig. 1) of the em- This model contains the classic structure and behavior of the data-flow (data, task, data-path, etc.), but also captures the variability in both structural properties (e.g., data size) and behavioral properties (e.g., alternative flows).

Variable platforms: on this side, a platform expert is in charge of expressing the platform specification (cf. fig. 2) as a templated component based system (cf. sec. 3.3). This model contains a set of components connected with each others. Similarly to the application one, the platform model also captures the variability of the defined components.

Variability-aware mapping process: the mapping algorithm (cf. sec. 3.4) consumes the application and platform input models previously defined and generates the Variability-Intensive Design Space, i.e. representing system implementations. It is made of two steps: (i) it finds for each task data and data-path (cf. fig. 1) all the possible mappings on appropriate platform processors and storage (cf. fig. 2); basically this is done by matching the task names with the names of the hardware functions of processors; data-paths are mapped on reachable memory of appropriate processor hardware functions; (ii) as the design space contains all mapping possibilities, the algorithm prunes unfeasible mappings w.r.t. structural and variability constraints.

Design space as a behavioral product line: from the system design space model, a Behavioral Product Line representing all system implementations is generated (cf. sec. 3.5). This product line is represented as a featured automaton, so that we can reuse and adapt techniques that rely on variabilityaware model-checking to validate the inferred systems. The basic idea is to transform a variable data-flow, a variable platform, and mappings to a data-flow automaton using, through a mapping automaton, a platform automaton to execute it. Valid executions of the application automaton should then respect generated properties representing end state reachability to ensure that the execution is correctly scheduled and executed onto the platform automaton.

Validation process: the validation process reuses automated reasoning techniques to assess structural and behavioral functional feasibility of the system variants represented by the behavioral product line (cf. sec. 3.6). The model checking is going to determine classic properties, such as safety, absence of deadlock, and our state reachability generated property, on all variants in one run. As a result, the validation solves and extracts valid variants respecting all structural, behavioral and variability constraints.

Applications as Variable Data-Flows

In our approach, a functional expert captures structure, behavior (data, task, data-path, etc.) and variability aspects (data size, alternative flows, etc.) of the functional requirements of the embedded system through an extended dataflow model. The extensions concern variability and data aspects of functional requirements, and in the following, we propose a formal data-flow model to do so.

Definition 1. A variable data-flow graph is a tuple V DG = (T, D, P ath, E, ζ) where:

• T is a set of tasks,
• D is a set of source data, and, ζ : D → {s0, ..., si ∈ N * } returns a set of alternative sizes of data,

|ζ(d ∈ D)| = > 1, if d has a variable size 1, if d has not a variable size
• P ath is a set of data-paths by which producer and consumer (i.e. tasks and data) are connected.

• E ⊆ (T ∪D)×P ath×T is the set of edges representing flows processing between producers and consumers.

The set of connected, input data-paths to a task I(t), output data-paths from a task or data O(v) are denoted by:

I(t) : {p ∈ P ath|(x, p, t) ∈ E}, O(v ∈ T ∪ D) : {p ∈ P ath|(v, p, x) ∈ E}.
Similarly I(p), input tasks to a output data-paths, and O(p), output tasks from a input data-paths, are denoted by:

I(p) : {prod ∈ T ∪ D|(prod, p, x) ∈ E}, O(p) : {t ∈ T |(x, p, t) ∈ E}.
Then:

|I(p)| + |O(p)| = > 2, if p has alternative flows 2, if p

has not flow variability

A variable data-flow represents multiple data-flow variants.

To implicitly represent all these variants in a single model, we follow the same approach as in variable workflows from [START_REF] Graf | Ivam: Implicit variant modeling and management for automotive embedded systems[END_REF], allowing data-paths to have multiple input and output tasks connected.

A data-path can be connected to multiple alternative, input tasks if |I(p)| > 1, and output tasks if with,

|O(p)| > 1. But, If |I(p)| = 1 ∧ |O(p)| = 1,
ζ(d1) = 512, ζ(d2) = {512, 1024}, I(p1) = d1, I(p2) = {a, b}, I(p3) = d2, O(p1) = {a, b}, O(p2) = c, O(p3) = c, I(a) = I(b) = p1, I(c) = {p2, p3}, O(a) = O(b) = p2, O(c) = ∅, O(d1) = p1, O(d2) = p3.

Platforms as Variable Resource Graphs

A variable platform specification is represented by a templated component based system (multi-pass processors, streaming processor, read-only memory, read-write memory, write-only memory, first-in-first-out buffers etc) where platform can have optional resource components and variability constraints on resources (dependency, incompatibility, etc.).

To capture variability aspects of a platform specification, we propose a formal architecture model defined as follows.

Definition 2. A variable resource graph is a tuple V RG = (P roc, S, Cs, ξ, θ, φrequires, φ excludes ) where: • Cs ⊆ (S × P roc) ∪ (P roc × S) is the set of connections between memory storage and processors,

• P roc = (F, B, C b ⊆ (F × B) × (B × F )) is a processor composed of a set F of
• R ⊆ P roc ∪ S is the set of resource components (i.e. processors and memory storage),

• θ : R → B return true if a component (i.e. processor or memory storage) is optional,

• φrequires : R → R captures dependency between resource components, similarly φ excludes : R → R captures incompatibility.

The set of, input memories to a processor function I(f ), output memories from a processor function O(f ) are denoted by:

∃p = (F, B, C b ) ∈ P roc, I(f ∈ F ) : {m ∈ S ∪ B|(m, p) ∈ Cs ∨ (m, f ) ∈ C b }, O(f ∈ F ) : {m ∈ S ∪ B|(p, m) ∈ Cs ∨ (f, m) ∈ C b }.
As a variable platform represents multiple platform configurations, we also capture implicitly all these configurations by introducing several functions, θ manages the optionality of a resource component. If θ(r) = ⊥ the resource is mandatory, otherwise the resource is optional, φrequires and φ excludes manages constrained relations of dependency and incompatibility between resource components. φrequires(r) = r0 means that if r is implemented then r0 must be implemented too. r depends on r0. On the contrary φ excludes (r) = r0 means that r and r0 cannot be implemented on the same platform variant. r and r0 are alternatives.

As memory storage can have alternative capacities, we introduce the function ξ which returns the set of alternative capacities C = ξ(s), each memory storage has at least one size and if |ξ(s)| > 1 the capacity of s is variable.

If the platform has no component variability ∀r ∈ R, θ(r) = ⊥ and no variable memory storage, ∀s ∈ S, |ξ(s)| = 1, the platform is not variable.

The platform specification of the running example V Gre is then formalized as

(P rocre = {DCU, GP U }, Sre = {RAM, ROM }, Cs re = {(RAM, DCU ), (ROM, DCU ), (RAM, GP U ), (ROM, GP U ), (GP U, RAM )})
where,

DCU = (F dcu = {a dcu , c dcu }, B dcu = r0 dcu , C b dcu = {(a dcu , r0 dcu ), (r0 dcu , c dcu )}), GP U = (Fgpu = {agpu, bgpu}, Bgpu = r0gpu, C bgpu {(agpu, r0gpu), (r0gpu, bgpu)}), with, ξ(ROM ) = 4096, ξ(RAM ) = {1024, 2048}, θ(GP U ) = θ(RAM ) = , θ(DCU ) = θ(ROM ) = ⊥ φrequires(GP U ) = RAM, φrequires(RAM ) = ∅, I(agpu) = {ROM, RAM }, O(agpu) = {r0gpu, RAM }, I(c dcu ) = {r0 dcu , ROM, RAM }, O(c dcu ) = ∅.

Variability-Aware Mapping Process

The mapping algorithm takes as inputs the variable dataflow and configurable platform models in order to find all embedded system implementations. We propose a mapping model to not only capture all implementations of a single data-flow into a single platform but to capture all data-flow variants implementations onto all platform configurations. Our variability-aware mapping model can be seen as a product line of traditional mapping models.

Definition 3. A variability-aware data-flow-oriented mapping V M = (T m, Dm, Em) where:

• T m ⊆ T × F is the set of possible mappings of tasks on processors ∀(t, f ) ∈ T m, t can be mapped on processor function f because f can implement t,

• Dm ⊆ D ×S is the set of mappings of data on memory storage,

• Em ⊆ E × (S ∪ B)
is the set of data-paths mapping on memory by which data are consumed/produced.

Definition 4. The Variability-Aware Mapping function M = V DG × V RG → V M sorts topologically the data-flow and finds appropriate mapping for each data, task and datapaths of the data-flow using resources of the resource graph.

Basically, each valid mapping should respect consistency constraints such as that (1) All tasks are mapped to, a least, one processor function:

∀t ∈ T, ∃(t, f ) ∈ T m, (2)
All data are mapped to, at least, one memory storage:

∀d ∈ D, ∃(d, s) ∈ Dm, (3)
All data-paths are mapped to, at least, one appropriate mapping. For data-path starting by an input datum, the storage on which the datum is mapped has to be reachable by the processor function on which the task consuming the datum is mapped.

∀e = (d ∈ D, p, t) ∈ E, ∃(e, s ∈ S) ∈ Em, ∃(d, s) ∈ Dm, ∃(t, f ) ∈ T m, s ∈ I(f ),
For data-path between tasks, the memory on which the output of the first task is mapped has to be reachable by the processor function on which the second task is mapped.

∀e = (t ∈ T, p, t ) ∈ E, ∃(e, m) ∈ Em, ∃(t, f ) ∈ T m, ∃(t , f ) ∈ T m, m ∈ O(f ) ∧ m ∈ I(f )
The mapping model of the running example V Mre is then formalized as (T mre = {(a, a dcu ), (a, agpu), (b, bgpu), (c, c dcu )}, Dmre = {(d1, RAM ), (d1, ROM ), (d2, RAM ), (d2, ROM )}, Emre = {((d1, p1, a), RAM ), ((d1, p1, a), ROM ), ((d1, p1, b), RAM ), ((d1, p1, b), ROM ), ((a, p2, c), r0 dcu ), ((a, p2, c), RAM ), ((b, p2, c), RAM ), ((d2, p3, c), RAM ), ((d2, p3, c), ROM ))}) Finally, The design space representing all system implementations, called variability-intensive embedded system design space is then composed of a data-flow, platform and mapping:

V DS ⊆ (V DG × V RG × V M )

Design Space as a Behavioral Product Line

Automata and model-checking techniques have been widely used to model and validate real-time and embedded systems [START_REF] Bengtsson | Uppaal-a tool suite for automatic verification of real-time systems[END_REF][START_REF] Clarke | Model checking[END_REF]. Interestingly, the basic approach used is to schedule an application automaton using a platform automaton [START_REF] Dalsgaard | Metamoc: Modular execution time analysis using model checking[END_REF]. Unfortunately, these approaches are not design to manage any variability aspect of specifications.

Our framework relies on Featured-Transition-Systems (FTS) to represent and validate the design space. FTS has the strength to model explicitly the variability points structurally, through a Feature Diagram [START_REF] Batory | Feature models, grammars, and propositional formulas[END_REF] (FD), instead of modeling variability points behaviorally, by optional transition with possible constraints [START_REF] Beek | Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints[END_REF]. This eases the transformation to featured automaton and the removal of invalid implementations from it. In our approach, we also use LT L property to ensure that all valid execution paths of all system implementations reach the end state of all task of the data-flow. Definition 5. A featured automaton is a tuple F A = (Loc, Loc0, I, Act ⊆ Af f ∪φ∪Com, trans, χ, Ch, L, AP, d, λ) such that:

• Loc is a finite set of locations, Loc0 ∈ Loc, is a set of initial states and I ∈ Loc, is a set of final states,

• Ch is a finite set of communication channels,

• χ is a finite set of variables,

• Act is a set of, Af f which is a finite set of variable affectations, φ which is a finite set of guards in a boolean expression form and Com, which is a set of communications Com ⊆ {c!m, c?m, c!?m|c ∈ Ch, m ∈ χ}

• trans ⊆ Loc × Act × Loc are state transitions, • d = (N ⊆ Nm ∪ Nopt ∪ Nxor, DE ⊆ N × N, T cl) is a Feature Diagram (FD)
, N is the set of mandatory, optional and alternatives features, DE represents relation between features, T cl are constraints between features, d F D ⊆ P(N ) is the set of valid product configurations,

• λ : trans → B(N ) is a total function that labels transitions with feature expressions.

• AP is a set of atomic proposition and L : Loc → AP labels transitions with atomic propositions.

A transition s α -→ s is possible for the set of product configurations P ⊆ λ(s α -→ s ) and if ∀g ∈ α ∩ φ, g is satisfied, ∀(c?m) ∈ α ∩ Com, wait for data event c!m, ∀(c!?m0) ∈ α ∩ Com, send data event c!m0 but wait for data event c!m1 with m0 = m1. Definition 6. A Linear Temporal Logic property (LT L) is a temporal expression of atomic proposition that all possible executions of system variants should satisfy as, f a F A |= ϕ where ϕ ::= a ∈ AP |ϕ ∧ ϕ| ϕ . Symbol means that the property will become true at some point in the future.

We now show how our design space is transformed to a F A.

To simplify the transformation process, let us use the following functions: For example, in our running example, the functions would be:

f : T ∪ P ath ∪ R → N, fs : D ∪ S × N * →
f (a) = A, fs(d2, 1024) = D2Size1024 fto(p1) = p1 T o, f f rom (p f rom ) = p1 F rom, fto(p1, a) = P1T oA, f f rom (a, p2) = P2F romA,
∀t ∈ T, ∀p ∈ |I(t)|, |O(p)| > 1 =⇒ ∃(f (t) ⇐⇒ fto(p, t)) ∈ T cl ∀t ∈ T, ∀p ∈ |O(t)|, |I(p)| > 1, ∃(f (t) ⇐⇒ f f rom (t, p)) ∈ T cl (3.
2) it creates for each task t the automaton (cf. fig. 4(c)) that will wait for data-paths allocation, then call the mapping automaton (cf. fig. 6(c)) to execute the task. ∃{t0 = (s0 The second function GenF A : V RG → F A transforms a variable resource graph into a F A in the following way.

∀p∈I(t),c(p)?in ----------→ s1), where, f (t) ∈ Nopt =⇒ λ(t0) = f (t) ∧ λ((s0 -→ s4) ∈ trans) = ¬f (t), s1 ∀p∈O(t),cm(p)!?out -------------→ s2 , s2 cm(t)!?in,out ---------→ s3,
(1) it creates feature constraints on resource implementation (cf. fig. 5(a)).

∀r ∈ R, θ(r) = =⇒ ∃f (r) ∈ Nopt ∀r ∈ R, ∀rreq ∈ φrequires(r), ∃(f (r) =⇒ f (rreq)) ∈ T cl ∀r ∈ R, ∀rexc ∈ φ excludes (r), ∃(f (r) =⇒ ¬f (rexc)) ∈ T cl (2.
s1 loc(in)=s i ∧∀(b i ,f )∈R b ,b i =f ree ---------------------→ s2, s1 loc(in)=b i ∧b i =in -----------→ s2, s2 loc(out)=so∧∀(f,bo)∈W b ,bo=f ree ----------------------→ s3, s2 loc(out)=bo∧bo=f ree --------------→ s3, s3 c(f )!in,out -------→ s0} ∈ trans
A third function GenF A : V M → F A transforms a variability-aware dataflow-oriented mapping into a F A as follows.

(1.1) it creates features representing all possible task mappings on processor function (cf. fig. 6(a)).

∀(t, f ) ∈ T m, ∃(fm(t) ∈ Nxor, ftm(t, f )) ∈ DE (1.
2) it creates for each task mapping the automaton that executes the processor function according to the mapping configuration (cf. fig. 6(c)).

∀t ∈ T, ∀(t, f ) ∈ T m, ∃{t0 = (s0 cm(t)?in,out --------→ s1), where, fm(t) ∈ Nopt =⇒ λ(t0) = fm(t) ∧ λ((s0 -→ s3) ∈ trans) = ¬fm(t) t1 = (s1 c(f )!?in,out --------→ s2), where, λ(t1) = ftm(t, f ), s2 cm(t)!in,out
--------→ s3}, ∈ trans

∀t ∈ T, f (t) ∈ Nopt =⇒ fm(t) ∈ Nopt ∧ (f (t) ⇐⇒ fm(t)) ∈ T cl
(2.1) If a task mapping feature is implemented on a processor function, the implemented input and output path mappings have to be reachable (cf. fig. 6(a)).

∀(t, f ) ∈ T m, ∀pi ∈ I(t), ∀po ∈ O(t), ∃(ftm(t, f ) ⇐⇒ ( ((x,p i ,t),m∈I(f ))∈Em fpm(pi, m))∧ ( ((t,po,x),m ∈O(f ))∈Em fpm(po, m ))) ∈ T cl (3.1)
If a task mapping feature using an optional processor is implemented, the processor must be implemented too.

∀p = (F, x, y) ∈ P roc, f (p) ∈ Nopt, ∀(t, f ∈ F ) ∈ T m =⇒ ∃(ftm(t, f ) =⇒ f (p)) ∈ T cl
Similarly, if a data-path mapping feature is implemented on fifo buffer of optional processor (3.2) or optional memory storage (3.3), the resource have to be implemented.

(3.2) ∀pu = (F, B, x) ∈ P roc, ∀((y, p, z), b ∈ B) ∈ Em, f (pu) ∈ Nopt =⇒ ∃(fpm(p, b) =⇒ f (pu)) ∈ T cl (3.3) ∀((x, p, y), s ∈ S) ∈ Em, f (s) ∈ Nopt =⇒ ∃(fpm(p, s) =⇒ f (s)) ∈ T cl
As an illustration, in our running example, the rules would be:

(1.2) A ⇐⇒ Am, B ⇐⇒ Bm (3.1) BOnBgpu =⇒ GP U , AOnAgpu =⇒ GP U (3.2) P 2OnR0gpu =⇒ GP U (3.3) P 1OnRAM =⇒ RAM , P 2OnRAM =⇒ RAM P 3OnRam =⇒ RAM

Validation Process

As our form of behavioral product lines is based on FTS [START_REF] Classen | Model checking lots of systems: efficient verification of temporal properties in software product lines[END_REF], model checking techniques can be directly reused. In our implementation (cf. next section), we reuse the ProVeLines checker as a back-end for the validation process. The process consists in verifying all execution paths of all products f a F A of the product line, in an efficient way by exploiting commonalities between different products. Theoretically, the more the products share common behavior and the more efficient should be the variability aware model checking in comparison of iterative model checking on individual systems [START_REF] Classen | Symbolic model checking of software product lines[END_REF]. Instead of exploring all executions for each system implementation, the model-checker explores an execution π once for all implementations P able to produce this specific execution:

P = {p ∈ d F D |π ∈ f a |p A}.
As mentioned in the previous section, some system configurations may expose inconsistent behaviors (e.g., memory allocation error, violation of graphical pipeline constraints). These behaviors will abort the execution and the basic properties (e.g. safety, absence of deadlock, state reachability) will obviously not be satisfied. In our validation process, we are able to remove these configurations from the system by relying again on the back-end model checker [START_REF] Classen | Symbolic model checking of software product lines[END_REF]. It computes the set of bad product configurations, which we remove from the feature diagram of the product line by adding the appropriate cross-tree constraints.

VALIDATION

Implementation

Overview

The framework depicted in Fig. 3 has been entirely implemented in Java. It consists of 3 main modules: i) metamodels of variable application and configurable platform (cf. Fig. 7 and8) ii) mapping meta-model Fig. 9 and algorithm (cf. listing 3) iii) generators that transform the design space composed by all system sub-domains (application, platform, mapping) (cf. listing 4) into formal models of behavioral product line (cf. listings 5 and 6) in order to remove invalid products (cf. listing 8) reusing automated formal reasoning techniques (cf. listing 7).

The first module allows for specifying a variable data-flow oriented application (cf. listing 1) and a configurable platform (cf. listing 2) via fluent APIs. As a result, the running example inputs are captured in less that 30 lines of code.

The second module calls our mapping algorithm (cf. listing 3) in order to infer, at the end, the resulting design space.

The third and last module transforms the design space into a Feature Model in TVL (cf. listing 5) and a Featured Automaton in fPromela (cf. listing 6), capturing, respectively the structural variability and behavior of the design space.

We reuse the ProVeLines model-checker [START_REF] Cordy | Provelines: a product line of verifiers for software product lines[END_REF][START_REF] Classen | Model checking software product lines with snip[END_REF], which consumes TVL and fPromela inputs to assess all system designs, in one run of variability-aware model checking. The resulting outputs, printed as a set of invalid sub-products lines (c.f listing 7), are directly used to constraint the design space to only obtain valid products (cf. listing 8).

Applications as Variable Data-Flows

Listing 1 illustrates how we capture the functional requirements (cf. fig. 1) of the embedded system through an extended data-flow Java API. The data-flow meta-model (cf. Task ta = app.addTask("ta", "A").connect(p1, "i").connect("o", p2);

5
Task tb = app.addTask("tb", "B").connect(p1, "i").connect("o", p2);

6
DataSource d2 = app.addDataSource("D2").addSizes(512, 1024).connect("o", p3);

7
Task tc = app.addTask("tc", "C").connect(p2, "i0").connect(p3, "i1"); 8 app.split(p1).to(ta).to(tb); app.join(p2).from(ta).from(tb);

Platforms as Variable Resource Graphs

Listing 2 illustrates how we express the platform specification (cf. fig. 2) of the embedded system through a resource component based Java API. The platform meta-model (cf. Fig. 8) contains templated resource components such as multi-pass processors instanced at line 13 and streaming processor at line 6. Other elements in the template can be hardware functions instanced at line 7,10,14, read-only memory at line 2, read-write RAM memory at line 3, first-in-first- Component dcu = plt.addComponent("DCU");

7
Processor a_dcu = dcu.addProcessor("a", "A");

8 Memory r0_dcu = dcu.addFIFOBuffer("R0"); 9 a_dcu.connectToInputPort("i", ram, rom).connectToOutputPort("o", r0_dcu);

10
Processor c_dcu = dcu.addProcessor("c", "C"); 11 c_dcu.connectToInputPort("i0", ram, rom, r0_dcu).connect("i1", ram, rom); The mapping algorithm (cf. listing 3) takes as inputs the variable data-flow and configurable platform Java models, and generates the Variability-Aware Mapping Space(cf. Fig.

for metamodel). It then represents all mapping of application elements onto platform resources

The process is composed of two steps : (i) it maps each data source and output data path on storage memories (line 4-7) (ii) it maps each task on appropriate processor function (i.e., processor function can implement the task while data path inputs can be mapped on reachable memory) and maps task output on memory (line 8-11). Then, the algorithm prunes unfeasible mappings w.r.t. structural and variability constraints at line 12 (e.g., data-path mapping are not reachable by any task mapping or vice versa), finally adding appropriate constraints to ensure mapping space consistency (line 13).

Listing 3: Mapping Algorithm

Design Space as a Behavioral Product Line

From the system design space model (cf.listing 4), which is the consistent composition of our 3 system sub-domains (i.e., application, mapping, platform), a Behavioral Product Line representing all system implementations is generated into a Feature Automaton (cf.listing 4). While the behavior of the whole product line is encoded in fPromela (cf. listing 6), a Feature Model in TVL encodes its structural variability (cf.listing 5).

Our framework relies on Featured-Transition-Systems (FTS) to formally reason on the structure and behavior of the design space. FTS has the strength to model explicitly the variability points structurally, through a Feature Diagram [START_REF] Batory | Feature models, grammars, and propositional formulas[END_REF] (FD) in TVL(cf.listing 5).

Thus, a single variability model is able to capture data size at line 9-12, memory capacity at line 19-22, data mapping 28-31, task mapping 32-35, alternative flow 9-12,13,14 vari-abilities, resource optionality 18,24, resource dependency 45, mapping 41 and design space consistency constraints 39, 43. On the other hand, the behavior of the design space is captured by an executable network of featured automata in fPromela where state transitions are guarded by constraints on feature values.

To execute the variable application over the configurable platform, featured automata that capture behavior of dataflow processes, such as data node (lines 18-34) and task node (lines 36-52), call functions over platform resource featured automata, such as memory storage (line 2-16) and processor.

Each featured automaton may have variable properties such as capacity for memory storage process (lines 8-11), data size (lines [START_REF] Sima | Runtime decision of hardware or software execution on a heterogeneous reconfigurable platform[END_REF][START_REF] Singh | Mapping on multi/many-core systems: survey of current and emerging trends[END_REF][START_REF] Temple | Using machine learning to infer constraints for product lines[END_REF][START_REF] Beek | Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints[END_REF] and data deployment location (lines 25-30) for data node process, or task deployment (line 42-47) for task process. In addition to properties, a featured automaton may be optional (i.e., behavior is executed if the element is present in the system design cf. lines 39-50).

According to the subset of design decisions to explore, variable properties are incrementally fixed. For example, for system designs where D2 with a size of 1024 is deployed on RAM with a capacity of 1024, we observe that after allocating D2 on RAM (line 26,6), RAM is full, and any other data allocation on RAM (e.g., D1 or data of P 2) would lead to a memory violation (cf. listing 7 line 4).

Evaluation

Industrial Use Case

In order to validate our tooled approach on an industrial scale, we applied it to a real low-end market instrument cluster provided by Visteon, the automotive systems company we collaborate with.

The functional requirements of the cluster represents a variable data-flow with 3 source images processed by 8 tasks connected by 9 data-paths. Each source image has two different resolutions (i.e HD and LD) and two tasks sub flow sequences are alternative through a xor join/split data-path, If each data-flow variant had one possible implementation on each platform configuration, the number of different cluster system implementations would be 384. In reality, some platform configurations do not provide the graphical functionalities required by some data-flow variants. Furthermore, due to multiple task implementation choices, data-flow variants have several thousand possible implementation alternatives onto a platform configuration. Setting the platform configuration to the higher end (i.e. selecting VRAM and all processors), one can find 72 and 78 possible implementations for two data-flow variants that take different xor data-path decisions. This is due to more pipelining opportunities in the second data-flow variant, even if there is more data-path mapping possibilities in the first one.

Table 1 shows time measurements of the complete toolchain while varying the different variability dimensions over the use case. In the first seven rows, we observe that the whole process is performing well with small to medium scale of variabilities. Data and memory size variability verifications are faster and require more state exploration than platform component and data-path variabilities. Component and data-path variabilities are also slower to check than data and memory size variabilities. It is likely to be due to the fact that contrary to size variability, hardware component and data-path variability are strongly impacting the implementation variability, and consequently the state space of the model checker.

We have also complemented this experimentation by taking a single structural data-flow from the industrial use case with a simulated larger platform, itself with multiple memories and processors. Results in the last three rows of Table 1 show that solving can scale to a large number of implementation variants. Even if the solving time is significant, we observe that the number of states explored to assess all the implementation variants is significantly low. This shows that behavioral commonalities between system variants are used to speed-up the verification process.

Scalability of System Variabilities

We now analyze the scalability of our solution against system variability by increasing the application, platform and mapping variability on simulated data. Fig. 10.a shows measurements of our toolchain for data size and memory capacities variability dimensions (called element variability) while Fig. 10.b is about mapping dimensions. Each variable system denotes his variability dimensions in the following format :

f low; size; resource; capacity; mapping Where f low represents the sum of flow variants of variable data-paths, size the sum of alternatives data sizes, resource the number of optional resources, capacity the sum of alternatives memory capacities and mapping the sum of alternatives mapping of application element onto platform resources.

Fig. 10.a shows a system where data size and memory capacities variability dimensions have been progressively increased so that the first and last system counts, respectively, 384 and 6912 variants. We show relative time and (automaton) states metrics -in total and per variants -compared to the normalized system presenting the lowest variability. Thus, for element variability dimensions (data size and memory capacity), even if, obviously, the time and states number needed to verify the system increase according to variability dimensions, the verification time and states number needed by variant decrease.

For the scalability of the mapping variability dimension, we mainly increase progressively the mapping dimension over 5 systems, the lowest system containing 64 variants while the highest has 23328. We observe that the needed time and explored states number grow quickly. We think this is due to the intrinsic high complexity of both binding and scheduling [START_REF] Singh | Mapping on multi/many-core systems: survey of current and emerging trends[END_REF], which leads to configuration space and state space explosion during checking. However, the verification speed-up by variant is still interesting for high variability system.

Scalability of System Complexities

We analyze here the scalability of our solution against system complexity by growing the application and platform size. Fig. 11.a shows an example where we increased progressively the size and complexity of both application and platform sides while keeping the mapping variability at a common factor (i.e., %40).

The normalized system presenting the lowest complexity and variability. It contains 14 application nodes and paths mapped on a 10 resources platform with 48 variants, while the most complex system has 22 nodes, 13 resources, and 2880 variants. A global system complexity metric, taking into account the system size and it's number of variants, has been discussed with our industrial partner.

We observe that the verification time and states needed increase quickly according to the system complexity (application and platform sizes). Interestingly, as the needed states and time to explore per variant in more complex while the system is growing, the verification time per variant is still lower. This observation can also be made on Fig. 11.b, where we progressively increase the complexity of a system with flow variability.

Threats to Validity

The validation on a single case study can be considered as the major internal threat to validity. Nonetheless it was incrementally built by numerous meetings with different domain experts of the automotive systems company. We gathered specification and feedback from several applications and platforms case studies, and we finally chose the presented one as the most representative among them.

As for external threats, we identified the data sets as the main issue. While the data sets are large, they are still simulated. Our creation procedure has been built to mimic the structure and behavior of both the platforms and the applications, taking the real case studies as a basis to be expanded by generators. Still we do not have empirical evidence of their correspondence.

CONCLUSION AND FUTURE WORKS

A tremendous amount of variability can be observed in embedded systems, and especially in data-flow oriented ones, which are now systematically built from highly variable specifications and target diverse hardware platforms configurable at a very high level of detail. To handle the early functional assessment of all these possible configurations, we proposed in this paper a tooled approach that takes variable dataflow specifications and variable hardware platform models to map them together and transform them into a behavioral product line representing the potential design space. These models and toolchain allow to use automated reasoning techniques to explore and assess the functional feasibility of all represented variants in a single run, and invalid products can be removed by adding constraints to the product line.

We reported on the application of the proposed approach to a real-world industrial use case of automotive instrument cluster, giving hints on a potential good applicability. Our experimental validation with large simulated datasets also shows a good scalability of the prototype implementation for industrial-scale applications and platforms.

As future work, we first plan to facilitate the usage of the framework with domain specific languages for input models (specification and platform), and to conduct larger experiments with them on different and new case studies from our industrial partner. Interestingly, we think that some product lines optimization techniques [START_REF] Dimovski | Efficient family-based model checking via variability abstractions[END_REF][START_REF] Temple | Using machine learning to infer constraints for product lines[END_REF] could be applied to assess more variable and complex embedded systems.

We will also extend our variability-focused framework by taking into account quality attributes (e.g. cost, run-time etc.). The extension would then provide optimized product selection as a complement to the functional validation presented in this paper. We expect this more complete framework to be applicable in different contexts, being similar in the separation of application models being mapped onto component-based platforms.

ACKNOWLEDGMENTS

We thank Visteon Electronics and the Association Nationale de la Recherche et de la Téchnologie for continuously supporting this research. We thank also Emmanuel Roncoroni and Olivier Bantiche who brought industrial expertise in instrument cluster engineering and Maxime Cordy for his valuable support on the ProVeLines model-checker.

Figure 2 :

 2 Figure 2: Platform specification

Figure 3 :

 3 Figure 3: Framework Overview

  the data-path is connected to only one input and output task (i.e the data-path has no flow variability). As data can have alternative sizes, we introduce the function ζ which returns the set of alternative sizes S = ζ(d), each datum has at least one size and if |ζ(d)| > 1 the size of d is variable. If the data-flow has no flow variability, ∀p ∈ P ath, |I(p)| + |O(p)| = 2, and no data variability, ∀d ∈ D, |ζ(d)| = 1, the data-flow is not variable. The functional specification of the running example V DGre is then represented as (Tre = {a, b, c}, Dre = {d1, d2}, P athre = {p1, p2, p3}, Ere = {(d1, p1, a), (a, p2, c), (d1, p1, b), (b, p2, c), (d2, p3, c)})

  N, fto : P ath → N, f f rom : P ath → N, fto : P ath × T → N, f f rom : T ∪ D × P ath → N, fm : T ∪ P ath → N, ftm : T × F → N, fpm : P ath × S ∪ B → N , which transforms model elements to features.

  fm(a) = Am, fm(p1) = P 1m, ftm(a, a dcu ) = AOnA dcu , fpm(p1, ROM ) = p1OnROM f (RAM ) = RAM, fs(RAM, 1024) = RAM Size1024, ... Similarly, c : T ∪ D ∪ P ath ∪ F ∪ S → Ch, cm : T ∪ P ath → Ch transforms model elements to communication channels to interact with them at automaton level. A first function GenF A : V DG → F A × LT L transforms a variable data-flow graph into a F A and generates the LT L property in the following way.(1.1) it transforms each datum d with variable size into a xor feature group (cf. fig.4(a)): ζ(d) > 1 =⇒ ∀s ∈ ζ(d), ∃(f (d) ∈ Nxor, fs(d, s)) ∈ DE (1.2) it creates the automaton for each source datum d ∈ D (cf. fig.4(b)), after setting the datum size, calling the mapping automaton (cf. fig. 6(a, b)) that will allocate the datum on the memory. ∀s ∈ ζ(d), ∃{t0 = (s0 size(in)=s -------→ s1) , where, |ζ(d)| > 1 =⇒ λ(t0) = fs(d, s), s1 ∀p∈O(d),cm(p)!?in ------------→ s2, s2 ∀p∈O(d),c(p)!in ----------→ s3} ∈ trans (2.1) it transforms each variable data-path p in a xor feature group (cf. fig. 4(a)). |O(p)| > 1 =⇒ ∀o ∈ O(p), ∃(fto(p) ∈ Nxor, fto(p, o)) ∈ DE |I(p)| > 1 =⇒ ∀i ∈ I(p), ∃(f f rom (p) ∈ Nxor, f f rom (i, p)) ∈ DE (3.1) it creates task/data-paths consistency constraints (cf. fig. 4(a)).

Figure 4 :

 4 Figure 4: Partial variable data-flow application FA

  1) it creates for each storage s features representing storage alternative sizes. ∀c ∈ ξ(s), ∃(f (s) ∈ Nxor, fs(s, c)) ∈ DE (2.2) it creates for each storage s an automaton that represents basic memory behavior (cf. fig. 5(b)), cons and cap are respectively the consumed size and the maximal capacity of the storage. Through channels, one can allocate memory, and if there is not enough memory, an error is raised. ∀c ∈ ξ(s), ∃{t0 = (s0 cons=0 -----→ s1), where, f (s) ∈ Nopt =⇒ λ(t0) = f (s) ∧ λ((s0 -→ s4) ∈ trans) = ¬f (s), s1 cap=c ----→ s2, where, λ(s1 cap=c ----→ s2) = f (s, c), s2 c(s)?in,cons+=size(in) ---------------→ s3, s3 cons<size -------→ s2, s3 cons≥size,error -----------→ s4} ∈ trans (3) it creates for each processor p an automaton that models basic graphic processor pipeline behavior (cf. fig. 5(c)). When a processor function is executed, the input and output are checked to verify that the pipeline is not misused. ∀p = (F, B, C b ) ∈ P roc, ∀f ∈ F, ∀(si, p) ∈ Cs, ∀(p, so) ∈ Ws, ∀(bi, f ) ∈ C b , ∀(f, bo) ∈ C b , ∃{t0 = (s0 c(f )?in,out -------→ s1), where, f (p) ∈ Nopt =⇒ λ(t0) = f (p) ∧ λ((s0 -→ s4) ∈ trans) = ¬f (p),

( 2 . 1 )( 2 . 2 )

 2122 Like 1.1, it creates features representing all possible data-path mappings on memory. ∀((x, p, y), s) ∈ Em, ∃(fm(p) ∈ Nxor, fpm(p, s)) ∈ DE Like 2.2, it creates for each data-path mapping the automaton that allocates memory (cf. fig.6(b)). ∀p ∈ P ath, ∀((x, p, y), s) ∈ Em, ∃{s0 cm(p)?out ------→ s1, t0 = (s1 c(s)!?out,loc(d)=s -----------→ s2) where, λ(t0) = fpm(p, s), s2 cm(p)!out ------→ s3} ∈ trans Finally the function GenF A : V DS → F A, defined by: GenF A((vdg, vrg, vm)) : GenF A(vdg)||GenF A(vrg)||GenF A(vm), transforms our design space into a featured automaton. (a) Platform FD (b) RAM storage (c) GPU processor

Figure 5 :( 1 . 1 )

 511 Figure 5: Partial variable platform FA

(a)Figure 6 :

 6 Figure 6: Partial Variability-Aware Mapping FA

Fig. 7 )23

 7 contains the classic structure and behavior of the data-flow (data instanced at line 3,6, task at line 4,5,7, datapath at line 2), but also captures the variability in both structural properties (e.g., data size at line 6) and behavioral properties (e.g., alternative flows by allowing data-paths to have multiple input and output tasks connected at line 4,5). Listing 1: Running Example Application 1 Application app = new Application("WarpWithWhat"); Path p1 = app.addPath("P1"); Path p2 = ...; Path p3 = ...; DataSource d1 = app.addDataSource("D1").addSize(512).connect("o", p1);4

9

 9

Figure 7 : 4 ram

 74 Figure 7: Application Metamodel

12 13

 12 Component gpu = plt.addComponent("GPU").setOptional(); 14 Processor a_gpu = ...;Memory r0_gpu = ...;Processor b_gpu = ...; 15 gpu.requires(ram);

Figure 8 :

 8 Figure 8: Platform Metamodel

7 } 8 for( 15 }Figure 9 :

 78159 Figure 9: Mapping Metamodel

Listing 4 :23Listing 5 :

 45 Generate Running Example Formal Models from Design Space 1 DesignSpace ds = new DesignSpace(app, mapping, plt); ToTVL toTVL = new ToTVL().generate(ds); ToPML tofPML = new TofPML().generate(ds); Part of Running Example Design Space variability in TVL

Figure 10 :

 10 Figure 10: Variability Analysis

Figure 11 :

 11 Figure 11: Complexity Analysis

Table 1 :

 1 Industrial use case results

	Variability	Implementation Platform data-flow States explored	Time	ms /	states /
		variants	variants	variants	(re-explored)	(ms)	variants variants
	NONE	78	0	0	2453 (331)	27	0.346	31.448
	Data size	624	0	8	15254 (2406)	201	0.322	35.976
	Platform	424	24	0	5673 (546)	65	0.153	13.379
	Platform and data size	3392	24	8	37435 (4856)	602	0.177	11.036
	data-path	150	0	2	4727 (981)	74	0.493	31.513
	data-path and data size	1200	0	16	29066 (6994)	587	0,489	24,222
	ALL	>4800	24	16	72704 (14652)	2361	-	-
	Platform mult. mem	16408	40	0	134941 (4534)	4010	0.244	8.224
	Platform mult. proc	2848	80	0	19625 (3224)	337	0.118	6.890
	Pltf. mult. proc & mem	516608	160	0	1341999 (175304) 289721	0.560	2.597
	resulting in 16 data-flow variants. The platform specifica-
	tion of the cluster is then represented by a variable hardware
	component system with 2 memories (a Video RAM and a
	ROM Flash) and 3 processors (two multi-pass GPU bitblit-
	ter and one streaming-based DCU). Each processor has a
	pipeline processing of 4 stages and 3 fifo buffers. In terms
	of platform variability, the 2 bitblitters and the VRAM are
	optional. Each memory has 2 different configurable sizes at
	manufacturing time. The number of platform configurations
	in the use case is then 24.

Finding the best solution among the remaining correct solutions is also an important problem, but out of the scope of this paper.