Publication detail

Verification of parametric concurrent systems with prioritised FIFO resource management

VOJNAR, T. HABERMEHL, P. BOUAJJANI, A.

Original Title

Verification of parametric concurrent systems with prioritised FIFO resource management

English Title

Verification of parametric concurrent systems with prioritised FIFO resource management

Type

journal article - other

Language

en

Original Abstract

We consider the problem of parametric verification over a class of systems of processes competing for access to shared resources. We suppose the access to the resources to be controlled according to a FIFO-based policy with a possibility of distinguishing low-priority and high-priority resource requests. We propose a model of the concerned systems based on extended automata with queues. Over this model, we address verification of properties expressed in LTL\X enriched with global process quantification and interpreted on finite as well as fair behaviours of the given systems. In addition, we examine parametric verification of process deadlockability too. By reducing the parametric verification problems to finite-state model checking, we establish several decidability results for different classes of the considered properties and systems (including the special case of systems with the pure FIFO resource management). Moreover, we show that parametric verification against formulae with local process quantification is undecidable in the given context.

English abstract

We consider the problem of parametric verification over a class of systems of processes competing for access to shared resources. We suppose the access to the resources to be controlled according to a FIFO-based policy with a possibility of distinguishing low-priority and high-priority resource requests. We propose a model of the concerned systems based on extended automata with queues. Over this model, we address verification of properties expressed in LTL\X enriched with global process quantification and interpreted on finite as well as fair behaviours of the given systems. In addition, we examine parametric verification of process deadlockability too. By reducing the parametric verification problems to finite-state model checking, we establish several decidability results for different classes of the considered properties and systems (including the special case of systems with the pure FIFO resource management). Moreover, we show that parametric verification against formulae with local process quantification is undecidable in the given context.

Keywords

formal verification, parameterized concurrent systems, cut-offs

RIV year

2008

Released

01.04.2008

Publisher

NEUVEDEN

Location

NEUVEDEN

ISBN

0925-9856

Periodical

FORMAL METHODS IN SYSTEM DESIGN

Year of study

32

Number

2

State

US

Pages from

129

Pages to

172

Pages count

44

URL

Documents

BibTex


@article{BUT48165,
  author="Tomáš {Vojnar} and Peter {Habermehl} and Ahmed {Bouajjani}",
  title="Verification of parametric concurrent systems with prioritised FIFO resource management",
  annote="We consider the problem of parametric verification over a class of systems of
processes competing for access to shared resources. We suppose the access to the
resources to be controlled according to a FIFO-based policy with a possibility of
distinguishing low-priority and high-priority resource requests. We propose
a model of the concerned systems based on extended automata with queues. Over
this model, we address verification of properties expressed in LTL\X enriched
with global process quantification and interpreted on finite as well as fair
behaviours of the given systems. In addition, we examine parametric verification
of process deadlockability too. By reducing the parametric verification problems
to finite-state model checking, we establish several decidability results for
different classes of the considered properties and systems (including the special
case of systems with the pure FIFO resource management). Moreover, we show that
parametric verification against formulae with local process quantification is
undecidable in the given context.",
  address="NEUVEDEN",
  chapter="48165",
  edition="NEUVEDEN",
  howpublished="print",
  institution="NEUVEDEN",
  journal="FORMAL METHODS IN SYSTEM DESIGN",
  number="2",
  volume="32",
  year="2008",
  month="april",
  pages="129--172",
  publisher="NEUVEDEN",
  type="journal article - other"
}