Communicating Embedded Systems: Software and Design

Chapter 5

Quantitative Verification of Markov Chains ¹

5.1. Introduction

Hardware and software systems are more and more pervasive in every day life and, therefore, there is an obvious demand for these systems to meet the functional and performance requirements that the users expect. Automatic verification methods are a possible, and doable, way to increase our level of confidence in the systems that we design and produce, both in terms of functionality (what the system does) and performance (how long does it take). Verification methods that take into account the randomness of systems work with a model of the system which is a stochastic process. In order to limit the complexity of the verification process, these stochastic processes are often either discrete time Markov chains (DTMC) or continuous time Markov chains (CTMC), usually automatically generated by some higher level formalism such as stochastic Petri nets or stochastic process algebras.

Historically, the functional verification and the evaluation of performance of an application have been considered as two distinct steps of the system development and verification process: each step had its own model and associated verification techniques. In the past 15 years, we have instead witnessed the flourishing of a discipline that aims at taking into consideration both aspects simultaneously, and is often referred to as probabilistic verification or, more appropriately, of verification of probabilistic systems. The moving force ...