State-based CCS semantics for concurrent Z specification

Kenji Taguchi; Keijiro Araki

State-based CCS semantics for concurrent Z specification

Kenji Taguchi, Keijiro Araki

Advanced Software Engineering

Research output: Contribution to conference › Paper › peer-review

39 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 language	English
Pages	283-292
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

Other	Proceedings of the 1997 1st International Conference on Formal Engineering Methods, ICFEM
City	Hiroshima, Jpn
Period	11/12/97 → 11/14/97

All Science Journal Classification (ASJC) codes

General Engineering

Cite this

@conference{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",

note = "Funding Information: Acknowledgments.　This study was supported in part by grants from Japan Science and Technology Agency (D-S).; Proceedings of the 1997 1st International Conference on Formal Engineering Methods, ICFEM ; Conference date: 12-11-1997 Through 14-11-1997",

year = "1997",

language = "English",

pages = "283--292",

}

TY - CONF

T1 - State-based CCS semantics for concurrent Z specification

AU - Taguchi, Kenji

AU - Araki, Keijiro

N1 - Funding Information: Acknowledgments.　This study was supported in part by grants from Japan Science and Technology Agency (D-S).

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 - Paper

AN - SCOPUS:0031357772

SP - 283

EP - 292

T2 - Proceedings of the 1997 1st International Conference on Formal Engineering Methods, ICFEM

Y2 - 12 November 1997 through 14 November 1997

ER -

State-based CCS semantics for concurrent Z specification

Abstract

Other

All Science Journal Classification (ASJC) codes

Other files and links

Fingerprint

Cite this