State-based CCS semantics for concurrent Z specification

Kenji Taguchi, Keijiro Araki

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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
Title of host publicationProceedings of the International Conference on Formal Engineering Methods, ICFEM
EditorsM.G. Hinchey, S. Liu
PublisherIEEE Comp Soc
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

Fingerprint

Semantics
Specifications
Specification languages
Formal methods
Acoustic waves

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Cite this

Taguchi, K., & Araki, K. (1997). State-based CCS semantics for concurrent Z specification. In M. G. Hinchey, & S. Liu (Eds.), Proceedings of the International Conference on Formal Engineering Methods, ICFEM (pp. 283-292). IEEE Comp Soc.

State-based CCS semantics for concurrent Z specification. / Taguchi, Kenji; Araki, Keijiro.

Proceedings of the International Conference on Formal Engineering Methods, ICFEM. ed. / M.G. Hinchey; S. Liu. IEEE Comp Soc, 1997. p. 283-292.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Taguchi, K & Araki, K 1997, State-based CCS semantics for concurrent Z specification. in MG Hinchey & S Liu (eds), Proceedings of the International Conference on Formal Engineering Methods, ICFEM. IEEE Comp Soc, pp. 283-292, Proceedings of the 1997 1st International Conference on Formal Engineering Methods, ICFEM, Hiroshima, Jpn, 11/12/97.
Taguchi K, Araki K. State-based CCS semantics for concurrent Z specification. In Hinchey MG, Liu S, editors, Proceedings of the International Conference on Formal Engineering Methods, ICFEM. IEEE Comp Soc. 1997. p. 283-292
Taguchi, Kenji ; Araki, Keijiro. / State-based CCS semantics for concurrent Z specification. Proceedings of the International Conference on Formal Engineering Methods, ICFEM. editor / M.G. Hinchey ; S. Liu. IEEE Comp Soc, 1997. pp. 283-292
@inproceedings{a63570ebea734bf5a8a0bf8a41c9dafc,
title = "State-based CCS semantics for concurrent Z specification",
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.",
author = "Kenji Taguchi and Keijiro Araki",
year = "1997",
language = "English",
pages = "283--292",
editor = "M.G. Hinchey and S. Liu",
booktitle = "Proceedings of the International Conference on Formal Engineering Methods, ICFEM",
publisher = "IEEE Comp Soc",

}

TY - GEN

T1 - State-based CCS semantics for concurrent Z specification

AU - Taguchi, Kenji

AU - Araki, Keijiro

PY - 1997

Y1 - 1997

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0031357772&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0031357772&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:0031357772

SP - 283

EP - 292

BT - Proceedings of the International Conference on Formal Engineering Methods, ICFEM

A2 - Hinchey, M.G.

A2 - Liu, S.

PB - IEEE Comp Soc

ER -