Please use this identifier to cite or link to this item: https://doi.org/10.1007/s11704-013-3091-5
Title: Model checking with fairness assumptions using PAT
Authors: Si, Y.
Sun, J.
Liu, Y.
Dong, J.S. 
Pang, J.
Zhang, S.J.
Yang, X.
Keywords: fairness
formal methods
model checking
PAT
verification tool
Issue Date: Feb-2014
Citation: Si, Y., Sun, J., Liu, Y., Dong, J.S., Pang, J., Zhang, S.J., Yang, X. (2014-02). Model checking with fairness assumptions using PAT. Frontiers of Computer Science 8 (1) : 1-16. ScholarBank@NUS Repository. https://doi.org/10.1007/s11704-013-3091-5
Abstract: 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. © 2014 Higher Education Press and Springer-Verlag Berlin Heidelberg.
Source Title: Frontiers of Computer Science
URI: http://scholarbank.nus.edu.sg/handle/10635/77888
ISSN: 20952228
DOI: 10.1007/s11704-013-3091-5
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

11
checked on Sep 16, 2018

WEB OF SCIENCETM
Citations

9
checked on Aug 29, 2018

Page view(s)

73
checked on Jul 27, 2018

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.