Composing Specifications Using Communication | Zendy

Helen Treharne | Zendy; Steve Schneider | Zendy; Marchia Bramble | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Composing Specifications Using Communication

Author(s) -

Helen Treharne,

Steve Schneider,

Marchia Bramble

Publication year - 2003

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

DOI - 10.1007/3-540-44880-2_5

Subject(s) - liveness , computer science , focus (optics) , process calculus , process (computing) , communicating sequential processes , interface (matter) , distributed computing , programming language , semantics (computer science) , operating system , operational semantics , physics , bubble , maximum bubble pressure method , optics

This paper develops a case study using the process algebra CSP to enable controlled interaction between B machines. This illustrates how B machines are essential components within a combined communicating system. The development steps used to build the case study are new: they are applications of theoretical results which allow us to focus on the external interface of a combined communicating system, compositionally verify it, and show that it is a refinement of a more abstract specification described in CSP. This allows safety and liveness properties to be established for combinations of communicating B machines

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research