Quantitative Assessments of Distributed Systems
Description
More details
Other editions
Additional editions
Persons
Dario Bruneo received his Degree in Computer Engineering from the Engineering Faculty of the University of Palermo (Italy) in 2000 and the PhD in Advanced Technologies for Information Engineering at the University of Messina (Italy) in 2005. Since then he has been engaged in research on distributed systems. He is currently an associate researcher at the Engineering Faculty of the University of Messina. The research activity of Dario Bruneo has been focused on the study of distributed systems with particular regards to the management of advanced service provisioning, to?the?system modeling and performance evaluation. Different research fields have been investigated ranging from the Quality of Service management, to the distributed programming, from ad-hoc and sensor networks to the performance analysis through analytical and simulative techniques. Is coauthor of more than 40 scientific papers on international journals and conference proceedings.
Salvatore Distefano is an assistant professor of the Politecnico di Milano. His research interests ?include performance evaluation, parallel?and distributed?computing, software engineering, and reliability techniques. During his research activity, he has contributed in the development of several tools such as WebSPN, ArgoPerformance and GS3.?He has been involved in several national and international research projects. He is author and co-author of more than 80 scientific papers.
Content
Preface xiii PART I VERIFICATION 1. Modeling and Verification of Distributed Systems Using Markov Decision Processes 3 1.1 Introduction 4 1.2 Markov Decision Processes 5 1.3 Markov Decision Well-Formed Net formalism 8 1.4 Case study: Peer-to-Peer Botnets 10 1.5 Conclusion 18 Appendices: Well-formed Net Formalism 21 A.1.1 Syntax of Basic Predicates 22 A.1.2 Markings and Enabling 23 References 25 2 Quantitative Analysis of Distributed Systems in Stoklaim: A Tutorial 27 2.1 Introduction 28 2.2 StoKlaim: Stochastic Klaim 29 2.3 StoKlaim Operational Semantics 34 2.4 MoSL: Mobile Stochastic Logic 43 2.5 jSAM: Java Stochastic Model-Checker 47 2.6 Leader Election in StoKlaim 49 2.7 Concluding Remarks 52 References 53 3 Stochastic Path Properties of Distributed Systems: the CSLTA Approach 57 3.1 Introduction 58 3.2 The Reference Formalisms for System Definition 59 3.3 The Formalism for Path Property Definition: CSLTA 61 3.4 CSLTA at work: a Fault-Tolerant Node 67 3.5 Literature Comparison 71 3.6 Summary and Final Remarks 73 References 75 PART II EVALUATION 4 Failure Propagation in Load-Sharing Complex Systems 81 4.1 Introduction 82 4.2 Building Blocks 84 4.3 Sand Box for Distributed Failures 89 4.4 Summary 102 References 103 5 Approximating Distributions and Transient Probabilities by Matrix Exponential Distributions and Functions 107 5.1 Introduction 108 5.2 Phase Type and Matrix Exponential Distributions 109 5.3 Bernstein Polynomials and Expolynomials 114 5.4 Application of BEs to Distribution Fitting 116 5.5 Application of BEs to Transient Probabilities 121 5.6 Conclusions 124 References 125 6 Worst-Case Analysis of Tandem Queueing Systems Using Network Calculus 129 6.1 Introduction 130 6.2 Basic Network Calculus Modeling: Per-flow Scheduling 132 6.3 Advanced Network Calculus Modeling: Aggregate Multiplexing 148 6.4 Tandem Systems Traversed by Several Flows 152 6.5 Mathematical Programming Approach 154 6.6 Related Work 165 6.7 Numerical Results 166 6.8 Conclusions 168 References 171 7 Cloud Evaluation: Benchmarking and Monitoring 175 7.1 Introduction 176 7.2 Benchmarking 176 7.3 Benchmarking with mOSAIC 184 7.4 Monitoring 185 7.5 Cloud Monitoring in mOSAIC?s Cloud Agency 191 7.6 Conclusions 193 References 195 8 Multiformalism and Multisolution Strategies for Systems Performance 201 8.1 Introduction 202 8.2 Multiformalism and Multisolution 203 8.3 Choosing the Right Strategy 205 8.4 Learning by the Experience 206 8.5 Conclusions and Perspectives 218 References 219 PART III OPTIMIZATION AND SUSTAINABILITY 9 Quantitative Assessment of Distributed Networks Through Hybrid Stochastic Modeling 225 9.1 Introduction 226 9.2 Modeling of Complex Systems 228 9.3 Performance Evaluation of KNXnet/IP Networks Flow Control Mechanism 234 9.4 LCII: On-line Risk Estimation of A Power-Telco Network 248 9.5 Conclusion 259 References 261 10 Design of IT Infrastructures of Data Centers: An Approach Based on Business and Technical Metrics 265 10.1 Introduction 266 10.2 Fundamental Concepts 267 10.3 Business-Oriented Models 270 10.4 Data Center Infrastructure Models 274 10.5 Methodology 277 10.6 Case Study - Data Center Design 283 10.7 Conclusion 292 References 297 11 Software Rejuvenation and its Application in Distributed Systems 301 11.1 Introduction 302 11.2 Software rejuvenation scheduling classification 304 11.3 Software rejuvenation granularity classification 307 11.4 Methods, policies and metrics of software rejuvenation 314 11.5 Software rejuvenation in distributed systems 315 11.6 Summary 318 References 321 12 Machine Learning Based Dynamic Reconfiguration of Distributed Data Management Systems 327 12.1 Introduction 328 12.2 Methodologies 330 12.3 Brief overview of Neural Networks 334 12.4 System Architecture and Performance Prediction Scheme 336 12.5 Experimentation 339 12.6 Conclusions 346 References 347 13 Going Green with the Networked Cloud: Methodologies and Assessment 351 13.1 Introduction 352 13.2 Modeling of Data Centre Power Consumption 353 13.3 Energy Efficiency in the Cloud 356 13.4 Performance Analysis Methodologies and Tools 361 13.5 Case Study: Performance Evaluation of Energy Aware Resource Allocation in the Cloud 366 13.6 Summary 370 References 371 Index 375
CHAPTER 1
MODELING AND VERIFICATION OF DISTRIBUTED SYSTEMS USING MARKOV DECISION PROCESSES
MARCO BECCUTI1, GIULIANA FRANCESCHINIS2 AND JEREMY SPROSTON1
1Dipartimento di Informatica, Università di Torino, Italy.
{beccuti,sproston}@di.unito.it
2DiSIT, Istituto di Informatica, Università del Piemonte Orientale, Italy.
giuliana.franceschinis@di.unipmn.it
Abstract.
The Markov Decision Process (MDP) formalism is a well-known mathematical formalism to study systems with unknown scheduling mechanisms or with transitions whose next-state probability distribution is not known with precision. Analysis methods for MDPs are based generally on the identification of the strategies that maximize (or minimize) a target function based on the MDP's rewards (or costs). Alternatively, formal languages can be defined to express quantitative properties that we want to be ensured by an MDP, including those which extend classical temporal logics with probabilistic operators.
The MDP formalism is low level: to facilitate the representation of complex real-life distributed systems higher-level languages have been proposed. In this chapter we consider Markov Decision Well-formed Nets (MDWN), which are probabilistic extensions of Petri nets that allow one to describe complex nondeterministic (probabilistic) behavior as a composition of simpler nondeterministic (probabilistic) steps, and which inherit the efficient analysis algorithms originally devised for well-formed Petri nets. The features of the formalism and the type of properties that can be studied are illustrated by an example of a peer-to-peer illegal botnet.
Keywords. Markov decision processes, modeling and verification.
1.1 Introduction
The mathematical formalism of Markov Decision Processes (MDPs) was introduced in the 1950s by Bellman and Howard [17, 7] in the context of operations research and dynamic programming, and has been used in a wide area of disciplines including economics, manufacturing, robotics, automated control and communication systems. An MDP can be regarded as a Markov chain extended with nondeterministic choice over actions, and is typically equipped with rewards (or costs) associated with transitions from state to state.
A key notion for MDPs is that of strategy, which defines the choice of action to be taken after any possible time step of the MDP. Analysis methods for MDPs are based on the identification of the strategies which maximize (or minimize) a target function either based on the MDP's rewards (or costs), or based on properties satisfied by the MDP's execution paths. For example, in a distributed system, there may be different recovery and preventive maintenance policies (modeled by different actions in the MDP); we can model the system using an MDP in order to identify the optimal strategy with respect to reliability, e.g., the optimal recovery and preventive maintenance policy that maximizes system availability. Reward-based performance indices rely on standard methods for MDPs, whereas path-based properties rely on probabilistic model checking methods [8, 3].
It is important to observe that the formalism of MDPs is low level, and it could be difficult to represent directly at this level a complex real-life distributed system. To cope with this problem, a number of higher-level formalisms have been proposed in the literature (e.g., stochastic transition systems [13], dynamic decision networks [14], probabilistic extensions of reactive modules [1], Markov decision Petri nets and Markov decision well-formed nets [5], etc.).
In this chapter we introduce the MDP formalism in the context of distributed systems and discuss how to express and compute (quantitative) properties which should be ensured by an MDP model (Sec. 1.2). Markov decision well-formed nets (MDWNs) are presented highlighting how they can be a good choice to model multi-component distributed systems (Sec. 1.3) such as an illegal botnet example. Standard MDP analysis and probabilistic model checking techniques are used to compute a number of performance indices on the illegal botnet example (Sec. 1.4).
An application example: peer-to-peer botnet. The application example presented in this chapter is inspired by the peer-to-peer illegal botnet model presented in [23]. Illegal botnets are networks of compromised machines under the remote control of an attacker that is able to use the computing power of these compromised machines for different malicious purposes (e.g., e-mail spam, distributed denial-of-service attacks, spyware, scareware, etc.). Typically, infection begins by exploiting web browser vulnerabilities or by involving a specific malware (a Trojan horse) to install malicious code on a target machine. Then the injected malicious code begins its bootstrap process and attempts to join to the botnet. When a machine is connected to the botnet it is called a bot, and can be used for a malicious purpose (we say that it becomes a working bot) or specifically to infect new machines (it becomes a propagation bot). This choice is a crucial aspect for the success of the malicious activity, meaning that the trade-off between the number of working bots and the number of propagation bots should be carefully investigated. To reduce the probability to be detected, the working and propagation bots are inactive most of the time. A machine can only be recovered if an anti-malware software discovers the infection, or if the computer is physically disconnected from the network.
Our MDP model is similar to that of [23], apart from the fact that we let the choice between the type of malicious activity, working or propagating, be nondeterministic, rather than a fixed probabilistic choice. In this way, we represent all possible choices of assignment of activity to an infected machine, including dynamic strategies that adapt their behaviour to the current global state of the botnet. We consider performance indices such as the average number of working or propagation bots at time t, and the probability that the number of working machines exceeds some threshold within time t. The performance indices obtained from our model are often significantly different from those obtained from a purely probabilistic version of the model in which the choices of activity of a newly infected machine have equal probability.
1.2 Markov Decision Processes
Since the aim of this chapter is to describe how dynamic distributed systems can be effectively studied using MDPs, in this section we introduce the MDP formalism, while in the next section we consider a more high-level formalism for the description of systems which are based on MDPs (more precisely, MDPs provide the underlying semantics of the high-level formalism).
An MDP comprises a set of states, which for the purposes of this chapter we can consider as being finite, together a description of the possible transitions among the states. In MDPs the choice as to which transition to take from a state s is made according to two phases: the first phase comprises a nondeterministic choice among a number of actions available in the state s; whereas the second phase comprises a probabilistic choice between the possible target states of the transition. The probability distribution used to choose the next state of the model in the second phase is determined by the choice of action made in the first phase.
The possibility to combine both nondeterministic and probabilistic choice in MDPs is useful in a number of different contexts. In the context of the formal modeling of systems, nondeterministic choice can be used to represent such factors as interleaving between concurrent processes, unknown implementation details, and (automatic or manual) abstraction.
In the following, we use a set of atomic propositions denoted by AP, which will be used to label the states of an MDP. For example, states corresponding to a system error will be labeled with a certain atomic proposition to distinguish them from non-error states.
A discrete probability distribution over a finite set Q is a function µ : Q [0, 1] such that = 1. We use Dist(Q) to denote the set of distributions over Q.
We now formally present the definition of MDPs. An MDP M = (S, A, p, r, l) comprises: 1) a set S of states; 2) a set A of actions; 3) a partial transition function p : S x A Dist(S); 4) a partial reward function r : S x A 5) a labeling function l : S 2AP.
The transition function, when defined for a state s S and action a A, maps to a distribution p(s, a) over states. For each state s S, we let As denote the set of actions a A for which p(s, a) is defined. We assume that As is non-empty for each state s S. Intuitively, when in the state s, the choice of action a is made nondeterministically from As, and subsequently the next state will be s´ with probability p(s, a)(s´) (see Fig. 1.1). The partial reward function is defined for all states s S and actions a As, and maps to a rational value r(s, a). The labeling function associates with each state s S a set of atomic propositions l(s), which represents a set of observable events that are satisfied in s. The labeling function...
