Paper Info
Title
Verification of parametric concurrent systems with prioritised FIFO resource management
Abstract
We consider the problem of parametric verification over a cla ss 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-pri ority resource requests. We propose a model of the concerned systems based on extended automata with queues. Over this model, we address verification of properti es expressed in LTL\X enriched with global process quantification and interprete d 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 decida bility results for differ- ent classes of the considered properties and systems (inclu ding the special case of systems with the pure FIFO resource management). Moreover, we show that parametric verification against formulae with local proces s quantification is un- decidable in the given context.
Year
DOI
Venue
2008
https://doi.org/10.1007/s10703-008-0048-7
Formal Methods in System Design
Keywords
Field
DocType
Formal verification,Parameterised verification,Infinite-state system verification,Cut off,Model checking,Parameterised networks of processes,Resource sharing
Resource management,Model checking,FIFO (computing and electronics),Computer science,Concurrency,Finite-state machine,Theoretical computer science,Parametric statistics,Temporal logic,Shared resource,Distributed computing
Journal
Volume
Issue
ISSN
32
2
0925-9856
Citations 
PageRank 
References 
17
0.79
17
Authors
3
Name
Order
Citations
PageRank
Ahmed Bouajjani12663184.84
Peter Habermehl250230.39
Tomás Vojnar313627.58