Verification of parametric concurrent systems with prioritised FIFO resource management

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F08%3APU76683" target="_blank" >RIV/00216305:26230/08:PU76683 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Verification of parametric concurrent systems with prioritised FIFO resource management

Original language description

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 LTLX enriched with global process quantificationand 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 lo

Czech name

Verifikace parametrických systémů paralelních procesů s prioritním FIFO řízením přístupu ke sdíleným zdrojům

Czech description

Článek navrhuje několik originálních výsledků týkajících se využití metody řezů k verifikaci parametrických systémů paralelních procesů s prioritním FIFO řízením přístupu ke sdíleným zdrojům.

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

<a href="/en/project/GA102%2F07%2F0322" target="_blank" >GA102/07/0322: Advanced Formal Approaches in the Design and Verification of Computer-Based Systems</a><br>

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2008

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

FORMAL METHODS IN SYSTEM DESIGN

ISSN

0925-9856

e-ISSN

—

Volume of the periodical

32

Issue of the periodical within the volume

2

Country of publishing house

US - UNITED STATES

Number of pages

44

Pages from-to

—

UT code for WoS article

—

EID of the result in the Scopus database

—