A model for the protocol design of back-end storage networks

This work presents a formal design for the system protocols of back-end storage networks. Such design relies on predicate-transition nets (PrT-nets). These nets actually represent an extension of Petri nets and can provide reasonable means for precise modeling of complex systems. The given model has demonstrated that by using PrT-nets the protocols of back-end networks can be constructed and interpreted in a natural manner. In that model we employed mainly two types of tokens, one to simulate user programs and requests and the other to express synchronization and control. To build up the model we used a modular approach. Each module is represented by a phase in the protocol net so that the complete design can eventually realize the required system specifications. Also, an insight into the design is emphasized and the validation of the protocol is pointed out. Accordingly, a well-behaved system is obtained so that the shared data is free from inconsistency, deadlocks, and residual signals.