研究模型验证中的公平性问题,全面定义了包括进程层面(process-level)的强/弱公平、事件层面(eventlevel)的强/弱公平以及全局强公平性(strong global fairness)等,把这些公平性条件集成进了一个模型验证工具PAT.该工具支持以on-the-fl...研究模型验证中的公平性问题,全面定义了包括进程层面(process-level)的强/弱公平、事件层面(eventlevel)的强/弱公平以及全局强公平性(strong global fairness)等,把这些公平性条件集成进了一个模型验证工具PAT.该工具支持以on-the-fly的方式对线性时序逻辑性质进行验证.通过对多个基准模型进行实验,该工具在基于公平条件的模型验证中表现出良好的性能.展开更多
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 mod...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 fair- ness 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 prop- erties. We show through empirical evaluation （on recent pop- ulation protocols as well as benchmark systems） that PAT has advantage in model checking with fairness. Previously un- known bugs have been revealed against systems which are designed to function only with strong global fairness.展开更多
文摘研究模型验证中的公平性问题,全面定义了包括进程层面(process-level)的强/弱公平、事件层面(eventlevel)的强/弱公平以及全局强公平性(strong global fairness)等,把这些公平性条件集成进了一个模型验证工具PAT.该工具支持以on-the-fly的方式对线性时序逻辑性质进行验证.通过对多个基准模型进行实验,该工具在基于公平条件的模型验证中表现出良好的性能.
文摘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 fair- ness 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 prop- erties. We show through empirical evaluation （on recent pop- ulation protocols as well as benchmark systems） that PAT has advantage in model checking with fairness. Previously un- known bugs have been revealed against systems which are designed to function only with strong global fairness.
