Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

6-2009

Abstract

Parameterized systems are characterized by the presence of a large (or even unbounded) number of behaviorally similar processes, and they often appear in distributed/concurrent systems. A common state space abstraction for checking parameterized systems involves not keeping track of process identifiers by grouping behaviorally similar processes. Such an abstraction, while useful, conflicts with the notion of fairness. Because process identifiers are lost in the abstraction, it is difficult to ensure fairness (in terms of progress in executions) among the processes. In this work, we study the problem of fair model checking with process counter abstraction. Even without maintaining the process identifiers, our on-the-fly checking algorithm enforces fairness by keeping track of the local states from where actions are enabled / executed within an execution trace. We enhance our home-grown PAT model checker with the technique and show its usability via the automated verification of several real-life protocols.

Keywords

Model Check, Connected Subgraph, Strongly Connect Component, Linear Temporal Logic, Model Check Algorithm

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the Second World Congress Eindhoven, The Netherlands, 2009 November 2-6

First Page

123

Last Page

139

ISBN

9783642050886

Identifier

10.1007/978-3-642-05089-3_9

Publisher

Springer Link

City or Country

Eindhoven, The Netherlands

Additional URL

https://doi.org/10.1007/978-3-642-05089-3_9

Download

Share

COinS