Modeling and Validating Broadcasting-Free Concurrent Systems

We consider the systems composed of a finite set of asynchronously cooperating subsystems. The subsystems may communicate with each other by sending or receiving synchronization messages. Each particular synchronization message has a unique sender and a unique receiver. Such set of subsystems is called “broadcasting-free”. We show how to generate a global description of the system from the descriptions of its subsystems provided they cooperate by means of the synchronization mechanism called rendez-vous. We show also how to validate the system behaviours. The susbystems and the whole system will be modelled by abstract machines defined in the paper.