Formal Methods for Performance Evaluation

Markov chains have become an accepted technique for modeling a great variety of situations. They have been in use since the early 1900’s, but it is only in recent years with the advent of high speed computers and cheap memory that they have begun to be applied to large-scale modeling projects. This paper outlines the events that have lead to the present state-of-the-art in the numerical approach to Markov chain performance modeling and describes current solution methods and ongoing research efforts.

The purpose of this tutorial is to survey queueing networks, a class of stochastic models extensively applied to represent and analyze resource sharing systems such as communication and computer systems. Queueing networks (QNs) have been proved to be a powerful and versatile tool for system performance evaluation and prediction. First we briefly survey QNs that consist of a single service center, i.e., the basic queueing systems defined under various hypotheses, and we discuss their analysis to evaluate a set of performance indices, such as resource utilization and throughput and customer response time. Their solution is based on the introduction of an underlying stochastic Markov process. Then, we introduce QNs that consist of a set of service centers representing the system resources that provide service to a collection of customers that represent the users. Various types of customers define the customers classes in the network that are gathered in chains. We consider various analytical methods to analyze QNs with single-class and multiple-class. We mostly focus on product-form QNs that have a simple closed form expression of the stationary state distribution that allows to define efficient algorithms to evaluate average performance measures. We review the basic results, stating from the BCMP theorem that defines a large class of product-form QNs, and we present the main solution algorithms for single-class e multiple-class QNs. We discuss some interesting properties of QNs including the arrival theorem, exact aggregation and insensitivity. Finally, we discuss some particular models of product-form QNs that allow to represent special system features such as state-dependent routing, negative customers, customers batch arrivals and departures and finite capacity queues. The class of QN models is illustrated through some application examples of to analyze computer and communication systems.

Generalized Stochastic Petri Nets are a modelling formalism that can be conveniently used for the analysis of complex models of Discrete Event Dynamic Systems and for their performance and reliability evaluation. The automatic construction of the probabilistic models that underly the dynamic behaviours of these nets rely on a set of results that derive from the theory of untimed Petri nets. The paper briefly surveys some results of net theory together with the different approaches used to introduce the concept of time in these models that are useful for the definition of Stochastic Petri Nets and Generalized Stochastic Petri Nets. Details on the solution techniques and on their computational aspects are provided. A brief overview of advanced material is included at the end of the paper to highlight the state of the art in this field and to give pointers to relevant results published in the literature.

In this tutorial we give an introduction to stochastic process algebras and their use in performance modelling, with a focus on the PEPA formalism. A brief introduction is given to the motivations for extending classical process algebra with stochastic times and probabilistic choice. We then present an introduction to the modelling capabilities of the formalism and the tools available to support Markovian based analysis. The chapter is illustrated throughout by small examples, demonstrating the use of the formalism and the tools.

Markovian behavioral equivalences are a means to relate and manipulate the formal descriptions of systems with an underlying CTMC semantics. There are three fundamental approaches to their definition: bisimilarity, testing, and trace. In this paper we survey the major results appeared in the literature about Markovian bisimilarity, Markovian testing equivalence, and Markovian trace equivalence. The objective is to compare these equivalences with respect to a number of criteria such as their discriminating power, the exactness of the CTMC-level aggregations they induce, the achievement of the congruence property, the existence of sound and complete axiomatizations, the existence of logical characterizations, and the existence of efficient verification algorithms.

This tutorial presents an overview of model checking for both discrete and continuous-time Markov chains (DTMCs and CTMCs). Model checking algorithms are given for verifying DTMCs and CTMCs against specifications written in probabilistic extensions of temporal logic, including quantitative properties with rewards. Example properties include the probability that a fault occurs and the expected number of faults in a given time period. We also describe the practical application of stochastic model checking with the probabilistic model checker PRISM by outlining the main features supported by PRISM and three real-world case studies: a probabilistic security protocol, dynamic power management and a biological pathway.

Stochastic fluid models have been applied to model and evaluate the performance of many important real systems. The automatic analysis tools to support of fluid models are still not as improved as the ones for discrete state Markov models, but there is a wide range of models which can be effectively described and analyzed with fluid models. Also the model support of hybrid models from various performance evaluation tools improves continuously.

The aim of this work is to summarize the basic concepts and the potential use of Markov fluid models. The factors which determine the limits of solvability of fluid models are also discussed. Practical guidelines can be extracted from these factors to determine the applicability of fluid models in practical modeling examples. The work is supported by an example where Fluid Models, derived from an higher level modeling language (Fluid Stochastic Petri Nets), have been exploited to study the transfer time distribution in Peer-to-Peer file sharing applications.

Stochastic performance models provide a powerful way of capturing and analysing the behaviour of complex concurrent systems. Traditionally, performance measures for these models are derived by generating and then analysing a (semi-)Markov chain corresponding to the model’s behaviour at the state-transition level. However, and especially when analysing industrial-scale systems, workstation memory and compute power is often overwhelmed by the sheer number of states.

This chapter explores an array of techniques for analysing stochastic performance models with large state spaces. We concentrate on explicit techniques suitable for unstructured state spaces and show how memory and run time requirements can be reduced using a combination of probabilistic algorithms, disk-based solution techniques and communication-efficient parallelism based on hypergraph-partitioning. We apply these methods to different kinds of performance analysis, including steady-state and passage-time analysis, and demonstrate them on case study examples.

Decision diagrams are a family of data structures that can compactly encode many functions on discrete structured domains, that is, domains that are the cross-product of finite sets. We present some important classes of decision diagrams and show how they can be effectively employed to derive “symbolic” algorithms for the analysis of large discrete-state models. In particular, we discuss both explicit and symbolic algorithms for state-space generation, CTL model-checking, and continuous-time Markov chain solution. We conclude with some suggestions for future research directions.

This chapter first reviews the origins of Software Performance Engineering (SPE). It provides an overview and an extensive bibliography of the early research. It then covers the fundamental elements of SPE: the data required, the software performance models and the SPE process. It illustrates how to apply the modeling and analysis techniques with a case study. It concludes with a review of the current status and outstanding problems.