Login | Register

On the Transformation of SystemC to AsmL Using Abstract Interpretation

Title:

On the Transformation of SystemC to AsmL Using Abstract Interpretation

Habibi, Ali and Tahar, Sofiène (2005) On the Transformation of SystemC to AsmL Using Abstract Interpretation. Electronic Notes in Theoretical Computer Science, 131 . pp. 39-49. ISSN 15710661

[thumbnail of ENTCS-2005.pdf]
Preview
Text (application/pdf)
ENTCS-2005.pdf - Accepted Version
136kB

Official URL: http://dx.doi.org/10.1016/j.entcs.2005.01.021

Abstract

SystemC is among a group of system level design languages proposed to raise the abstraction level for embedded system design and verification. A straight and sound verification by model checking or theorem proving of SystemC designs is, however, infeasible given the object-oriented nature of this library and the complexity of its simulation environment. We illustrated, in a previous work, the feasibility and success of performing model checking and assertions monitors generation of SystemC using a variant of Abstract State Machines (ASM) languages (AsmL). In this paper, we establish the soundness of our approach by proving the correctness of the transformation from SystemC to AsmL.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Refereed:Yes
Authors:Habibi, Ali and Tahar, Sofiène
Journal or Publication:Electronic Notes in Theoretical Computer Science
Date:2005
Digital Object Identifier (DOI):10.1016/j.entcs.2005.01.021
Keywords:abstract interpretation; formal verification; systemc
ID Code:977381
Deposited By: Danielle Dennie
Deposited On:14 Jun 2013 15:43
Last Modified:18 Jan 2018 17:44

References:

[1]
Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]

[2]
Patrick Cousot , Radhia Cousot, Systematic design of program transformation frameworks by abstract interpretation, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.178-190, January 16-18, 2002, Portland, Oregon [doi>10.1145/503272.503290]

[3]
Yuri Gurevich, Evolving algebras 1993: Lipari guide, Specification and validation methods, Oxford University Press, Inc., New York, NY, 1995

[4]
Ali Habibi , Sofiene Tahar, Design for Verification of SystemC Transaction Level Models, Proceedings of the conference on Design, Automation and Test in Europe, p.560-565, March 07-11, 2005 [doi>10.1109/DATE.2005.112]

[5]
A. Habibi and S. Tahar. AsmL fixpoint semantics. Technical report, Department of ECE, Concordia University, December 2004

[6]
A. Habibi and S. Tahar. SystemC fixpoint semantics. Technical report, Department of ECE, Concordia University, December 2004

[7]
F. Logozzo. Analyse Statique Modulaire de Langages à Objets. PhD thesis, Ecole Polytechnique, Paris, France, June 2004

[8]
Microsoft Corp. AsmL for Microsoft .NET framework, 2004

[9]
Müller, W., Ruf, J. and Rosenstiel, W., SystemC Methodologies and Applications. 2003. Kluwe Academic Pub.

[10]
Peter D. Mosses, Denotational semantics, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991

[11]
http://www.systemc.org

[12]
K. Oumalou, A. Habibi, and S. Tahar. Design for verification of a PCI bus in SystemC. In Symposium on System-on-Chip, Finland, November 2004

[13]
Ashraf Salem, Formal Semantics of Synchronous SystemC, Proceedings of the conference on Design, Automation and Test in Europe, p.10376, March 03-07, 2003
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top