An operational semantics for ZCCS

Author

Galloway, A.J. ; Stoddart, W.J.

Author_Institution

Dept. of Comput. Sci., York Univ., UK

fYear

1997

fDate

12-14 Nov. 1997

Firstpage

272

Lastpage

282

Abstract

G. Bruns (1995) has proposed a version of value-passing CCS in which an agent language, based on that proposed by Milner, is augmented with a rich data language. The data language can be used to describe sets, tuples and sequences etc. constructed from integer, Boolean and string constants. Z is a widely used formal specification language in which sets, tuples and sequences can be described, but also additional constructs such as free types and bindings. In addition, Z has a rich structuring mechanism-its schema calculus. Z is frequently used to specify the operations of a system on its state, and has a refinement calculus and formal semantics. This article introduces ZCCS, a version of value-passing CCS in which the data language used to describe the action/agent parameters and conditions is Z. We introduce the style and syntax of ZCCS and illuminate this with a small example. In addition, we present an operational semantics for ZCCS.

Keywords

Boolean functions; formal specification; refinement calculus; specification languages; Boolean constants; Z; ZCCS; agent language; data language; formal specification language; operational semantics; sequences; sets; tuples; value-passing CCS; Calculus; Carbon capture and storage; Computer science; Concrete; Data engineering; Input variables; Mathematics; Specification languages; Systems engineering and theory; Vocabulary;

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

Filename

630434