Istituto di Scienza e Tecnologie dell'Informazione     
Fantechi A., Gnesi S., Latella D. Temporal logics verification of lotos specifications using abstract interpretation. Internal note CNUCE-B4-94-019, 1994.
In [6, 5] a technique for the automatic derivation of an Abstract Interpretation Domain for (the Abstract Data Types part) of LOTOS specifications has been proposed. In this paper we present an abstract model of process semantics, Abstract Trace Semantics, which is built on top of the above mentioned Abstract Interpretation Domain and which we use as a model for an abstract interpretation of a linear time temperal logics. Both Abstract Trace Semantics and the abstract interpretation of the satisfiability relation are proven correct w.r.t. their concrete counterparts. The main advantage of the proposed approach stems from the fact that it allows to completely automatize the verification that a formula is satisfied by a process in the abstract domain. When the formula is satisfied by the process in the abstract domain, then the correctness theorem guarantees that indeed the formula holds for the process
Subject Specifications

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional