Akademik Veri Yönetim Sistemi
IFIP TRANSACTIONS C-COMMUNICATION SYSTEMS, cilt.10, ss.465-478, 1993 (SCI-Expanded)
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.