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

Research output: Chapter in book / Conference proceeding › Conference article published in proceeding or book › Academic research › peer-review

8 Citations (Scopus)

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
Publication status	Published - 20 Apr 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

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

ASJC Scopus subject areas

Computer Science Applications
Computer Graphics and Computer-Aided Design
Electrical and Electronic Engineering

More information

10.1109/ASPDAC.2009.4796564

Cite this

@inproceedings{c845b39faab845f4b9ca8d9133fea84e,

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",

month = apr,

day = "20",

doi = "10.1109/ASPDAC.2009.4796564",

language = "English",

isbn = "9781424427482",

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, 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.

Research output: Chapter in book / Conference proceeding › Conference article published in proceeding or book › Academic research › 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/4/20

Y1 - 2009/4/20

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 - http://www.scopus.com/inward/record.url?scp=64549132914&partnerID=8YFLogxK

U2 - 10.1109/ASPDAC.2009.4796564

DO - 10.1109/ASPDAC.2009.4796564

M3 - Conference article published in proceeding or book

SN - 9781424427482

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

Conference

ASJC Scopus subject areas

More information

Other files and links

Fingerprint

Cite this