Temporal logics verification of lotos specifications using abstract interpretation

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.