TY - GEN
T1 - Process-based design verification for systems involving shared resources
AU - Cheung, K. S.
AU - Chow, K. O.
PY - 2006
Y1 - 2006
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=39749142597&partnerID=8YFLogxK
U2 - 10.1109/APSCC.2006.79
DO - 10.1109/APSCC.2006.79
M3 - Conference contribution
AN - SCOPUS:39749142597
SN - 0769527515
SN - 9780769527512
T3 - Proceedings of 2006 IEEE Asia-Pacific Conference on Services Computing, APSCC
SP - 99
EP - 106
BT - Proceedings of 2006 IEEE Asia-Pacific Conference on Services Computing, APSCC
T2 - 2006 IEEE Asia-Pacific Conference on Services Computing, APSCC
Y2 - 12 December 2006 through 15 December 2006
ER -