| dc.description.abstract | An embedded system is a combination of hardware and software designed
to perform a dedicated function. Embedded systems typically come with
stringent performance constraints such as throughput, latency, memory demands
and resource usages. Deriving (or proving) that these performance
constraints are satisfied in all possible circumstances is a challenging task
due to increasing complexity of such systems.
In this thesis, we focus on formal method-based performance analysis
techniques for dynamic streaming applications using data
ow models
of computation (MoC). Streaming applications are applications that transform
input streams of data of indefinite length to output streams of data.
They are considered dynamic if their computational and communicational
requirements vary at run-time. Data
ow formalisms have been widely used
to model and analyze streaming applications. Finite-state machine-based
scenario-aware data
ow (FSM-SADF) is one of better-known MoCs used
for modeling of dynamic streaming applications. In particular, FSM-SADF
models the execution of a dynamic application as a sequence of fairly static
modes of operation called scenarios. Each scenario is in turn modeled by a
synchronous data
ow (SDF) graph.
FSM-SADF allows rigorous design-time analysis and comes equipped
with various worst-case performance analysis techniques.
However, as the number of scenarios grows, FSM-SADF experiences
compactness problems which in turn render it incapable of capturing applications
exposing fine-grained data-dependent dynamic behavior. As the first
contribution of this thesis we identify the semantic link between FSM-SADF
and parameterized data
ow models based on SDF we refer to as SDF-based
parameterized data
ow (SDF-PDF) by relating the concepts of FSM-SADF
scenario and SDF-PDF configuration/instance. SDF-PDF, by using dynamic
parameters has the ability of capturing fine-grained data-dependent
application dynamics. By exploiting the semantic link with FSM-SADF we
adapt the worst-case throughput and latency analysis techniques of FSM - SADF to be used for the analysis of SDF-PDF models. Thus, we have
indirectly, by introducing the SDF-PDF concept and recasting it into the
FSM-SADF context enabled worst-case performance analysis of applications
exhibiting fine-grained data-dependent dynamism.
SDF-PDF as a parameterized data
ow model considers data-dominated
applications with fine-grained data-dependent dynamics. However, many
streaming applications can in addition have intricate control requirements.
Therefore, the second contribution of the thesis combines parameterized
data
ow and FSM-SADF into a novel model called FSM-based parameterized
scenario-aware data
ow (PFSM-SADF). Combining the properties of
the two, as a FSM/data
ow hybrid, PFSM-SADF is able to capture applications
with both fine-grained data-dependent dynamics and intricate control
requirements. For a
avor of PFSM-SADF based on SDF called SDFbased
PFSM-SADF (SDF-PFSM-SADF), we in addition propose worst-case
throughput and latency analysis techniques.
As the third contribution of the thesis we consider SDF-PFSM-SADF
where parameters are deemed static or change infrequently. This is often
the case for many applications is practice. Under such restricted semantics
(normally, SDF-PFSM-SADF parameters are dynamic), we develop a technique
that expresses the worst-case throughput of the graph as a function
of the graph's parameters. Such expressions can be efficiently evaluated at
both design-time and run-time and therefore can be used to perform both
offine and online optimizations.
The available analysis methods for FSM-SADF are implemented in the
SDF3 tool. However, SDF3 is of limited scope in the sense that it supports
only a predefined set of properties. As the fourth contribution of the thesis,
we report on the translation of the FSM-SADF formalism to uppaal timed
automata that enables a more general verification of FSM-SADF models
than currently supported by existing tools, i.e. by SDF3.
Finally, the fifth and the last contribution of the thesis extends FSMSADF
to enable it to capture systems that make use of event-driven mechanisms
to control the operation of its data-intensive parts. For the extension,
translated to uppaal timed automata, we propose a schedulability analysis
technique formulated as a reachability problem for (ordinary) timed automata.
All of the analysis techniques presented in this thesis are evaluated on
realistic case studies from the multimedia domain and/or on representative
artificial case studies. | nb_NO |
