Toward a context-driven deployment optimization for embedded systems: a product line approach

Abstract

Producing a large family of resource-constrained multi-processing systems on chips (MPSoC) is challenging, and the existing techniques are generally geared toward a single product. When they are leveraged for a variety of products, they are expensive and complex. Further in the industry, a considerable lack of analysis support at the architectural level induces a strong dependency on the experiences and preferences of the designer. This paper proposes a formal foundation and analysis of MPSoC product lines based on a featured transition system (FTS) to express the variety of products. First, features diagrams are selected to model MPSoC product lines, which facilitate capturing its semantics as FTS. To this end, the probabilistic model checker verifies the resulting FTS that is decorated with tasks characteristics and processors’ failure probability. The experimental results indicate that the formal approach offers quantitative results on the relevant product that optimizes resource usage when exploring the product family.

1 Introduction

Efficient utilization of computation components in Multi-Processing System-On-Chip (MPSoC) is still a primary issue. Design-Space Exploration (DSE) techniques [46] have been proposed to automatically explore the driven alternative architectures by various system quality attributes (i.e., communication traffic, power, energy), and reporting the near-optimal ones. This daunting process is handled at different levels of abstraction in the design flow [27], and its efficiency relies on the used technique to evaluate the design point at that abstraction level [20, 41]. Architectural DSE, referred to as deployment [3] independently to physical structures, usually focuses on the overall system design and its quality attributes (i.e., the number of processing units, allocation). In contrast, micro-architecture DSE focused on the internal component architecture space (i.e., bus arbiter policy, processor architecture). However, although the evaluation tools at a low level can perform a cycle-accurate analysis [5, 43], it is still challenging to exploit them due to (i) a large number of options and configuration parameters values and (ii) the prohibitively high total run-time.

Based on the Product Line (PL) [8] philosophy, Feature Diagrams (FDs) are a de facto standard where diverse platform variants are identified upfront, and a model of their differences and commonalities is created. Based on the hardware platform configuration provided by Meedeniya et al. [35], the feature diagram for the MPSoC PL shown in Fig. 1 depicts all possible MPSoC configurations (called “products”). Also, features selection for a particular product is not made arbitrarily. The product usage contexts often dictate features selection. The notion of context variability is introduced by [21] and [47] to identify the features selection context.

Fig. 1

System feature diagram of the MPSoC PL

In this paper, the MPSoC product line is divided into two kinds of lines: system and context. The former portrays the hardware platform features, whereas the latter describes the conditional assembly. The study shines a spotlight on the decision-making at the architectural level by using probabilistic model checking to produce a reliable product configuration that optimizes tasks assignment and prunes all possible design alternatives that do not meet given constraints.

1.1 Variability-intensive system

According to Van Gurp et al. [48], “Variability” is commonly understood as the ability of a software system or software artifacts (i.e., components, modules) to be adapted so that they fit a specific context. Building on the definition of variability, Variability-intensive System [34] is a system where variability and related challenges contribute essential influences to software analysis, design, implementation, and evolution. When designed and appropriately implemented, variability-intensive systems can significantly improve development costs, speed, and quality compared to developing and maintaining single products. The variability-intensive system includes product lines, configurable or customizable single systems [17], context-aware mobile applications [32], or OSGi¹ bundles.

1.2 Problem statement

By relying on the deployment studied in the state-of-the-art [26, 31, 38, 51]. All of them state the lack of deployment efficiency in an MPSOC. Sengupta et al. [44] and Conrady et al. [13] rely mainly on meta-heuristic approaches, especially Genetic algorithms, to deploy a processing element. Still, unfortunately, the process requires considerable processing time and memory capacities to come up with only an approximate solution. While other approaches [26, 31] focus more on the low-level view of MPSOC, however, they do not consider the different layers of MPSOC like drivers and other embedded software.

1.3 Current challenges

A product of the MPSoC product line is specified by features encompassing a subset of processing and networking elements. A literature search [49] revealed how to model products by means of transitions system (TS) as shown in Fig. 3a, b. Both TS are produced randomly and do not rely on some selection criteria, the user selects the physical unit (e.g., transition $\texttt { (s=1)} \xrightarrow []{\texttt { PE1}} \texttt {(s=2)}$ in Fig. 3a) modeled as states transition and then makes the deployment (e.g., transition $\texttt { (s=5) }\xrightarrow []{\texttt { DeployPE3}} \texttt {(s=6)}$ in Fig. 3a) modeled also as states transition. The satisfaction is based on the user preference. The first variant in Fig. 3a contains two processors and one bus, whereas the second one, the platform is constituted of three processors and two buses (i.e., we refer by ${{\texttt {PR}}_{{\texttt {i}}}}$ to processors, ${{\texttt {NE}}_{{\texttt {j}}}}$ to buses, and ${{\texttt {T}}_{{\texttt {i}}}}$ to tasks). No logic is applied for selection criteria. Although the problem related to MPSoC variability-space exploration is addressed in several works Mendis et al. [36], Xie et al. [51], Malazgirt and Yurdakul [31], none has provided accurate means for checking variability-intensive MPSoC over temporal properties concerning its usage context.

Fig. 2

Context feature diagram of the MPSoC PL

Fig. 3

TS products generated from Figs. 1 and 2

1.4 Contributions

The paper relies on the formalism of the Featured Transition System (FTS) proposed by Classen et al. [11] that captures all products at a glance. The model is fed to a probabilistic model checker that provides critical insights on the optimal deployment, such as the number of allocated processing elements, while considering reliability as an objective. The model is enhanced with quality metrics related to the operational profile of product components, such as the processing speed and data sizes that are requested to be served by the processing elements.

Our approach is composed of two main phases as portrayed in Fig. 4—FTS construction and quantitative assessment—and validation phase. In the first phase, we combine the system, the context’s feature diagram, the task’s graph, and the components’ reliability obtained from quality metrics [37] to build the FTS in the PRISM input language. The output of this phase is checked by STORM tool [14], a model checker that offers better performance than traditional symbolic model checkers. In particular, we identified a set of properties that can be expressed in a probabilistic fashion (i.e., in PCTL) to address the following question: “How reliable is the mapping of software tasks on an MPSoC platform.” The validation phase considers tasks and hardware platform to perform simulation using the SCoPE tool that opens perspectives of integration with the TASTE tool [2]. A list of acronyms used in the rest of the article is given in Table 1. In a nutshell, we summarize the main contribution of our work.

• Providing the main concepts needed to understand MPSOC components and feature diagrams.

• Formalizing the deployment problem in MPSOC in an understandable and easy way.

• Presenting the theoretical foundation of PTS and FTS as well as describing their semantics in PRISM.

• Developing an approach that runs three phases (construction, verification, validation) to check the correct and precise deployment of the different components in MPSoC.

• Experimenting and validating our developed approach on a real and complex use case.

Table 1 A list of acronyms used in the article

Fig. 4

Proposed methodology for context-driven deployment

The paper is organized as follows. Section 2 reviews the preliminaries, and Sect. 3 introduces the needed concepts related to our reference architecture. Then, Sect. 4 develops our approach regarding tasks assignment and the FTS construction and verification. As an application, a case study from an automotive area in Sect. 5 demonstrates the efficacy of the proposed approach. Sections 6 and 7 present an overview of the related work and concludes the paper, respectively.

2 Preliminaries

This section provides the required concepts forming the basics of our contribution.

2.1 Probabilistic transition system

Probabilistic Transition Systems (PTSs) [18] are a modeling formalism that extends classical Transition Systems (TSs) to exhibit probabilistic and nondeterministic features. Definition 1 formally illustrates a PTS where $\texttt {Dist(S)}$ denotes the set of convex distributions over the set of states S and $\mu \texttt {=[...,s}_{\texttt {i}}\mapsto \texttt {p}_{\texttt {i}}{} \texttt {,...]}$ is a distribution in $\texttt {Dist(S)}$ that assigns a probability $\mu (\texttt {s}_{\texttt {i}})=\texttt {p}_{\texttt {i}}$ to the state $\texttt {s}_{\texttt {i}} \in \texttt {S}$.

Definition 1

(Probabilistic Transition System) A Probabilistic transition system is a tuple $\texttt {M} =\langle {\bar{\texttt {s}}}{} \texttt {, S, L,} \Sigma \;\texttt {,}\; \delta \rangle$:

• ${\bar{\texttt {s}}}$ is an initial state, such that ${\bar{\texttt {s}}} \in \texttt {S}$,

• $\texttt {S}$ is a set of states,

• $\texttt {L: S }\rightarrow \texttt {2}^{\texttt {AP}}$ is a labeling function that assigns each state $\texttt {s} \in \texttt {S}$ to a set of atomic propositions taken from the set of atomic propositions ($\texttt {AP}$),

• ${\Sigma }$ is a finite set of actions,

• $\delta \texttt {: S} \times \Sigma \rightarrow \texttt {Dist(S)}$ is a probabilistic transition function assigning for each $\texttt {s} \in \texttt {S}$ and ${\alpha \in \Sigma }$ a probabilistic distribution $\mu \in \texttt {Dist(S)}$.

For PTS’s composition, this concept is modeled by the parallel composition as stipulated in Definition 2. During synchronization, each PTS resolves its probabilistic choice independently. For transitions, $\texttt {s}_{\texttt {1}} \xrightarrow []{ \alpha } \mu _{\texttt {1}}$ and $\texttt {s}_{\texttt {2}} \xrightarrow []{ \alpha } \mu _{\texttt {2}}$ that synchronize in ${\alpha }$ then the composed state ($\texttt {s'}_{\texttt {1}}{} \texttt {,s'}_{\texttt {2}}$) is reached from the state ($\texttt {s}_{\texttt {1}}{} \texttt {,s}_{\texttt {2}}$) with probability ($\mu _{\texttt {1}}{} \texttt {(s'}_{\texttt {1}}{} \texttt {)} \times \mu _{\texttt {2}}{} \texttt {(s'}_{\texttt {2}}{} \texttt {)}$). In the no synchronization case, a PTS takes a transition where the other remains in its current state with probability one.

Definition 2

(Parallel composition) The parallel composition of two PTSs: $\texttt {M}_{\texttt {1}}=\langle {\bar{\texttt {s}}}_{\texttt {1}}{} \texttt {, S}_{\texttt {1}}{} \texttt {, L}_{\texttt {1}}, \Sigma _{\texttt {1}}, \delta _{\texttt {1}}\rangle$ and $\texttt {M}_{\texttt {2}}=\langle {\bar{\texttt {s}}}_{\texttt {2}}, \texttt {S}_{\texttt {2}}, \texttt {L}_{\texttt {2}}, \Sigma _{\texttt {2}}, \delta _{\texttt {2}}\rangle$ is a PTS $\texttt {M}=\langle ({\bar{\texttt {s}}}_{\texttt {1}},{\bar{\texttt {s}}}_{\texttt {2}}{} \texttt {), S}_{\texttt {1}} \times \texttt {S}_{\texttt {2}}{} \texttt {, L}_{\texttt {s}_{\texttt {1}}} \cup \texttt {L}_{\texttt {s}_{\texttt {2}}}{} \texttt {,} \Sigma _{\texttt {1}} \cup \Sigma _{\texttt {2}}{} \texttt {,} \delta \rangle$ where: $\delta \texttt {: S}_{\texttt {1}} \times \texttt {S}_{\texttt {2}}{} \texttt {,} \Sigma _{\texttt {1}} \cup \Sigma _{\texttt {2}}$ is a set of transitions ($\texttt {s}_{\texttt {1}}{} \texttt {,s}_{\texttt {2}}$) $\xrightarrow []{ \alpha } \mu _{\texttt {1}} \times \mu _{\texttt {2}}$ such that one of the following requirements is met.

• 1. $\texttt {s}_{\texttt {1}} \xrightarrow []{ \alpha } \mu _{\texttt {1}}$, $\texttt { s}_{\texttt {2}} \xrightarrow []{ \alpha } \mu _{\texttt {2}}$, and $\alpha \in \Sigma _{\texttt {1}} \cap \Sigma _{\texttt {2}}$,

• 2. $\texttt {s}_{\texttt {1}} \xrightarrow []{ \alpha } \mu _{\texttt {1}}$, $\mu _{\texttt {2}} = \texttt {[ s}_{\texttt {2}} \mapsto \texttt {1]}$, and $\alpha \in \Sigma _{\texttt {1}} \setminus \Sigma _{\texttt {2}}$,

• 3. $\mu _{\texttt {1}} \texttt {= [ s}_{\texttt {1}} \mapsto \texttt {1]}$, $\texttt {s}_{\texttt {2}} \xrightarrow []{ \alpha } \mu _{\texttt {2}}$, and $\alpha \in \Sigma _{\texttt {2}} \setminus \Sigma _{\texttt {1} }$.

Example 1

To illustrate the applicability of PTS to model dependability, we rely on the case study presented in [28]. The system comprises a processor (M) which reads and processes data from three sensors ($\texttt {S}_{\texttt {1}}$, $\texttt {S}_{\texttt {2}}$ and $\texttt {S}_{\texttt {3}}$) and uses them to control two actuators ($\texttt {A}_{\texttt {1}}$ and $\texttt {A}_{\texttt {2}}$). A concrete example of such a system might be a gas boiler, where the sensors are thermostats and the actuators are valves. Any of the three sensors can fail with probability $\texttt {p}$ expressed by transitions $\texttt {(s=3)} \rightarrow \texttt {(s=2)}$ and $\texttt {(s=2)} \rightarrow \texttt {(s=1)}$ in Fig. 5a, but they are used in triple modular redundancy: the processor can determine sufficient information to proceed provided two of the three are functional. If more than one becomes unavailable the system is shut down. In similar fashion, it is sufficient for only one of the two actuators to be working, but if this is not the case, the system is shut down. The processor can also fail (Fig. 5b). This can be either a permanent fault expressed by transition $\texttt {(i=2)} \rightarrow \texttt {(i=0)}$ with probability $\texttt {p}_{\texttt {f}}$ or a transient fault expressed by transition $\texttt {(i=2)} \rightarrow \texttt {(i=1)}$ with probability $\texttt {p}_{\lambda }$. In the latter case, the situation can be rectified automatically by the processor rebooting itself as expressed by transition $\texttt {(i=1)} \rightarrow \texttt {(i=2)}$. In either case, the system is automatically shut down. The graphical representation of PTS associated with the sensor and processor behavior is portrayed in Fig. 5.

Fig. 5

Overall system structure of sensors-processor in Example 1

2.2 Property specification

The properties specification language PCTL associated with PTSs is expressed by the following BNF grammar:

$$\begin{aligned}&\varphi {:}{:}= \texttt {true} \ |\ \texttt {ap} \ |\ \varphi _{\texttt {1}} \wedge \varphi _{\texttt {2}} \ |\ \lnot \varphi \ |\ \texttt {P}_{\bowtie \texttt {p}} [\psi ] \\&\psi {:}{:}=\texttt {X}\varphi \ | \ \varphi _{\texttt {1}} \cup ^{\le \texttt {k}} \varphi _{\texttt {2}} \ |\ \texttt {F}^{\texttt {t}} \varphi \end{aligned}$$

Where “ap” is an atomic proposition, $\texttt {k} \in {\mathbb {N}}$, $\texttt {p} \in \texttt {]0,1[}$ and $\bowtie \in \texttt {\{} <\texttt {,} \le \texttt {,} >\texttt {,} \ge \texttt {\}}$. “${\wedge }$” represents the conjunction operator and “${\lnot }$” is the negation operator. The probabilistic path operator $\texttt {P}_{\bowtie \texttt {p}} [\psi ]$ provides the probability to satisfy a path formula ${\psi }$ with the constraint $\bowtie \texttt {p}$. “X,” “$\cup ^{\texttt {k}}$” and “${{\cup }}$” are the next, the bounded until and the until temporal logic operators, respectively. Other operators can be derived such as:

• $\texttt {false} \equiv \lnot \texttt {true}$,

• $\varphi _{\texttt {1}} \vee \varphi _{\texttt {2}} \equiv \lnot ( \lnot \varphi _{\texttt {1}} \wedge \lnot \varphi _{\texttt {2}})$,

• $\varphi _{\texttt {1}} \Rightarrow \varphi _{\texttt {2}} \equiv \lnot \varphi _{\texttt {1}} \vee \varphi _{\texttt {2}}$ ,

• $\varphi _{\texttt {1}} \Leftrightarrow \varphi _{\texttt {2}} \equiv \varphi _{\texttt {1}} \Rightarrow \varphi _{\texttt {2}} \wedge \varphi _{\texttt {2}} \Rightarrow \varphi _{\texttt {1}}$ ,

• Future: $\texttt { F} \varphi \equiv \texttt {true} \cup \varphi$ or $\texttt { F}^{\le \texttt {k}} \varphi \equiv \texttt {true} \cup ^{\le \texttt {k}} \varphi$ where $\texttt {k}\ge \texttt {0}$,

• Generally: $\texttt { G} \varphi \equiv \lnot \texttt {(F} \lnot \varphi \texttt {) }$ or $\texttt {G}^{\le \texttt {k}} \varphi \equiv \lnot \texttt {(F}^{\le \texttt {k}} \lnot \varphi )$ and $\texttt {k}\ge \texttt {0}$.

• $\texttt {P}_{\ge \texttt {p}} \texttt {[G} \varphi \texttt {] = P}_{\le \texttt {1-p}} \texttt {[F }\lnot \varphi \texttt {] }$

Below, two requirements (queries) of the system presented in Fig. 5 are expressed in PCTL and illustrated in the natural language.

• $\texttt {P}_{\texttt {=?}} \texttt {[(s} < \texttt {2) \& \& (i = 2) ]}$ “The probability that the number of working sensors has dropped below 2 and the processor is functioning (and so can report the failure).”

• $\texttt {P}_{\texttt {=?}} \texttt {[(i=1)} \cup \texttt {(i = 2) ]}$ “The probability that the processor will be rebooted after a transient failure.”

To specify a satisfaction relation of a PCTL formula in a state “s,” a class of adversaries has been defined [18] to solve the nondeterministic choice in a PTS. Hence, a PCTL formula should be satisfied under all adversaries. The satisfaction relation of a PCTL formula is denoted by “${\vDash }$” and defined as follows, where “s” is a state and “${\pi }$” is a path (sequence of states). In this paper, the path “${\pi }$” is obtained by a memoryless adversary [18].

• $\texttt { s} \vDash \texttt {true}$ is always satisfied,

• $\texttt { s} \vDash \texttt {ap} \Leftrightarrow \texttt {ap} \in \texttt {L(s)}$ and L is a labeling function,

• $\texttt { s} \vDash \varphi _{\texttt {1}} \wedge \varphi _{\texttt {2}} \Leftrightarrow \texttt {s} \vDash \varphi _{\texttt {1}} \wedge \texttt {s} \vDash \varphi _{\texttt {2}}$ ,

• $\texttt { s} \vDash \lnot \varphi \Leftrightarrow \texttt {s} \nvDash \varphi$,

• $\texttt { s} \vDash \texttt {P}_{\bowtie \texttt {p}} \texttt {[}\psi \texttt {]} \Leftrightarrow \texttt {P(}\{ \pi | \pi \vDash \psi \texttt {\})} \bowtie \texttt {p }$ such that the probability of the path $\pi \texttt {= s}_{\texttt {0}}{} \texttt {...s}_{\texttt {n}}$ is given by $\texttt { P(}\pi \texttt {) =} \prod _{\texttt {i=0}}^{\texttt {n-1}} \texttt {p(s}_{\texttt {i}}{} \texttt {, s}_{\texttt {i+1}})$,

• $\pi \vDash \texttt {X} \varphi \Leftrightarrow \pi (\texttt {1}) \vDash \varphi$ where $\pi \texttt {(1)}$ is the second state of ${\pi }$

• $\pi \vDash \varphi _{\texttt {1}} \cup ^{\le \texttt {k}} \varphi _{\texttt {2}} \Leftrightarrow \exists \texttt {i} \le \texttt {k :} \forall \texttt {j}<\texttt {i}, \pi \texttt {(j)} \vDash \varphi _{\texttt {1}} \wedge \pi \texttt {(i)} \vDash \varphi _{\texttt {2}}$,

• $\pi \vDash \varphi _{\texttt {1}} \cup \varphi _{\texttt {2}} \Leftrightarrow \exists \texttt {k}\ge \texttt {0} : \pi \vDash \varphi _{\texttt {1}} \cup ^{\le \texttt {k}} \varphi _{\texttt {2}}$.

2.3 Feature diagrams

Product Line (PL) engineering [45] is a method for expressing large-scale systems, including common and variable features. To express such configuration, FD is dedicated to express variability as depicted in Figs. 1 and 2. A FD has exactly one root (in the example platform and context). Features have a type: either they are “mandatory” (e.g., Feature BUS in Fig. 2), stating that they must be selected or “optional” (e.g., Feature RISC in Fig. 2), stating that may be selected during the derivation process. Multiple optional features are structured in groups and also have a type: an “or” group means that at least one of the group’s features has to be selected, whereas an “And” group requires the selection of all features. A configuration of an FD is said to be valid if it does not contradict any of the constraints imposed by the context FD.

2.4 Context feature diagrams

A system is defined as context-aware if it provides relevant services to the user depending on the context where the system is evolving. For instance, the adaptation feature of smartphones that changes the orientation of the screen (landscape/portrait mode) depends on the phone position. Designers of context-aware systems identify the relevant context features used to adapt the system behavior. Our approach relies on the topology (i.e., connectivity map) structure that describes the physical connections of hardware components. We use “context” variability to model those “context” features intend to be selected or not. The related FD is depicted in Fig. 2. For instance, depending on the current processing element, multiple processors could be selected and linked in the same region. If the processing element PE5 is selected, then multiple successors are available such as: PE3, PE4, PE6, PE3. Also, if the PE5 and PE6 are selected, in this case one network element, NE3 is selected.

However, contemporary product lines approaches do not distinguish context features independently from the system features. According to Capilla et al. [9], one approach is to model context by anchoring system features in one branch and context features in another, as in Hartmann and Trew [21], Ubayashi et al. [47]. However, this approach overloads the number of the relationship between both types of components. The second alternative is to label only those features that relate to context changes as in Mauro et al. [7, 15, 33]. The second alternative is the basis of our approach, distinguishing system features from context features.

3 FTS formalism

In this section, we recall the basic concepts and definitions that will be used throughout the paper.

Let $\texttt {N}$ be a set of all features of a variability-intensive system. A specific set of features $\texttt {p} \subseteq \texttt {N}$ specifies an instance of the variability expressed in the system feature diagram or product in PL terminology. A variability system is then a set of products, i.e., a set of sets of features $\texttt {px} \subseteq {\mathscr {P}}{} \texttt {(N)}$.

Definition 3

An FD $\texttt {d}$ is a tuple $\langle \texttt {N,px}\rangle$, where $\texttt {N} \subseteq \texttt {F}$ is the set of features and $\texttt {px} \subseteq {\mathscr {P}}{} \texttt {(N)}$ is the set of products; We also write $\texttt {[[d]]}_{\texttt {FD}}$.

In this paper, the behavior of the individual product is represented with probabilistic transition systems (PTS). A PTS is a directed graph where transitions are labeled with actions. As an example, the semantics of a subset of hardware platform derived from the $\texttt {FD}$ in Fig. 1 is a combination of processing and networking elements (using short features names): $\texttt {\{ \{ {PE5, NE3, PE6} \}, \{ {PE5, NE3, PE6} \}, \{ {PE5, NE1, PE1} \} \}}$.

A configurable product behavior of $\texttt {p}$ is a non-empty infinite sequence $\sigma = \texttt {s}_{\texttt {0}}\alpha _{\texttt {1}}{} \texttt {s}_{\texttt {1}}\alpha _{\texttt {2}}$ with $\texttt {s}_{\texttt {0}} \in \texttt {I}$ such that $\texttt {s}_{\texttt {i}}\xrightarrow []{\alpha _{\texttt {i+1}} } \texttt {s}_{\texttt {i+1}}$ for all $\texttt {i} \ge \texttt {0}$. A path is an execution from which the information about the transitions has been removed, i.e., , the path ${\pi }$ for the execution ${\sigma }$ is the sequence $\texttt {s}_{\texttt {0}}{} \texttt {s}_{\texttt {1}}\ldots$. The ith state in a path ${\pi }$ is denoted by $\pi _{\texttt {i}}$, and the first state being $\pi _{\texttt {0}}$. The semantic of a TS, written $[[\texttt {ts}]]_{\texttt {TS}}$, is a set of paths.

Classen et al. [11] propose a Featured Transition System (FTS) to describe the behavior of all the products of a PL. Features labeling the FTS transitions belong to the product if and only if the transitions are part of the product behavior. For instance, the situation in which a transition is present if and only if both features $\texttt {a}$ and $\texttt {b}$ that are part of the product can be easily modeled with feature expression $\texttt {a} \wedge \texttt {b}$ Feature expressions are obtained from the context feature diagram. Formally, FTS can be described in terms of automata as:

Fig. 6

FTS of software and hardware platform

Definition 4

An FTS is a tuple $\texttt {fts} =\langle {\bar{\texttt {s}}}, \texttt {S}, \texttt {L}, \Sigma , \delta , \texttt {d}, \gamma \rangle$:

• $\langle {\bar{\texttt {s}}}, \texttt {S}, \texttt {L}, \Sigma , \delta , \texttt {d}, \gamma \rangle$ is a PTS,

• d is a feature model, and

• $\gamma : \delta \rightarrow (\{\bot ,\top \}^{|\texttt {N}|}\rightarrow \{\bot ,\top \})$ is a Boolean function over a set of features labeling each transition with a feature expression.

The behavior of two products introduced in Figs.3a, b of the PL hardware platform in Fig. 1 can be represented with FTS as in Fig. 6. The feature expression (i.e., required features to enable the transition) of the transition is shown next to its actions label, separated by a slash. PE1 is selected when transition ($(\texttt {s}=10) \rightarrow (\texttt {s}=11)$) is triggered if and only if the feature expression $(\texttt {PE2} \wedge \texttt {NE2}) \vee ((PE3 \vee PE4 \vee PE5) \wedge NE1)$ is stated true.

Feature expression configuration is obtained from the context feature diagram where $\texttt {PE1}$ is part of $\texttt {Region 1}$ and $\texttt {Region 2}$. $\texttt {NE1}$ is selected when transition ($(\texttt {s}=\texttt {17}) \rightarrow (\texttt {s}=\texttt {20})$) is triggered if and only if the feature expression $\texttt {PE1} \vee \texttt {PE3} \vee \texttt {PE4} \vee \texttt {PE5}$ is stated true. Feature expression construction is detailed in Sect. 4.4.

In the case where processor $\texttt {PE5}$ is selected, two alternatives are available to select a networking element since the choice is non-deterministic. Two transitions $(\texttt {s}=\texttt {17}) \rightarrow (\texttt {s}=\texttt {20})$ and $(\texttt {s}=\texttt {17}) \rightarrow (\texttt {s}=\texttt {18})$ can be fired since the Boolean feature expressions leading to the selection of NE1: $\texttt {PE1} \vee \texttt {PE3} \vee \texttt {PE4} \vee \texttt {PE5}$ and NE3: $\texttt {PE6} \vee \texttt {PE5}$ are evaluated to true, respectively, except the expression leading to the selection of NE2: $\texttt {PE1} \vee \texttt {PE2}$ is evaluated to false.

Definition 5

(Projection in FTS) The projection of an FTS fts to a product $\texttt {p} \in [[\texttt {d}]]$ noted $\texttt {fts}_{|\texttt {p}}$ is a PTS pts’=$\langle {\bar{\texttt {s}}}, \texttt {S, L}, \Sigma , \delta , \texttt {d,} \gamma \rangle$ where $\delta '=\{\texttt {t} \in \delta | \texttt {p} \vDash \gamma (\texttt {t})\}$.

The behavior of a particular product of the PL is deduced through a projection. So, If the feature expression of FTS transitions is not evaluated to be true, then these transitions are removed. Definition 5 portrays the projection of an FTS.

In the deployment plan of SPL in Fig. 1, e.g., a valid product in the transition system of Fig. 3b (i.e., projection) is derived randomly where the hardware platform contains a set of physical units (i.e., $\texttt {PE1, PE2, NE2}$). This is not admitted by the FTS semantics according to which the platform requires the selection of one processor from $\texttt {\{ PE1, PE2, PE3, PE4, PE5, PE6\}}$. The choice between the transitions $(\texttt {s}=10)\rightarrow (\texttt {s}=11)$, $(\texttt {s}=10)\rightarrow (\texttt {s}=14)$ could be non-deterministic in the first step of the derivation. Moreover, there are more alternatives during the derivation process depending on the presence of some physical units (e.g., $(\texttt {s}=10)\rightarrow (\texttt {s}=12)$ is selected only if the Boolean expression $\texttt {PE3} \vee \texttt {PE4} \vee \texttt {PE5} \wedge \texttt {NE2}$ is satisfied). Finally, one of the product projection corresponds to $\texttt {fts}_{|\{\texttt {T}_{\texttt {1}},..,\texttt {T}_{\texttt {n}},\texttt {PE1,NE2 ,PE2} \}}$.

The FTS represents all products configurations of the PL, and its semantics comprises the semantics of all feasible projections. Its formal definition is given below.

Definition 6

(Semantics of FTS)

$$\begin{aligned}{}[[\texttt {fts}]]_{\texttt {FTS}} = \bigcup _{\texttt {c}\in [[\texttt {d}]]_{\texttt {FD}}} [[\texttt {fts}_{|\texttt {c}}]]_{\texttt {PTS}} \end{aligned}$$

FTS are meant to represent the configuration (i.e., behavior) of the myriad instances of the variability-intensive system. A product derivation is driven by the evaluation of feature expression in FTS. Meanwhile, we do not expect engineers to write this specification manually. So, context information is employed to enrich our FTS model. We need to provide an algorithm considering system and context feature model as inputs to build our FTS.

4 Correct modeling and sound analysis of FTS

In this section, we present FTS modeling using the PRISM language. We use the STORM model checker to accept PRISM source code as input language. Indeed, STORM model checker provides a range of different engines that pursue different approaches to reason on Markov models such as Sparse, Decision Diagram (DD), Hybrid (combine the Sparse and DD engines), etc. The innovation brought by Storm Model Checker is the exploration and abstraction-refinement-based engines [6]. The former is based on the idea of applying techniques from machine learning. On the fly, it tries to explore parts of the system that contribute most to the model checking result. The latter starts with a coarse over-approximation of the concrete model. This abstract model is then analyzed. Then, based on the obtained results, one of two things happens, either the result carries over to the concrete model and can return an answer, or refining the abstracted model. In the last case, the abstraction is performed continuously until reaching a particular answer.

4.1 PRISM language

To construct and analyze FTS with STORM [14], it must be specified in PRISM language. A description of the supported models is provided in [22]. Markov Decision Process (MDP) is selected because it captures probabilistic systems’ behavior by supporting non-determinism and uncertainty. FTS requirements are specified by PCTL temporal logic to express all properties.

Generally, a probabilistic system “$\texttt {S}$” that is described as a PRISM program “$\texttt {P}$” that comprises a set of “$\texttt {n}$” modules ($n>0$), the state of each one is defined by the evaluation of a countable set of finite-ranging local variables. The global state of the system is the evaluation of the local variables ($\texttt {V}_{\texttt {l}}$) and the global ones ($\texttt {V}_{\texttt {g}}$) denoted by $\texttt {V}= \texttt {V}_{\texttt {l}} \cup \texttt {V}_{\texttt {g}}$.

The behavior of each module is a set of guarded commands. Generally, a command takes the following form: $\texttt {[a] g} \rightarrow \texttt {p}_{\texttt {1}}:\texttt {u}_{\texttt {1}} +\cdots + \texttt {p}_{\texttt {m}}:\texttt {u}_{\texttt {m}}$, or, $\texttt {[a] g} \rightarrow \texttt {u}$, which means, for the action “$\texttt {a}$” if the guard “$\texttt {g}$” is true, then, an update “$\texttt {u}_{\texttt {i}}$” is enabled with a probability “$\texttt {p}_{\texttt {i}}$”. For the second case, for the action “$\texttt {a}$” if the guard “$\texttt {g}$” is true, then, the update “$\texttt {u}$” is enabled. A guard is a logical proposition consisting of variables evaluation and propositional logic operators. The update “$\texttt {u}_{\texttt {i}}$” is an evaluation of variables expressed as a conjunction of assignments: $(\texttt {v}'_{\texttt {j}}=\texttt {val}_{\texttt {j}}) \& \ldots \& (\texttt {v}'_{\texttt {k}}=\texttt {val}_{\texttt {k}})$ where $\texttt {v}'_{\texttt {j}}$ are local variables and $\texttt {val}_{\texttt {i}}$ are values evaluated via expressions denoted by “eval” that requires type consistency ($eval: \texttt { V}_{\texttt {l}} \rightarrow {\mathbb {N}} \cup \{ \texttt {true, false}\}$). The formal definition of a command is given in Definition 7.

Definition 7

(PRISM command) A PRISM command is a tuple $\texttt { c}=\langle \texttt {a,g,u}\rangle$, where:

• $\texttt { a}$: is an action label,

• $\texttt { g}$: is a predicate over $\texttt {V}$,

• $\texttt { u}: \{(\texttt {p}_{\texttt {i}},\texttt {u}_{\texttt {i}}) | \ \texttt {m}>1, 0<\texttt {p}<1, \sum ^{\texttt {m}}_{\texttt {i}=1} \texttt {p}_{\texttt {i}}=1$ and $\texttt {u}_{\texttt {i}}=\{(\texttt {v,eval}(\texttt {v})): \texttt {v}\in \texttt {V}_{\texttt {l}} \} \}$

A module that describes the behavior of a sub-part of a system can be considered as a set of commands. The variables of each module are declared and initialized locally. A module is formally defined in Definition 8.

Definition 8

(PRISM module) A PRISM module “$\texttt {M}$” is a tuple $\texttt { M}=\langle \texttt {V}_{\texttt {l}}, \texttt {I}_{\texttt {l}}, \texttt {C}\rangle$, where:

• $\texttt {V}_{\texttt {l}}$: is a finite set of local variables associated with the module M,

• $\texttt { I}_{\texttt {l}}$: is the initial values of $\texttt {V}_{\texttt {l}}$,

• $\texttt { C} =\{ \texttt {c}_{\texttt {i}}:0\le \texttt {i}\le \texttt {k} \}$ is a finite set of commands that defines the behavior of the module M.

To describe the composition between modules, PRISM uses the following Communicating Sequential Processes (CSP) [23] operators.

• Synchronization: It is a parallel composition of modules. For two modules $\texttt {M}_{\texttt {1}}$ and $\texttt {M}_{\texttt {2}}$, their synchronization is denoted by $\texttt {M}_{\texttt {1}} || \texttt {M}_{\texttt {2}}$ and they can synchronize only on actions appearing in both $\texttt {M}_{\texttt {1}}$ and $\texttt {M}_{\texttt {2}}$.

• Interleaving: It is an asynchronous parallel composition of modules that are fully interleaved without synchronization. $\texttt {M}_{\texttt {1}}$ interleaves with $\texttt {M}_{\texttt {2}}$ is denoted by $\texttt {M}_{\texttt {1}} ||| \texttt {M}_{\texttt {2}}$.

• Parallel Interface: It is a restricted parallel composition of modules. The modules synchronize only on shared actions. For example, let $\{\texttt {a,b},\ldots \}$ be the set of shared actions between $\texttt {M}_{\texttt {1}}$ and $\texttt {M}_{\texttt {2}}$, the interface parallel composition of $\texttt {M}_{\texttt {1}}$ and $\texttt {M}_{\texttt {2}}$ in $\{\texttt {a,b},\ldots \}$ is denoted by: $\texttt {M}_{\texttt {1}} | [ \texttt {a,b},\ldots ] | \texttt {M}_{\texttt {2}}$.

As a result, Definition 9 stipulates formally a system containing $\texttt {n}$ modules and combined by a CSP algebraic expression.

Definition 9

(PRISM system) A PRISM system is a tuple $\texttt { P}=\langle \texttt {V, I, exp, M}_{\texttt {1}}, \ldots , \texttt {M}_{\texttt {n}}, \texttt {CSPexp} \rangle$, where:

• $\texttt {V}= \texttt {V}_{\texttt {g}} \bigcup ^{\texttt {n}}_{\texttt {i}=1} \texttt {V}_{\texttt {li}}$: is a finite set of the union of global and local variables,

• $\texttt {I}= \texttt {I}_{\texttt {g}} \bigcup ^{\texttt {n}}_{\texttt {i}=1} \texttt {I}_{\texttt {li}}$: is a finite set of the initial values of global ($\texttt {I}_{\texttt {g}}$) and local ($\texttt {I}_{\texttt {l}}$) variables,

• exp is a set of global logic expressions,

• $\texttt {M}_{\texttt {1}}, \ldots , \texttt {M}_{\texttt {n}}$ is a countable set of modules,

• CSPexp is a CSP algebraic expression.

Example 2

The PRISM model of the system described in Fig. 5 comprises three modules, one for the sensors, one for the actuators, and one for each processor. Lines 5–10 in listing 1 show the section of the PRISM language description which models the sensors. This constitutes a single module sensor with an integer variable $\texttt {s}$ representing the number of sensors currently working. The module’s behavior is described by one guarded command, which represents the failure of a single sensor. Its guard “$\texttt {s} > \texttt {0}$” states this can occur at any time, except when all sensors have already failed. The action $(\texttt {s}'=\texttt {s-1})$ simply decrements the counter of functioning sensors.

Lines 12–21 in listing 1 show a second module which is the PRISM language description of the input processor. The module has a single variable i with range $\{\texttt {0, 1, 2}\}$ which indicates which of the three possible states the processor is in, i.e., whether it is working, is recovering from a transient fault, or has failed. The three guarded commands in the module correspond, respectively, to the processor failing, suffering a transient fault, and rebooting. Two points of note are as follows. Firstly, the guards of these commands can refer to variables from other modules, as evidenced by the use of $\texttt {s} \ge \texttt {2}$. This is because the processor ceases to function once it has detected that less than two sensors are operational. Secondly, the last command contains an additional label reboot, placed between the square brackets at the start of the command. This is used for synchronizing actions between modules, i.e., allowing two or more modules to make transitions simultaneously.

4.2 FTS reachability

As reported in Sect. 1.4, the primary purpose of the proposed approach is to capture the FTS based on its system and context feature diagram and encode it into PRISM input language as PTS. Thus, the PRISM model checker performs a search in the state space of the FTS, and thus it needs an equal representation in PRISM language that is faithful to the FTS semantics. Therefore, the model checking algorithm has to keep track of the states and the products in which they are reachable.

The reachability relation $\texttt {R}$ is the computed structure by the model checking algorithm as the FTS is explored. It is a set of couples ($\texttt {s,px}$) such that a state $\texttt {s}$ is reachable by the products in $\texttt {px}$.

Definition 10

A reachability relation of an FTS is a total function, $\texttt {R: S} \mapsto \texttt {P(N)}$, so that $\forall \texttt {s} \in \texttt {S, p} \in \texttt {R(s)}$, $\texttt {s}$ is reachable in $\texttt {fts}_{|\texttt {p}}$:$\exists \pi \in [[\texttt {fts}_{|\texttt {p}}]]_{\texttt {TS}}$, $\texttt {i} \in \mathrm {N}$, and $\texttt {head}(\pi _{\texttt {i}})= \texttt {s}$.

Computing $\texttt {R}$ is efficiently handled by STORM while exploring the FTS. STORM model checker implements a lot of engines as the constructed models can be stored as binary decision diagrams (BDDs) and multi-terminal BDDs (MTBDDs). They have demonstrated to enable the verification for large hardware circuits. Moreover, encoding the reachable states in PRISM language by Boolean variables that are true if the reachable state is selected.

Given a state $\texttt {s}$ reachable by-products in $\texttt {px}$, a transition leaving $\texttt {s}$, say $\texttt {t}=\texttt {s} \rightarrow \texttt {s}'$, can be fired for all products if the selected feature belongs to the connectivity context of the required components, else, $\texttt {s}'$ will only be reachable by a subset of $\texttt {px}$. It is formalized in the following definition.

Definition 11

The successors of a state $\texttt {s} \in \texttt {S}$ for a product $\texttt {px} \in \texttt {P(N)}$ are given by:

$$\begin{aligned} \texttt { Post (s,px)} =\{ (\texttt {s}',\texttt {px}') | \texttt {s} \xrightarrow {\alpha } \texttt {s}' \in \delta \wedge \texttt {px}' = \texttt {px} \cap [[\gamma (\texttt {s}\rightarrow \texttt {s}')]] \} \end{aligned}$$

Let us illustrate this with the configuration platform given in Fig. 6. State $\texttt {(s=10)}$ is an initial state, and thus reachable by all products. From there, the transitions $(\texttt {s}=10) \xrightarrow {\texttt {PE1}} (\texttt {s}=11)$ can be only fired by products in ${[[({\texttt {PE2}} \wedge {\texttt {NE2}}) \vee ({\texttt {PE3}} \wedge {\texttt {PE4}} \wedge {\texttt {PE5}} \wedge {\texttt {NE1}}) ]]}$. The transition $(\texttt {s}=17) \xrightarrow {\texttt {NE1}} (\texttt {s}=20)$ can be fired for all products in ${[[({\texttt {PE1}} \vee {\texttt {PE2}}) ]]}$.

4.3 FTS platform construction

Figure 7 defines the metamodel that structures the construction of the FTS based on the feature diagram. The class $\texttt {Diagram}$ located in the top left captures the initial node of the feature diagram through the function $\texttt {getRoot}()$. The class $\texttt {Diagram}$ contains a set of nodes and it is specified by the relation $\texttt {hasNodes}()$ with a cardinality (${{\texttt {1}} \rightarrow {\texttt {*}}}$). The class $\texttt {Node}$ is identified by its attribute $\texttt {name}$ of type $\texttt {String}$. This class is endowed with four operations. $\texttt {isRoot}()$ indicates if the $\texttt {Node}$ is the root of the feature diagram, whereas the operation $\texttt {isLeaf}()$ indicates if the Node has no successors. For example, the processing element $\texttt {PE1}$ in Fig. 1 is a leaf node and the $\texttt {Platform}$ is the root. The operation $\texttt {getParent}()$ returns the predecessor of the currently visited node except the root in which the operation returns $\texttt {NULL}$. The operation $\texttt {getsiblings}()$ returns the set of nodes that are located at the same level. If the node has successors, the relation $\texttt {hasSuccessors}()$ identifies the kind of successors according to the concepts studied in Sect. 2 by the class $\texttt {Child}$. Three kinds of relationships are identified in the paper as a function: $\texttt {OR}()$, $\texttt {AND}()$, and $\texttt {MULT}()$. Each operation returns a set of successors. Meanwhile, when the feature diagram is explored, Algorithm 3 has to identify the nature of that relationship through the operation $\texttt {isOR}()$, $\texttt {isAND}()$ and $\texttt {isMULT}()$. Each of that operation returns a Boolean value. Moreover, the node could be $\texttt {mandatory}$ or $\texttt {optional}$. The types of the successors are identified when the operation $\texttt {isMULT}()$ returns true. For the sake of accuracy, three kinds of nodes are identified: $\texttt {Processor}$, $\texttt {Network}$ or $\texttt {Task}$ using the operations $\texttt {isProcessors}()$, $\texttt {isNetwork}()$ and $\texttt {isTask}()$, respectively. The relative operations belong to the class $\texttt {Kind}$.

Fig. 7

Feature diagram metamodel

Based on the metamodel in Fig. 7, the task graph and the feature diagrams exploration process are modeled in Listing 2 and Listing 3. In Listing 2, the exploration starts by exploring the system feature diagram as depicted in lines 3–7. In lines 13–44, the algorithm verifies the type of successors. In line 15, the algorithm checks if the successors are multiples, then it deeply traverses the tree until the three leaves are located. If the kind of the feature is a processor (Line-19), then the algorithm returns the context of that leaf as PRISM formula $ctx_{i}$. The formula is defined by Table 2 as follows as described in line 22. The engine will check if the formula is satisfied to activate the next state. Line 23 portrays a probabilistic command where the successful execution depends on the quality metrics reported in the task graph (see Sect. 3). When the processor is selected, then the equivalent commands are depicted in lines 30–31. The algorithm explores recursively the feature diagram (line 36) such that the exploration terminates when the leaf is located.

The algorithm in Listing 3 is customized according to the context of the deployment. So, the objective is to find the tree leaves and their siblings to construct the formula. For instance, in lines 7–19, if the node successor’s branch is a disjunction, the formula is generated following Table 2 (line 2). In contrast, if the successor branch is a conjunction, the formula is produced following Table 2 Line-1. However, if the siblings are optional or mandatory, as shown in Table 2line 1, the PRISM code is generated according to lines 19–32 in Listing 2.

Table 2 Mapping from feature diagram to PRISM formula

4.4 FTS software construction

Following the same manner of the platform construction, the same metadata that structures the construction of the FTS based on the feature diagram is used. In Fig. 6, a top part is dedicated for task selection based on its predecessors. For instance, Task $\texttt {T1}$ is selected if the task $\texttt {T9}$ and $\texttt {T4}$ were selected and that, the transition ($(\texttt {s}= 0) \rightarrow (\texttt {s}=1)$) is enabled. The same process is executed for the rest of the tasks. It is represented by the PRISM command in Listing 4 (lines 1–16). Each task is declared as a Boolean variable and initialized to false (line 4–7) except the FTS node “${\bar{\texttt {s}}}$” is initialized to true. In the beginning, the STORM engine selects randomly one task from a set of tasks, as mentioned in line 9. When the command is enabled, it sets the task variable to true. The context in which the task is selected depends on its tasks predecessor. For instance, a task is considered as an initial task means that its context formula is set to true (line 16).

5 Evaluation

The developed tool² takes as input system and context feature diagrams related to the hardware platform and the tasks graph to build FTS in PRISM language. STORM model checker accepts PRISM language as input and PCTL properties to perform verification on automotive systems following steps presented in Fig. 4.

5.1 Construction phase

Fig. 8

Task graph

Fig. 9

Automatic braking system

The application in Fig. 9 is mapped into the MPSoC system is the Automatic Braking System (ABS) [35]. The logical views of the subsystems are depicted in Fig. 8. The “$\texttt {ABS Main Unit}$” is the decision-making unit concerning the wheels braking levels, while the “$\texttt {Load Compensator unit}$” computes adjustment factors from the wheel-load sensing inputs. Transceiver software components (4 to 7) are associated with each wheel and communicate with brake actuators and sensors. “$\texttt {Brake Pedal}$” is the software component that reads from the dedicated sensor and sends data to the “$\texttt {Emergency Stop Detection}$” software module (Fig. 9).

Additional parameters are considered in the construction of the FTS model. i) software workload (wl): a computational load of a software component in executing a requested task, and ii) the processing speed ($\texttt {ps}$) expressed in MI (million instructions). Also, parameters are specified for the link between component $\texttt {T}_\texttt {i}$ to $\texttt {T}_{\texttt {j}}$. Data size ($\texttt {ds}$) is the quantity of data exchanged between tasks $\texttt {T}_{\texttt {i}}$ and $\texttt {T}_{\texttt {j}}$ during one communication event and expressed in KB (kilobytes). To obtain a reliability estimation of the automotive architecture in focus, the FTS is extended with reliability’s of the ABS system processing elements and communication links. So, the reliability of component $\texttt {PE}_{\texttt {i}}$ can be computed as:

$$\begin{aligned} \text {R}_{\texttt {i}} = \texttt {e}^{-\texttt {fr}(\texttt {d}(\texttt {T}_{\texttt {i}})) \times \frac{\texttt {wl}(\texttt {T}_{\texttt {i}})}{\texttt {ps}(\texttt {PE}_{\texttt {i}})}}\end{aligned}$$

(1)

Where $\texttt {d}(\texttt {T}_{\texttt {i}})$ denotes the processing elements $\texttt {PE}_{\texttt {i}}$ selected for $\texttt {T}_{\texttt {i}}$, and $\texttt {fr}$ its failure rate. A similar computation can be employed for the reliability of communication elements which are characterized by failure rates ($\texttt {fr}$) of hardware buses and the time taken for communication defined as a function of buses data rates $\texttt {dr}$ and data sizes $\texttt {ds}$ required for software communication:

$$\begin{aligned} \text {R}_{\texttt {i}} = \texttt {e}^{\texttt {-fr}(\texttt {d}(\texttt {T}_{\texttt {i}}),\texttt {d}(\texttt {T}_{\texttt {j}})) \times \frac{\texttt {ds}(\texttt {T}_{\texttt {i}},\texttt {T}_{\texttt {j}})}{\texttt {dr}(\texttt {d}(\texttt {T}_{\texttt {i}}),\texttt {d}(\texttt {T}_{\texttt {j}}))}}\end{aligned}$$

(2)

The resulting FTS is portrayed in Fig. 10, where processing and networking elements fail with probability $\texttt {1-R}_{\texttt {PEi}}$ and $\texttt {1-R}_{\texttt {NEi}}$, respectively. For instance, if $\texttt {PE1}$ is selected then a failure may happen with probability $\texttt {1-R}_{\texttt {PE1}}$ when the transition $(\texttt {s}=11) \xrightarrow []{ \texttt {PE1}_{\texttt {fail}}} (\texttt {s}=10)$ is triggered. A correct processor selection is modeled with transition $(\texttt {s}=11) \xrightarrow []{ \texttt {deployPE1}} (\texttt {s}=17)$ with probability $\texttt {R}_{\texttt {PE1}}$. Also, Networking elements behave as the same fashion as processing elements. For instance, if the networking element $\texttt {NE2}$ is selected a failure may happen may happen with probability $\texttt {1-R}_{\texttt {NE2}}$ when the transition $(\texttt {s}=19) \xrightarrow []{ \texttt {NE2}_{\texttt {fail}}} (\texttt {s}=17)$ is triggered. A correct bus selection is modeled with transition $(\texttt {s}=19) \xrightarrow []{ \texttt {deployPE1}} (\texttt {s}=21)$ with probability $\texttt {R}_{\texttt {NE2}}$.

Fig. 10

A part of FTS in Fig. 6 with components reliability

5.2 Verification phase

To perform analysis, we first study the longest expected time to assure tasks deployment successfully on hardware platforms. STORM model checker provides quantitative results of all possible architecture configurations, including worst and best-case scenarios. This is done using PCTL properties of the form:

$$\begin{aligned} \text {Rmin}=? [ \texttt {F}(``{} \texttt {success}\text {''})] \end{aligned}$$

(3)

$$\begin{aligned} \text {Rmax} =? [ \texttt {F}(``{} \texttt {success}\text {''})]\end{aligned}$$

(4)

which represent the minimum (best case) and maximum (worst case) expected time value, from the beginning until the completion of deployment. Thus, the model is enhanced with rewards associated with states or transitions.

For the MDP model, it associates to each state a value characterizing the expected time between any two deployments. Depending on the task characteristics, the minimum and the maximum expected time for task assignments is 39.8 and 41-time units, respectively. Moreover, we can determine that the application model is mapped to the maximum desired number of processing elements such that the PRISM label reference “success” is true (Listing 5 line 6). This label expresses that the application tasks were deployed. We augment our model with a reward structure that computes the number of processing elements during the assignment to respond to this property. The relative enhancement is described Listing 5 in lines 1–3.

The reward is assigned to transitions of a model labeled with actions PE$_{i}$. It is specified similarly to state rewards, within the ${\textbf {rewards}} ... {\textbf {endrewards}}$ construct.

To check the reliable deployment with optimal processors and buses utilization, the properties (5) and (6):

$$ \begin{aligned}&\text {Pmin}=? [ \texttt {F} \le 40 \ (``{} \texttt {success}\text {''} \ \& \ `` \texttt {PE}\text {''}\ \& \ ``{} \texttt {NE}\text {''})] \end{aligned}$$

(5)

$$ \begin{aligned}&\text {Pmax}=? [ \texttt {F} \le 40 \ (``{} \texttt {success}\text {''} \ \& \ `` \texttt {PE}\text {''}\ \& \ ``{} \texttt {NE}\text {''})] \end{aligned}$$

(6)

enable us to estimate the minimum and maximum probability that the deployment terminates within 40 time steps with a certain number of buses “NE” and processors “PE.”

Our assessments show that not all the deployment candidates are faithful to the requirement of ISO 26262 [25]. This standard targets reliability near 99.99%. Quantitative experiments depicted in Table 3 pinpoint the optimal derived MPSoC platform exploiting five processors, with a probability of 99.997% in the best and worst cases. The evaluation provides a clear view of the number of processors the designer may use to perform the deployment. The advantage of the verification is the ability to enrich our model with parameters that are not visible in the simulation, like reliability. Uncertainties need to be taken into account for system reliability modeling and assessment. The exponential distribution is used to model uncertainties with components failure rates. The approach cannot record the identity of the processors running the tasks due to the high complexity of the FTS model storage. However, a high or a low number of processors is not enough to judge the validity of the deployment. In some cases, the number of processors impacts the consumed energy, which leads to finding a trade-off between the number of processors and energy consumption.

Table 3 Deployment probability

5.3 Validation phase

Although our proposed approach based on probabilistic model checking can estimate solutions that satisfy the high-level constraints and design objectives, the quality of such solutions can also be radically different at a low level. Many metrics can be used in these comparisons. So, we try to validate the relevant product based on simulation as in Fig. 4 to check the performance that is not visible at the FTS level (i.e., Fig. 6). Thus, we measure the quality of our solutions in terms of CPU usage and energy.

SCoPE tool [42] is a C++ library that implements the mechanic to perform MPSoC HW/SW co-simulation and also Network-on-Chip (NoC) analysis. Results may encompass energy, execution time, power, and several executed instructions. Moreover, these outputs may feed design-space exploration to select suitable processors for embedded systems.

The designer starts by defining the hardware infrastructure as it is represented in the feature diagram. The hardware primitives are described in the SCoPE C++ library. SCoPE hardware components are interconnected using standard TLM2 interfaces. When the simulation is done, and results are accepted, the engineers can embed the code and the platform architecture at the high-level representation of the TASTE tool [2, 12] using AADL [16]. A portion of the SCoPE platform description is presented in “Appendix”.

According to the study, the obtained estimations are close to the high-level assessment based on model checking, such that the 80% usage of processors is never attained for the deployment in five and six processors. In contrast, the core energy required to execute the application is acceptable. The different combinations of products in the deployment schema in Fig. 3 are detailed in Figs. 11 and 12. The graphical representation in Fig. 12 portrays the minimum and the maximum CPU utilization for each processor’s configuration. Also, Fig. 11 portrays the consumed energy while the application is running.

To examine the data variation on the graph, it can be seen that the platform with at least one processor and at most four processors results in high CPU utilization and energy. These observations are in line with the already obtained results in Paul et al. [40], Hoque et al. [24], Cinque et al. [10], such that the on-chip cache in the processor is becoming sensitive to failures induced by “soft error.” Another important observation that does not appear in our experiments is that as the processing elements are used, the volume of exchanged data via buses increases, lengthening the actual execution time tasks. As observed, it does not influence our experiments.

Fig. 11

Energy consumption

Fig. 12

The variation on CPU utilization

6 Related work

The current work related to the application of PL is vast and varied, and we try to survey relatively close ones. The aspects covered in this section are modeling language and traditional DSE approaches.

6.1 Model representation

Ziadi et al. [52] propose a UML profile for variability with optional and alternatives stereotypes. This profile is used to model behavior with sequence diagrams, and no verification mechanisms are provided. In contrast, Ghezzi and Sharifloo [19] and Lanna et al. [29] proposed UML and feature diagrams for variability. The diagram used to model product line behavior is a sequence diagram with stereotypes that should correspond to the variability expressed in the feature diagram. The behavioral diagram is transformed into a probabilistic model such as DTMC. Moreover, the approach provides the mechanism to check quantitatively whether the derived products satisfy reliability properties expressed in PCTL.

Andrés et al. [1] provided a formal representation of an FD. They define an algebraic language, called SPLA, to describe Software Product Lines and use SAT-solver to check the satisfiability of an SPL. Varshosaz et al. [50] and Classen et al. [11] proposed featured transitions systems (FTSs), a compact mathematical package to express the behavior of all possible derivations that could occur. Then, the implemented model checking algorithms check all products and identify faulty ones against LTL properties.

These relevant papers do not give a meaning to context features that drive the selection of system features. Some articles, such as Mauro et al. [33], Hartmann and Trew [21] and Ubayashi et al. [47] defined approaches and frameworks that allow modeling customizable evolving context-aware PLs and offer much more expressivity for a product derivation and adaptation [4, 39].

6.2 Design space exploration

In literature, DSE methods depend on the particular abstraction level and design objectives. For example, at lower levels of abstraction, evaluations tools such as RTL simulators [30, 53] are capable of caring slow but cycle-accurate analysis. Meanwhile, at the higher level of abstraction, estimation techniques ranging from analytical models to system-level simulation such as [26, 31, 36, 38, 51] allow designers to obtain estimations of the final deployment candidate. Despite the design solution achievement with a relatively low number of simulations, a total run-time typically in orders of hours of each DSE experiment is still a common denominator. An extensive overview of existing work in the field of software deployment is provided [46].

Compared to the existing works, our paper extends the proposed work [11, 50] to model the tasks and the hardware elements derivations. Moreover, the paper addressed the problem of evaluating the deployment reliability regarding the hardware components’ operational profile. In particular, we introduced a probabilistic model checking approach that can self-balance the number of architectural points to the intended percentiles of the values, which ultimately characterize the system reliability.

7 Conclusion

In this work, we presented a context-driven deployment methodology to analyze a real-time application mapped on an MPSoC system following the product line approach. The presented method relies on the probabilistic model checker called STORM as a basis for modeling and analyzing the real-time applications and MPSoC platforms. The application is characterized by a set of tasks where the platform is derived by varying the components of the hardware library. For an illustration purpose, we presented a real case study adapted from the automotive industry. Compared to the traditional techniques based on simulation, our proposed approach can estimate the reliability of the MPSoC system according to the platform topology constraints. Besides, the user can introduce more restrictions upon the parameterizable model for further resources management, such as power/energy and memory access.

In addition to traditional design objectives such as system performance, there is an increasing need for taking system security into account. Embedded systems are becoming more ubiquitous and interconnected, and they attract attackers. Security, however, cannot be quantified because it interferes with conventional system objectives, contrary to the earlier mentioned ones. Further, addressing this issue at the very early design stage required new techniques. Our future target is to make the software reconfigurable at run-time to accommodate dynamic tasks that require dynamic resource usage.

Appendix: SCoPE platform description

The description of the system to be simulated is done in the sc_main function. In this function, we described the HW platform, the SW infrastructure, and the application SW. The structure of a common SCoPE sc_main function is portrayed in Listing 6. For each OS model, it is required to indicate the number of processors that will be controlled by the OS (line 9). To load the application SW, it is necessary to load in the OS models and the name of the entry function of each application in line 14.