In: Lecture Notes in Computer Science, Vol. 1091; Proc. 17th International Conference in Application and Theory of Petri Nets (ICATPN'96), Osaka, Japan, pages 29-56. Springer-Verlag, June 1996.
Abstract: The purpose of this article is to introduce the concepts and ideas that are necessary for understanding computerized process-algebraic compositional verification. Furthermore, by describing two recent case studies an attempt is made to demonstrate the power of the compositional approach and to describe some advanced ways of using the basic techniques. The case studies are given first so that the basic concepts may be introduced in an informal manner. Then the article attempts to elucidate the process-algebraic way of modeling systems and their behaviors. The idea of compositionality is explained. The most important process-algebraic semantic models are described in detail and related to each other, paying special emphasis on algorithmic issues. The representation is at the semantic and state space level; process-algebraic languages are not discussed. Therefore, the techniques presented should be immediately applicable to a wide range of formalisms that can be given semantics in terms of state spaces and transition occurrences.