Industrial Applications of Probabilistic Model Checking- A Model-based Approach for Embedded Networked Systems and Concurrent Data Structures -

Nowadays, due to the rapid growth of complexity of hardware/software systems, designing such systems to meet critical requirements (e.g., performance, energy efficiency) becomes an increasingly challenging work. Performance evaluation and optimization becomes a mandatory routine in the system design. This is usually done based on running simulations of very detailed prototypes using specific simulation tools. However the results obtained by simulation usually lack the information of performance bounds caused by the best and worst-case scenarios. In this dissertation, we demonstrate industrial applications of probabilistic model checking -a model-based approach- to evaluate and optimize the performance of systems during design phase. Our applications cover systems from several, currently popular fields: embedded systems, computing servers, the next generation mobile networks and concurrent data structures. %We utilize the probabilistic model called Markov reward automata (MRA), which is capable of modeling and analyzing large systems. On the one hand, it is 1) compositional, 2) allows to be reduced effectively by confluence reduction --a novel on-the-fly reduction technique akin to partial order reduction--, and 3) can be efficiently analyzed. On the other hand, MRA have a rich expressiveness: the transitions equipped with either discrete probability distributions or the exponentially timed delays allow to describe the discrete and continuous stochastic phenomena in system behavior, which are crucial in today's systems due to various sources of uncertainty; the non-determinism allows to model conflicting activities (e.g., scheduling strategies) or underspecification due to unknown or unpredictable environment. Moreover, it also allows rewards to be attached to the states and transitions. Various performance metrics such as average energy consumption, and average throughput of the system can be derived from the quantitative analysis based on MRA. In the first part of the dissertation, we briefly give an overview of several common probabilistic models including Markov automata (MA) and Markov reward automata (MRA). We explain how to model check the quantitive properties on M(R)A and how the reduced state space can be directly generated on-the-fly by confluence reduction. In the end, we give a short introduction to two relevant probabilistic model checking tools we used throughout our applications, which support modeling, state space generation/optimization (e.g., confluence reduction for M(R)A), and analysis based on the probabilistic models. In the second part of the dissertation, we provide five applications of probabilistic model checking and show how the obtained results give us an informative insight of the system design. In each application, we begin with explaining how we model the system to be evaluated in detail and which performance metrics of interest can be derived from the quantitative properties based on probabilistic models. In the end, we analyze the obtained results from probabilistic model checking based on our observations. The first application focuses on a synthesis problem from software to hardware in automotive control systems to optimize the overall energy consumption using the information of driving scenarios as a probabilistic model. We provide a novel combination of two model-based approaches to optimize the energy consumption of automotive control systems rather than using simulation or analytical techniques. The second application considers performance evaluation of embedded systems, which are initially modeled by exponentially timed scenario-aware dataflow (eSADF). We give a formal definition of eSADF and hardware platform in terms of MRAs and various useful performance metrics including energy consumption are derived based on the resulting MRA. In the third application, we provide a first industrial case study to evaluate the performance of computing servers using the recent generalized stochastic Petri nets (GSPNs)-to-Markov automata semantics. In the fourth application, we compare the performance between different scheduling algorithms in long term evolution (LTE) networks through probabilistic model checking. The non-determinism allowed in MRA, which is used to model the decision alternatives (e.g, scheduling possibilities), yields bounds on performance metrics. These bounds provide us useful information about how far is a given scheduling algorithm away from the optimal one (w.r.t. a certain performance metric), which cannot be obtained by using simulation. The last application focuses on the performance comparison between lock-free and lock-based concurrent data structures of various types including stacks, queues, and lists. From these successful industrial applications in the dissertation, we conclude that probabilistic model checking is an effective model-based approach to evaluate the performance of various types of modern systems and provides a uniform and elegant framework from modeling to performance evaluation. Moreover, Markov (reward) automata, which is a rich expressive probabilistic model that can be efficiently analyzed, bridge the gap between an elegant theory and practical engineering needs