Model checking with fairness assumptions using PAT

Recent development on distributed systems has shown that a variety of fairness constraints (some of which are only recently defined) play vital roles in designing self-stabilizing population protocols. Existing model checkers are deficient in verifying the systems as only limited kinds of fairness a...

Full description

Saved in:
Bibliographic Details
Published in:Frontiers of Computer Science 2014-02, Vol.8 (1), p.1-16
Main Authors: SI, Yuanjie, SUN, Jun, LIU, Yang, DONG, Jin Song, PANG, Jun, ZHANG, Shao Jie, YANG, Xiaohu
Format: Article
Language:English
Subjects:
Computer networks
Computer Science
Empirical analysis
fairness
formal methods
model checking
PAT
Research Article
Toolkits
Verification
verification tool
公平性
分布式系统
基准系统
模型检查
模型检测
运作体系
验证系统
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Recent development on distributed systems has shown that a variety of fairness constraints (some of which are only recently defined) play vital roles in designing self-stabilizing population protocols. Existing model checkers are deficient in verifying the systems as only limited kinds of fairness are supported with limited verification efficiency. In this work, we support model checking of distributed systems in the toolkit PAT (process analysis toolkit), with a variety of fairness constraints (e.g., process-level weak/strong fairness, event-level weak/strong fairness, strong global fairness). It performs on-the-fly verification against linear temporal properties. We show through empirical evaluation (on recent population protocols as well as benchmark systems) that PAT has advantage in model checking with fairness. Previously unknown bugs have been revealed against systems which are designed to function only with strong global fairness.
ISSN:2095-2228
2095-2236
DOI:10.1007/s11704-013-3091-5