Worst-case Performance Analysis of Scenario-aware Real-time Streaming Applications

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.