Improving Scalability of Model-Checking for Minimizing Buffer Requirements of Synchronous Dataflow Graphs

Nan Guan; Zonghua Gu; Wang Yi; Ge Yu

doi:10.1109/ASPDAC.2009.4796564

Improving Scalability of Model-Checking for Minimizing Buffer Requirements of Synchronous Dataflow Graphs

Nan Guan^*
, Zonghua Gu
, Wang Yi
, Ge Yu

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

8 Scopus citations

Abstract

Synchronous Dataflow (SDF) is a well-known model of computation for dataflow-oriented applications such as embedded systems for signal processing and multimedia. It is important to minimize the buffer size requirements of applications generated from SDF graphs, since memory space is often a scarce resource in these systems due to cost or power consumption constraints. Some authors have proposed to use model-checking for finding the minimum buffer size requirements, but the scalability of model-checking is limited by state space explosion. In this paper, we present several techniques for reducing state space size and improving scalability of model-checking by exploiting problem-specific properties of SDF graphs.

Original language	English
Title of host publication	Proceedings of the ASP-DAC 2009
Subtitle of host publication	Asia and South Pacific Design Automation Conference 2009
Pages	715-720
Number of pages	6
DOIs	https://doi.org/10.1109/ASPDAC.2009.4796564
State	Published - 2009
Externally published	Yes
Event	Asia and South Pacific Design Automation Conference 2009, ASP-DAC 2009 - Yokohama, Japan Duration: 19 Jan 2009 → 22 Jan 2009

Publication series

Name	Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC

Conference

Conference	Asia and South Pacific Design Automation Conference 2009, ASP-DAC 2009
Country/Territory	Japan
City	Yokohama
Period	19/01/09 → 22/01/09

Access to Document

10.1109/ASPDAC.2009.4796564

Cite this

Guan, N., Gu, Z., Yi, W., & Yu, G. (2009). Improving Scalability of Model-Checking for Minimizing Buffer Requirements of Synchronous Dataflow Graphs. In Proceedings of the ASP-DAC 2009: Asia and South Pacific Design Automation Conference 2009 (pp. 715-720). Article 4796564 (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC). https://doi.org/10.1109/ASPDAC.2009.4796564

@inproceedings{47c3a5e3b84146629004a582b5a98326,

title = "Improving Scalability of Model-Checking for Minimizing Buffer Requirements of Synchronous Dataflow Graphs",

abstract = "Synchronous Dataflow (SDF) is a well-known model of computation for dataflow-oriented applications such as embedded systems for signal processing and multimedia. It is important to minimize the buffer size requirements of applications generated from SDF graphs, since memory space is often a scarce resource in these systems due to cost or power consumption constraints. Some authors have proposed to use model-checking for finding the minimum buffer size requirements, but the scalability of model-checking is limited by state space explosion. In this paper, we present several techniques for reducing state space size and improving scalability of model-checking by exploiting problem-specific properties of SDF graphs.",

author = "Nan Guan and Zonghua Gu and Wang Yi and Ge Yu",

year = "2009",

doi = "10.1109/ASPDAC.2009.4796564",

language = "英语",

isbn = "9781424427482",

series = "Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC",

pages = "715--720",

booktitle = "Proceedings of the ASP-DAC 2009",

note = "Asia and South Pacific Design Automation Conference 2009, ASP-DAC 2009 ; Conference date: 19-01-2009 Through 22-01-2009",

}

Guan, N, Gu, Z, Yi, W & Yu, G 2009, Improving Scalability of Model-Checking for Minimizing Buffer Requirements of Synchronous Dataflow Graphs. in Proceedings of the ASP-DAC 2009: Asia and South Pacific Design Automation Conference 2009., 4796564, Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC, pp. 715-720, Asia and South Pacific Design Automation Conference 2009, ASP-DAC 2009, Yokohama, Japan, 19/01/09. https://doi.org/10.1109/ASPDAC.2009.4796564

Improving Scalability of Model-Checking for Minimizing Buffer Requirements of Synchronous Dataflow Graphs. / Guan, Nan; Gu, Zonghua; Yi, Wang et al.
Proceedings of the ASP-DAC 2009: Asia and South Pacific Design Automation Conference 2009. 2009. p. 715-720 4796564 (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Improving Scalability of Model-Checking for Minimizing Buffer Requirements of Synchronous Dataflow Graphs

AU - Guan, Nan

AU - Gu, Zonghua

AU - Yi, Wang

AU - Yu, Ge

PY - 2009

Y1 - 2009

N2 - Synchronous Dataflow (SDF) is a well-known model of computation for dataflow-oriented applications such as embedded systems for signal processing and multimedia. It is important to minimize the buffer size requirements of applications generated from SDF graphs, since memory space is often a scarce resource in these systems due to cost or power consumption constraints. Some authors have proposed to use model-checking for finding the minimum buffer size requirements, but the scalability of model-checking is limited by state space explosion. In this paper, we present several techniques for reducing state space size and improving scalability of model-checking by exploiting problem-specific properties of SDF graphs.

AB - Synchronous Dataflow (SDF) is a well-known model of computation for dataflow-oriented applications such as embedded systems for signal processing and multimedia. It is important to minimize the buffer size requirements of applications generated from SDF graphs, since memory space is often a scarce resource in these systems due to cost or power consumption constraints. Some authors have proposed to use model-checking for finding the minimum buffer size requirements, but the scalability of model-checking is limited by state space explosion. In this paper, we present several techniques for reducing state space size and improving scalability of model-checking by exploiting problem-specific properties of SDF graphs.

UR - https://www.scopus.com/pages/publications/64549132914

U2 - 10.1109/ASPDAC.2009.4796564

DO - 10.1109/ASPDAC.2009.4796564

M3 - 会议稿件

AN - SCOPUS:64549132914

SN - 9781424427482

T3 - Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC

SP - 715

EP - 720

BT - Proceedings of the ASP-DAC 2009

T2 - Asia and South Pacific Design Automation Conference 2009, ASP-DAC 2009

Y2 - 19 January 2009 through 22 January 2009

ER -

Improving Scalability of Model-Checking for Minimizing Buffer Requirements of Synchronous Dataflow Graphs

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this