VERIFICATION BY CONSECUTIVE PROJECTIONS


HAGHVERDI E., INAN K.

IFIP TRANSACTIONS C-COMMUNICATION SYSTEMS, cilt.10, ss.465-478, 1993 (SCI İndekslerine Giren Dergi) identifier

  • Cilt numarası: 10
  • Basım Tarihi: 1993
  • Dergi Adı: IFIP TRANSACTIONS C-COMMUNICATION SYSTEMS
  • Sayfa Sayıları: ss.465-478

Özet

A new complexity relief technique for verifying formal specifications based on finite state machines is described. The method uses a Hoare's CSP-like nondeterministic semantics instead of the more commonly used observational equivalence and thus offers greater simplification without an essential loss of information. The approach is based on two algebraic operators on processes that perform parallel composition and process projection. It is shown that under appropriate conditions the complexity raising operation of parallel composition and the complexity reducing operation of process projection can be used alternately to keep the cumulative complexity within practical bounds. The merits of the technique are described via the dining philosophers problem through the concept of the composite philosopher. The method was implemented and applied to an example of alternating bit transport protocol. Presently the verifier implementation is being applied to problems of realistically larger sizes to assess its practical complexity reduction power.