Formal Engineering Methods, International Conference on (1997)
Nov. 12, 1997 to Nov. 14, 1997
K. Taguchi , Dept. of Comput. Sci. & Commun. Eng., Kyushu Univ., Fukuoka, Japan
K. Araki , Dept. of Comput. Sci. & Commun. Eng., Kyushu Univ., Fukuoka, Japan
Presents 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 is given. The main characteristic of the semantics is its ability in describing the evolution of processes and transitions 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.
multiprocessing systems; state-based CCS semantics; Z notation; formal method; value-passing CCS; calculus of communicating systems; concurrent systems specification; state-based semantics; process evolution; state transitions; Hennessy-Milner logic; liveness; safety; actions
K. Taguchi, K. Araki, "The state-based CCS semantics for concurrent Z specification", Formal Engineering Methods, International Conference on, vol. 00, no. , pp. 283, 1997, doi:10.1109/ICFEM.1997.630435