Publication detail

Verification of Parameterized Concurrent Systems with Resource Sharing

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

Original Title

Verification of Parameterized Concurrent Systems with Resource Sharing

Type

report

Language

English

Original Abstract

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.

Keywords

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

Authors

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

Released

30. 9. 2002

Publisher

The Information Society Technologies (IST) programme of the EU Fifth Framework Programme

Location

Paris

Pages count

27

URL

http://www.liafa.jussieu.fr/~haberm/ADVANCE/Year2/d12-2.ps

BibTex

@techreport{BUT192487,
  author="Ahmed {Bouajjani} and Peter {Habermehl} and Tomáš {Vojnar}",
  title="Verification of Parameterized Concurrent Systems with Resource Sharing",
  year="2002",
  publisher="The Information Society Technologies (IST) programme of the EU Fifth Framework Programme",
  address="Paris",
  pages="27",
  url="http://www.liafa.jussieu.fr/~haberm/ADVANCE/Year2/d12-2.ps"
}