Verification of Parameterized Concurrent Systems with Resource Sharing

formal verification, parametric verification, automated verification, concurrent systems, resource sharing

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 report, 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.