Affordable Access

Automatic verification of any number of concurrent, communicating processes

Authors
Publisher
Institute of Electrical and Electronics Engineers
Publication Date
Keywords
  • Qa76 Computer Software
Disciplines
  • Communication

Abstract

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.