Date Added: Mar 2010
Abstract State Machines (ASMs, for short) provide a practical new computational model which has been applied in the area of software engineering for systems design and analysis. However, reasoning about ASM models occurs, not within a formal deductive system, but basically in the classical informal proofs style of mathematics. Several formal verification approaches for proving correctness of ASM models have been investigated. In this paper, the authors consider the use of the TLA + logic for the deductive verification of a certain class of ASMs, namely basic ASMs which have successfully been applied in describing the dynamic behavior of systems at various levels of abstraction.