A formal method for synthesising components of shared resource systems

Shared resource systems are characterised by the competition of shared resources among different system components. In the process of synthesising system components into a single integrated whole, it is essentially required that the integrated system should be free from erroneous situations such as deadlock and capacity overflow, which are easily induced by the competition of shared resources. In this paper, a Petri-net-based method is proposed for the synthesis process. The method begins with specifying the system components as augmented marked graphs. They are then synthesised into an integrated system by fusing the common places of shared resources. As the integrated system is structurally an augmented marked graph, the design correctness in terms of liveness, boundedness and reversibility can be effectively analysed by making use of the desirable properties of augmented marked graphs.