Affordable Access

Automatic verification of any number of concurrent, communicating processes

Institute of Electrical and Electronics Engineers
Publication Date
  • Qa76 Computer Software
  • Communication


The automatic verification of concurrent systems by model-checking is limited due to the inability to generalise results to systems consisting of any number of processes. We use abstraction to prove general results, by model-checking, about feature interaction analysis of a telecommunications service involving any number of processes. The key idea is to model-check a system of constant number (m) of concurrent processes, in parallel with an "abstract" process which represents the product of any number of other processes. The system, for any specified set of selected features, is generated automatically using Perl scripts.

There are no comments yet on this publication. Be the first to share your thoughts.