In this paper we present an abstract model of process semantics, Abstract Trace Semantics, which is built on top of an abstract interpretation for LOTOS.We use it as a modle ofr an abstract interpretation of a linear time temporal logis. Both Abstract Trace Semantics andthe abstract interpretation of the satisfiablity relation are proven correct w.r.t. their ocncrete counterparts. The main advnatage of the proposed approach is that it makes automatic model checkig applciable also to full value pasing process algebras. Currently, modle checking is applied only to porcess algebraic specifications where only synchronization is supported. BY means of abstract interpretation we can reduce the infinite branching of labeled transition systems, which si due to infinite data types, to finite branching. In this way we can completely automate 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.
展开▼
