RI UFLA (Universidade Federal de Lavras) >
Revistas UFLA >
Infocomp >

Please use this identifier to cite or link to this item: http://repositorio.ufla.br/jspui/handle/1/9907

Title: Temporal deductive verification of basic ASM models
???metadata.dc.creator???: Daho, Hocine El-Habib
Benhamamouch, Djillali
Keywords: Abstract State Machines (ASMs)
Temporal Logic of Actions (TLA)
Deductive Verification
Máquinas de estados abstratos
Lógica temporal de ações
Verificação dedutivo
Publisher: Editora da UFLA
???metadata.dc.date???: 1-Mar-2010
Citation: DAHO, H. E.-H.; BENHAMAMOUCH, D. Temporal deductive verification of basic ASM models. INFOCOMP: Journal of Computer Science, Lavras, v. 9, n. 1, p. 12-21, Mar. 2010.
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.
Other Identifiers: http://www.dcc.ufla.br/infocomp/index.php/INFOCOMP/article/view/286
???metadata.dc.language???: eng
Appears in Collections:Infocomp

Files in This Item:

There are no files associated with this item.

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

View Statistics


DSpace Software Copyright © 2002-2010  Duraspace - Feedback