Specification and Verification of Systems Using Model Checking and Markov Reward Models

Lifson, Farrel (2004) Specification and Verification of Systems Using Model Checking and Markov Reward Models, MSc.

PDF flifson.pdf Download (999kB)

Abstract

The importance of service level management has come to the fore in recent years as computing power becomes more and more of a commodity. In order to present a consistently high quality of service systems must be rigorously analysed, even before implementation, and monitored to ensure these goals can be achieved. The tools and algorithms found in performability analysis offer a potentially ideal method to formally specify and analyse performance and reliability models. This thesis examines Markov reward models, a formalism based on continuous time Markov chains, and it's usage in the generation and analysis of service levels. The particular solution technique we employ in this thesis is model checking, using Continuous Reward Logic as a means to specify requirement and constraints on the model. We survey the current tools available allowing model checking to be performed on Markov reward models. Specifically we extended the Erlangen-Twente Markov Chain Checker to be able to solve Markov reward models by taking advantage of the Duality theorem of Continuous Stochastic Reward Logic, of which Continuous Reward Logic is a sub-logic. We are also concerned with the specification techniques available for Markov reward models, which have in the past merely been extensions to the available specification techniques for continuous time Markov chains. We implement a production rule system using Ruby, a high level language, and show the advantages gained by using it's native interpreter and language features in order to cut down on implementation time and code size. The limitations inherent in Markov reward models are discussed and we focus on the issue of zero reward states. Previous algorithms used to remove zero reward states, while preserving the numerical properties of the model, could potentially alter it's logical properties. We propose algorithms based on analysing the continuous reward logic requirement beforehand to determine whether a zero reward state can be removed safely as well as an approach based on substitution of zero reward states. We also investigate limitations on multiple reward structures and the ability to solve for both time and reward. Finally we perform a case study on a Beowulf parallel computing cluster using Markov reward models and the ETMCC tool, demonstrating their usefulness in the implementation of performability analysis and the determination of the service levels that can be offered by the cluster to it's users.

Item Type:	Electronic thesis or dissertation (MSc)
Uncontrolled Keywords:	Markov Reward Models CRL Continuous Reward Logic Beowulf Stochastic Modelling
Subjects:	Computing methodologies > Modeling and simulation Mathematics of computing > Probability and statistics Computer systems organization > Dependable and fault-tolerant systems and networks
Date Deposited:	31 May 2004
Last Modified:	10 Oct 2019 15:35
URI:	http://pubs.cs.uct.ac.za/id/eprint/134

Actions (login required)

View Item