View this PageEdit this PageUploads to this PageHistory of this PageTop of the SwikiRecent ChangesSearch the SwikiHelp Guide

11.11. 13.00 Tomáš Vojnar: Verifikace parametrických paralelních systémů se sdílenými zdroji

Verification of Parameterized Concurrent Systems with Resource Sharing

Tomas Vojnar
FIT, Brno University of technology

Ahmed Bouajjani and Peter Habermehl
LIAFA, Paris University 7/CNRS

One very common source of potential errors in concurrent systems is that of access to shared resources. It is thus desirable to be able to verify correctness of the way shared resources are treated in such systems. In the talk, after a slightly extended introduction devoted to automated verification of infinite-state systems in general, we discuss verification of parameterized systems of processes competing for access to shared resources under the FIFO resource management policy with or without priorities. We deal with various generic property classes expressible in (fragments of) temporal logics and covering certain forms of safety, deadlockability, as well as liveness.

In particular, we present three kinds of results. (1) We prove some parametric verification problems arising in the considered context to be efficiently
reducible to finite-state verification. This is done by arguing that to prove a given property for any number of processes, it is often sufficient to consider a certain ``cut-off'' number of processes depending on the number of processes made visible in the formula of interest and/or the number of resources available. (2) For some problems in the domain of FIFO with priorities, we show that using a simple cut-off as in the previous case is in general insufficient.
However, such problems may still be decidable, and there may exist cut-offs taking additionally into account the structure of the process control automaton and/or the formula to be verified. We show an example of such a cut-off for 1-index liveness properties. (3) Finally, we discuss some undecidability results related to the given area.


Link to this Page