Simulation-Based Invariant Verification Technique for the OTS/CafeOBJ Method

Simulation-Based Invariant Verification Technique for the OTS/CafeOBJ Method

We demonstrate the power of the simulation-based invariant verification technique through two case studies in which it is formally verified that two mutual exclusion protocols, MCS protocol and Anderson protocol, enjoy the mutual exclusion property by the simulation-based invariant verification tech...

Full description

Bibliographic Details
Main Authors: Duong Dinh Tran, Dang Duy Bui, Kazuhiro Ogata
Format: Article
Language:English
Published: IEEE 2021-01-01
Series:IEEE Access
Subjects:
Algebraic specification language
CafeOBJ
invariant properties
proof scores
mathematical induction
refinement
Online Access:https://ieeexplore.ieee.org/document/9466495/

Internet

https://ieeexplore.ieee.org/document/9466495/

Similar Items