The state-based CCS semantics for concurrent Z specification

Author

Taguchi, Kenji ; Araki, Keijiro

Author_Institution

Dept. of Comput. Sci. & Commun. Eng., Kyushu Univ., Fukuoka, Japan

fYear

1997

fDate

12-14 Nov. 1997

Firstpage

283

Lastpage

292

Abstract

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.

Keywords

algebraic specification; calculus of communicating systems; formal specification; multiprocessing programs; multiprocessing systems; process algebra; safety; Hennessy-Milner logic; Z notation; actions; calculus of communicating systems; concurrent systems specification; formal method; liveness; process evolution; safety; state transitions; state-based CCS semantics; state-based semantics; value-passing CCS; Algebra; Carbon capture and storage; Computer science; Concurrent computing; Data structures; Information science; Information systems; Logic; Safety; Specification languages;

fLanguage

English

Publisher

ieee

Conference_Titel

Formal Engineering Methods., 1997. Proceedings., First IEEE International Conference on

Conference_Location

Hiroshima, Japan

Print_ISBN

0-8186-8002-4

Type

conf

DOI

10.1109/ICFEM.1997.630435

Filename

630435