Toggle Main Menu Toggle Search

ePrints

Applying Step Coverability Trees to Communicating Component-Based Systems

Lookup NU author(s): Professor Henriette Kleijn, Professor Maciej Koutny

Downloads


Abstract

Like reachability, coverability is an important tool for verifying behavioural properties of dynamic systems. When a system is modelled as a Petri net, the classical Karp-Miller coverability tree construction can be used to decide questions related to the (required) capacity of local states. Correctness (termination) of the construction is based on a monotonicity property: more resources available implies more behaviour possible. Here we discuss a modification of the coverability tree construction allowing one to deal with concurrent occurrences of actions (steps) and to extend the notion of coverability to a dynamic action-based notion (thus viewing bandwidth as a resource). We are in particular interested in component-based systems in which steps are subject to additional constraints like (local) synchronicity or maximal concurrency. In general the behaviour of such systems is not monotonous and hence new termination criteria (depending on the step semantics) are needed. We here investigate marked graphs, a Petri net model for systems consisting of concurrent components communicating via buffers.


Publication metadata

Author(s): Kleijn J, Koutny M

Publication type: Report

Publication status: Published

Series Title: School of Computing Science Technical Report Series

Year: 2009

Pages: 19

Print publication date: 01/01/2009

Source Publication Date: January 2009

Report Number: 1134

Institution: School of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne

URL: http://www.cs.ncl.ac.uk/publications/trs/papers/1134.pdf


Share