Process-Based Design Verification for Systems Involving Shared Resources

In system synthesis, one need to derive from a given set of processes a system design which is correct in the sense that the system is well-behaved (that is, live, bounded and reversible). This is especially important for shared-resource systems, in which erroneous situations such as deadlock and capacity overflow are easily induced because of the sharing of common resources among different asynchronous processes. In this paper, a process-based method is proposed for verifying the well-behavedness of a system. The method can be performed at an early stage of system development, where functional requirements are elicited and interpreted as processes. By specifying the given processes as augmented marked graphs, we perform stepwise synthesis of these augmented marked graphs through the fusion of their common places which denote the shared resources. Liveness, boundedness and reversibility can be effectively checked by making use of the special properties of augmented marked graphs