engleski

Verification of mutual exclusion algorithms with SMV system

Mutual exclusion algorithms can exhibit intricate behavior for which correctness can be hard to establish. We demonstrate automatic verification of five algorithms by symbolic model checking. We used SMV tool which enables property specification in computation tree logic and allow us to impose fairness constraints on a model. For each of the algorithm we verify safety, liveness, non-blocking and no strict ordering properties.

formal verification ; model checking ; mutual exclusion algorithms ; CTL ; SMV

nije evidentirano