A Rewriting Semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis

Michael Katelman; José Meseguer

doi:10.1016/j.entcs.2007.06.007

A Rewriting Semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis

Research output: Contribution to journal › Article › peer-review

Abstract

We present a rewriting logic semantics in Maude of the ABEL hardware description language. Based on this semantics, and on Maude's underlying LTL model checker, we propose a scalable formal analysis framework and tool for hardware/software co-design. The analysis method is based on trace checking of finite system behaviors against LTL temporal logic formulas. The formal properties of the hardware, the embedded software, and the interactions between both can all be analyzed this way. We present two case studies illustrating our method and tool.

Original language	English (US)
Pages (from-to)	47-60
Number of pages	14
Journal	Electronic Notes in Theoretical Computer Science
Volume	176
Issue number	4
DOIs	https://doi.org/10.1016/j.entcs.2007.06.007
State	Published - Jul 28 2007

Keywords

Maude
co-design
co-verification
hardware description languages
program semantics
rewriting logic

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Online availability

10.1016/j.entcs.2007.06.007

Library availability

Discover UIUC Full Text

Cite this

@article{149d3fbdde354a8fa9446d70d91e15fc,

title = "A Rewriting Semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis",

abstract = "We present a rewriting logic semantics in Maude of the ABEL hardware description language. Based on this semantics, and on Maude's underlying LTL model checker, we propose a scalable formal analysis framework and tool for hardware/software co-design. The analysis method is based on trace checking of finite system behaviors against LTL temporal logic formulas. The formal properties of the hardware, the embedded software, and the interactions between both can all be analyzed this way. We present two case studies illustrating our method and tool.",

keywords = "Maude, co-design, co-verification, hardware description languages, program semantics, rewriting logic",

author = "Michael Katelman and Jos{\'e} Meseguer",

note = "Funding Information: We thank the referees for their detailed comments on a previous version that have helped us improve the presentation. In addition, we thank Sean Keller for reviewing a draft of the paper, and Andrew Colombi for a version of the graphics program. This research has been supported in part by ONR grant N00014–02-1-0715.",

year = "2007",

month = jul,

day = "28",

doi = "10.1016/j.entcs.2007.06.007",

language = "English (US)",

volume = "176",

pages = "47--60",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

number = "4",

}

TY - JOUR

T1 - A Rewriting Semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis

AU - Katelman, Michael

AU - Meseguer, José

N1 - Funding Information: We thank the referees for their detailed comments on a previous version that have helped us improve the presentation. In addition, we thank Sean Keller for reviewing a draft of the paper, and Andrew Colombi for a version of the graphics program. This research has been supported in part by ONR grant N00014–02-1-0715.

PY - 2007/7/28

Y1 - 2007/7/28

N2 - We present a rewriting logic semantics in Maude of the ABEL hardware description language. Based on this semantics, and on Maude's underlying LTL model checker, we propose a scalable formal analysis framework and tool for hardware/software co-design. The analysis method is based on trace checking of finite system behaviors against LTL temporal logic formulas. The formal properties of the hardware, the embedded software, and the interactions between both can all be analyzed this way. We present two case studies illustrating our method and tool.

AB - We present a rewriting logic semantics in Maude of the ABEL hardware description language. Based on this semantics, and on Maude's underlying LTL model checker, we propose a scalable formal analysis framework and tool for hardware/software co-design. The analysis method is based on trace checking of finite system behaviors against LTL temporal logic formulas. The formal properties of the hardware, the embedded software, and the interactions between both can all be analyzed this way. We present two case studies illustrating our method and tool.

KW - Maude

KW - co-design

KW - co-verification

KW - hardware description languages

KW - program semantics

KW - rewriting logic

UR - http://www.scopus.com/inward/record.url?scp=34447629040&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=34447629040&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2007.06.007

DO - 10.1016/j.entcs.2007.06.007

M3 - Article

AN - SCOPUS:34447629040

SN - 1571-0661

VL - 176

SP - 47

EP - 60

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 4

ER -

A Rewriting Semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis

Abstract

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this