Process-based design verification for systems involving shared resources

K. S. Cheung, K. O. Chow

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationProceedings of 2006 IEEE Asia-Pacific Conference on Services Computing, APSCC
Pages99-106
Number of pages8
DOIs
Publication statusPublished - 2006
Externally publishedYes
Event2006 IEEE Asia-Pacific Conference on Services Computing, APSCC - Guangzhou, Guangdong, China
Duration: 12 Dec 200615 Dec 2006

Publication series

NameProceedings of 2006 IEEE Asia-Pacific Conference on Services Computing, APSCC

Conference

Conference2006 IEEE Asia-Pacific Conference on Services Computing, APSCC
Country/TerritoryChina
CityGuangzhou, Guangdong
Period12/12/0615/12/06

Fingerprint

Dive into the research topics of 'Process-based design verification for systems involving shared resources'. Together they form a unique fingerprint.

Cite this