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 Jitsion 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.
K.S. Cheung K.O. Chow
Hong Kong Baptist University City University of Hong Kong
国际会议
2006 Asia-Pacific Services Computing Conference(IEEE亚太地区服务计算会议)
广州
英文
99-106
2006-12-12（万方平台首次上网日期，不代表论文的发表时间）