State-based CCS semantics for concurrent Z specification

Kenji Taguchi, Keijiro Araki

Research output: Contribution to conferencePaperpeer-review

38 Citations (Scopus)

Abstract

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.

Original languageEnglish
Pages283-292
Number of pages10
Publication statusPublished - 1997
EventProceedings of the 1997 1st International Conference on Formal Engineering Methods, ICFEM - Hiroshima, Jpn
Duration: Nov 12 1997Nov 14 1997

Other

OtherProceedings of the 1997 1st International Conference on Formal Engineering Methods, ICFEM
CityHiroshima, Jpn
Period11/12/9711/14/97

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Fingerprint Dive into the research topics of 'State-based CCS semantics for concurrent Z specification'. Together they form a unique fingerprint.

Cite this