Lookup NU author(s): Professor Maciej Koutny
Full text for this publication is not currently held within this repository. Alternative links are provided below where available.
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 treeconstruction 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 systemsconsisting of concurrent components communicating via buffers.
Author(s): Kleijn J, Koutny M
Editor(s): Arbab, F., Sirjani, M.
Publication type: Conference Proceedings (inc. Abstract)
Publication status: Published
Conference Name: Fundamentals of Software Engineering: Third IPM International Conference (FSEN)
Year of Conference: 2010
ISSN: 0302-9743 (Print) 1611-3349 (Online)
Notes: This volume contains revised selected papers from the conference
Library holdings: Search Newcastle University Library for this item
Series Title: Lecture Notes in Computer Science