Detail publikace

Verification of parametric concurrent systems with prioritised FIFO resource management

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

Originální název

Verification of parametric concurrent systems with prioritised FIFO resource management

Typ

článek v časopise - ostatní, Jost

Jazyk

angličtina

Originální abstrakt

We consider the problem of parametric verification over a class ofsystems of processes competing for access to sharedresources. We suppose the access to the resources to be controlledaccording to a FIFO-based policy with a possibility of distinguishinglow-priority and high-priority resource requests. We propose a model ofthe concerned systems based on extended automata with queues. Over thismodel, we address verification of properties expressed in LTL\Xenriched with global process quantification and interpreted on finiteas well as fair behaviours of the given systems. In addition, weexamine parametric verification of process deadlockability too. Byreducing the parametric verification problems to finite-state modelchecking, we establish several decidability results for differentclasses of the considered properties and systems (including the specialcase of systems with the pure FIFO resource management). Moreover, weshow that parametric verification against formulae with local processquantification is undecidable in the given context.

Klíčová slova

formal verification, parameterized concurrent systems, cut-offs

Autoři

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

Rok RIV

2008

Vydáno

1. 4. 2008

ISSN

0925-9856

Periodikum

FORMAL METHODS IN SYSTEM DESIGN

Ročník

32

Číslo

2

Stát

Spojené státy americké

Strany od

129

Strany do

172

Strany počet

44

URL

http://www.springerlink.com/content/f234451821483p0j/fulltext.pdf

BibTex

@article{BUT48165,
  author="Tomáš {Vojnar} and Peter {Habermehl} and Ahmed {Bouajjani}",
  title="Verification of parametric concurrent systems with prioritised FIFO resource management",
  journal="FORMAL METHODS IN SYSTEM DESIGN",
  year="2008",
  volume="32",
  number="2",
  pages="129--172",
  issn="0925-9856",
  url="http://www.springerlink.com/content/f234451821483p0j/fulltext.pdf"
}