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 )