Stochastic Modelling and Verification

Project details

Funded by: the British Council/DAAD.

Dates: 1998-2001

Institutions: University of Bonn, University of Mannheim, University of Erlangen-Nurnberg, University of Birmingham and Univerity of Edinburgh.

Abstract

This research is concerned with stochastic modelling and verification of computer systems such as distributed systems and communication protocols. The project will focus on advancing the semantic foundations of stochastic process algebras. We will concentrate on: formulating a logic-based specification language for Markovian process algebras, efficient model checking methods for systems with probability and time, and developing the semantic foundations for stochastic process algebras with general distributions.

Aims

The objectives of the research are:

• To develop a logic specification language for Markovian process algebras with exponential distributions.
• To develop the quantitative probabilistic model checking paradigm for processes with real time.
• To consider a class of stochastic process algebras with a large subclass of general distributions.

People

From Birmingham

• Marta Kwiatkowska (British Project Leader)
• Mark Ryan
• Gethin Norman
• Jeremy Sproston
• Amani El-Rayes
• Dave Parker
• Rashid Mehmood
• Stefano Cattani

From Edinburgh

• Jane Hillston
• Stephen Gilmore
• Graham Clark

From Bonn (previously Mannheim)

• Christel Baier (German Project Leader)
• Alexander Asteroth

From Erlangen-Nurnberg

• Ulrich Herzog (German Person Responsible)
• Markus Siegle
• Joachim Meyer-Kayser
• Ulrich Klehmet
• Matthias Kuntz

Associate partners

• Joost-Pieter Katoen
• Holger Hermanns

Further information

Project Meetings:

• Birmingham, 1-3 October 1998.
• Erlangen, 29-30 May 1999.
• Edinburgh, 16-17 March 200.