Specification and Refinement using a Heterogeneous Notation for Concurrency and Communication

Richard F. Paige

Specification and Refinement using a Heterogeneous Notation for Concurrency and Communication

Computer Science

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

Abstract

It is shown how to combine the Z formal specification notation with a predicative
notation so as to be able to specify and reason about concurrency and communication.
The integration is carried out so as to alleviate some of the limitations
noted with previous integration approaches, such as the inability to use Z proof
rules and tools with the integrated notation. In the process, it is demonstrated that
it is not necessary to combine Z with a very different behavioural formalism in
order to reason about concurrency.

Original language	Undefined/Unknown
Pages	353-372
Publication status	Published - 1999

Access to Document

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.3986

Cite this

@conference{70f9f898ff0b4dca91ef4ae2ae46a537,

title = "Specification and Refinement using a Heterogeneous Notation for Concurrency and Communication",

abstract = "It is shown how to combine the Z formal specification notation with a predicativenotation so as to be able to specify and reason about concurrency and communication.The integration is carried out so as to alleviate some of the limitationsnoted with previous integration approaches, such as the inability to use Z proofrules and tools with the integrated notation. In the process, it is demonstrated thatit is not necessary to combine Z with a very different behavioural formalism inorder to reason about concurrency.",

author = "Paige, {Richard F.}",

year = "1999",

language = "Undefined/Unknown",

pages = "353--372",

}

TY - CONF

T1 - Specification and Refinement using a Heterogeneous Notation for Concurrency and Communication

AU - Paige, Richard F.

PY - 1999

Y1 - 1999

N2 - It is shown how to combine the Z formal specification notation with a predicativenotation so as to be able to specify and reason about concurrency and communication.The integration is carried out so as to alleviate some of the limitationsnoted with previous integration approaches, such as the inability to use Z proofrules and tools with the integrated notation. In the process, it is demonstrated thatit is not necessary to combine Z with a very different behavioural formalism inorder to reason about concurrency.

AB - It is shown how to combine the Z formal specification notation with a predicativenotation so as to be able to specify and reason about concurrency and communication.The integration is carried out so as to alleviate some of the limitationsnoted with previous integration approaches, such as the inability to use Z proofrules and tools with the integrated notation. In the process, it is demonstrated thatit is not necessary to combine Z with a very different behavioural formalism inorder to reason about concurrency.

M3 - Paper

SP - 353

EP - 372

ER -