In this paper we will present a formal method which combines the Z notation and value-passing CCS (Calculus of Communicating Systems) for specifying concurrent systems. In order to provide a sound theoretical basis for the method, the state-based semantics for value-passing CCS will be given. The main characteristic of the semantics is its ability in describing evolution of processes and transition of states simultaneously. We also present a Hennessy-Milner logic based on that semantics which enables us to express properties such as liveness and safety ascribed both to states and to actions.
|Number of pages||10|
|Publication status||Published - 1997|
|Event||Proceedings of the 1997 1st International Conference on Formal Engineering Methods, ICFEM - Hiroshima, Jpn|
Duration: Nov 12 1997 → Nov 14 1997
|Other||Proceedings of the 1997 1st International Conference on Formal Engineering Methods, ICFEM|
|Period||11/12/97 → 11/14/97|
All Science Journal Classification (ASJC) codes