We have developed a general definition of segregation in the context of Z system specifications. This definition is general enough to allow multi-way communications between otherwise segregated parties along defined channels. We have an abstract definition of segregation in terms of the traces allowed by systems, a concrete style of specification to ensure segregation (a generalisation of promotion that we call multi-promotion ) and a proof that unconstrained multi-promotion is a sufficient condition to ensure segregation.
More on the
Full paper : PDF 248K
@inproceedings(SS-ZB2000a,
author = "David Cooper and Susan Stepney",
title = "Segregation with Communication",
pages = "451--470",
crossref = "ZB-00"
)
@proceedings(ZB2000,
title = "ZB2000: First International Conference of B and Z Users,
York, UK, August 2000",
booktitle = "ZB2000: First International Conference of B and Z Users,
York, UK, August 2000",
editor = "Jonathan P. Bowen and Steve Dunne and Andy Galloway and Steve King",
series = "LNCS",
volume = 1878,
publisher = "Springer",
year = 2000
)