System-on-chip Verification project

Hardware verification group

Technical Report

AsmL is a novel executable specification language based on the theory of Abstract State Machines (ASMs). It represents one of the most powerful practical engines to write and execute ASMs. In this report, we present a proven complete small-step trace-based operational semantics of the main parts of AsmL. Such a semantics provides precise and non ambiguous definitions of AsmL. It is very useful to guarantee a unique implementation of the language and interpretation of its behavior. Furthermore, they can be used in conducting formal proofs for sound abstractions or even to construct syntactical transformers to other languages.

AsmL Semantics in Fixpoint

A. Habibi and S. Tahar

Date: December 2004

 Download PDF file: (PDF file)

 Send comments and suggestions to: habibi@ece.concordia.ca