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

Michael Katelman, José Meseguer

Research output: Contribution to journalArticle

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 languageEnglish (US)
Pages (from-to)47-60
Number of pages14
JournalElectronic Notes in Theoretical Computer Science
Volume176
Issue number4
DOIs
StatePublished - 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)

Fingerprint Dive into the research topics of 'A Rewriting Semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis'. Together they form a unique fingerprint.

  • Cite this