Specification and verification of systems using model checking and Markov reward models

Lifson, Farrel

Specification and verification of systems using model checking and Markov reward models

Master Thesis

2004

Publisher

University of Cape Town

Department

Department of Computer Science

Faculty

Faculty of Science

Abstract

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.

Description

Includes bibliographical references.

Keywords

Computer Science

Reference:

Collections

Masters

Full item page