Temporal Deductive Verification of Basic ASM Models

Abstract State Machines (ASMs, for short) provide a practical new computational modelwhich 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 classicalinformal proofs style of mathematics. Several formal verification approaches for proving correctnessof ASM models have been investigated. In this paper we consider the use of the TLA+logic for thedeductive verification of a certain class of ASMs, namely basic ASMs which have successfully beenapplied in describing the dynamic behavior of systems at various levels of abstraction. In particular, webase our verification purpose on a translation of basic ASMs to the Temporal Logic of Actions (TLA) used as a formal basis to formally specify and reason about temporal behaviors of basic ASM models. The temporal deductive approach is illustrated by the formal correctness proof of a producer-consumersystem formalized in terms of basic ASMs