Specification and verification of systems using model checking and Markov reward 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.

Grantor dc:publisher.institution

Department of Computer Science

Year dc:date.issued

2004

Author dc:creator

• Lifson, Farrel

Advisor dc:contributor.advisor

• Kritzinger, Pieter S

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/11427/6412

OAI identifier oai:identifier

oai:open.uct.ac.za:11427/6412