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