Segregation with Communication

摘要

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 called multi-promotion) and a proof that unconstrained multi-promotion is a sufficient condition to ensure segregation.