Translation of a fragment of AsmL specification language to Higher Order Logic
Rostislav E. Yavorsky · 2003
The Abstract State Machine Language (AsmL) is an executable specification language developed at Microsoft Research. It is based on the notion of Abstract State Machine (ASM, formerly known as evolving algebra). According to the main ASM thesis, any algorithm at any level of abstraction can be faithfully simulated by an appropriate ASM. This specification method has been used for the description of the semantics of programming languages, communication protocols, distributed agorithms etc. [1, 2, 3]. AsmL is a powerful industrial strength language; it is a full member of the .NET family of languages. It is accompanied by tools for model based test generation and runtime verification [1]. On the other hand, tools for static analysis of the AsmL specifications by means of theorem provers have not been developed yet. Our main goal is to define a fragment of AsmL that can be formalized in a theorem prover without much overhead, yet is rich enough to deal with reasonable properties of models. The algorithm for the AsmL to HOL translation described in this paper is implemented in a tool, which is intended to be part of integrated verification environment. This work is based on earlier research on verification of ASM like models in theorem provers (see [4, 5, 6]). In section 1 we describe our technique using the example of a railroad crossing controller. In section 2, a general computation model is described that provides the theoretical background for the translation of a fragment of AsmL into the language of higher order logic. Then, in section 3, the corresponding fragment of AsmL and normal form of specification are outlined. In section 4, we describe the translation of this fragment of AsmL into the language of HOL theorem prover (HOL 4 Kananaskis [7]). Section 5 provides some useful HOL tactics for the verification of specifications.