Temporal Deductive Verification of Basic ASM Models
Main Article Content
Abstract
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 we 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. In particular, we base 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-consumer system formalized in terms of basic ASMs.
Article Details
How to Cite
Daho, H. E.-H., & Benhamamouch, D. (2010). Temporal Deductive Verification of Basic ASM Models. INFOCOMP Journal of Computer Science, 9(1), 12–21. Retrieved from https://infocomp.dcc.ufla.br/index.php/infocomp/article/view/286
Section
Articles
Upon receipt of accepted manuscripts, authors will be invited to complete a copyright license to publish the paper. At least the corresponding author must send the copyright form signed for publication. It is a condition of publication that authors grant an exclusive licence to the the INFOCOMP Journal of Computer Science. This ensures that requests from third parties to reproduce articles are handled efficiently and consistently and will also allow the article to be as widely disseminated as possible. In assigning the copyright license, authors may use their own material in other publications and ensure that the INFOCOMP Journal of Computer Science is acknowledged as the original publication place.