FOCOVE: Formal Concurrency Verification Environment for Complex Systems
Djamel Eddine Saïdouni, Adel Benamira, Nabil Belala, Farid Arfi, Hichem Arioui, Rochdi Merzouki, Hadj Ahmed Abbassi · AIP conference proceedings · 2008
This paper presents a tool to exploit a true concurrency model, namely the Maximality‐based Labeled Transitions Systems. We show the use of this model in model checking technique. Three techniques are implemented in order to solve the state space combinatorial explosion problem: the reduction modulo α‐equivalence relation, the joint use of covering steps and maximality semantics, and the maximality‐based symbolic representation.