电子学报 ›› 2015, Vol. 43 ›› Issue (11): 2298-2304.DOI: 10.3969/j.issn.0372-2112.2015.11.024

• 学术论文 • 上一篇    下一篇

基于可满足性计数的(≠,=)约束工作流鲁棒性验证

翟治年1, 王刚2, 郑志军1, 彭艳斌1, 潘志刚1, 王中鹏1   

  1. 1. 浙江科技学院信息与电子工程学院, 浙江 杭州 310023;
    2. 中国核电工程有限公司河北分公司民用工程研究设计所, 河北 石家庄 050011
  • 收稿日期:2014-10-13 修回日期:2015-07-06 出版日期:2015-11-25
    • 通讯作者:
    • 王中鹏
    • 作者简介:
    • 翟治年 男,1977年5月生,河北张家口人.2012年毕业于华南理工大学计算机应用技术专业,获工学博士学位.现为浙江科技学院信息与电子工程学院讲师,主要从事信息安全与访问控制方面的研究.E-mail:zhaizhinian@gmail.com
    • 基金资助:
    • 国家自然科学基金 (No.51376162); 浙江省自然科学基金 (No.LY13F050005)

Verification of(≠,=)Constrained Workflow Robustness Based on Satisfiability Counting

ZHAI Zhi-nian1, WANG Gang2, ZHENG Zhi-jun1, PENG Yan-bing1, PAN Zhi-gang1, WANG Zhong-peng1   

  1. 1. School of Information and Electronics Engineering, Zhejiang University of Science and Technology, Hangzhou, Zhejiang 310023, China;
    2. Civil Engineering Research & Design Institute, China Nuclear Power Engineering Limited Corporation Hebei Branch, Shijiazhuang, Hebei 050011, China
  • Received:2014-10-13 Revised:2015-07-06 Online:2015-11-25 Published:2015-11-25

摘要:

工作流将业务过程分解为有序的步骤并分配人力资源加以执行.资源分配受访问控制约束及资源异常干扰,存在可满足性和鲁棒性问题.而其鲁棒性验证又依赖于其可满足性判定,目前通过求可满足性的一个解来完成.本文提出另一种途径,通过统计解的个数来完成判定.特别地,通过多项式计数归约为有求解器可用的#SAT问题,给出了互斥和绑定约束下的可满足性计数算法.实验表明,相对目前时间复杂度最低的可满足性求解算法,该可满足性计数算法显著提高了实际判定效率和适用规模.

关键词: 工作流, 授权, 约束, 资源分配, 可满足性

Abstract:

In a workflow system,a business process is decomposed into orderly steps,and then human resources are allocated to execute them.The process of resource allocation is constrained by access control and influenced by resource exceptions,so there exist the issues of satisfiability and robustness.Especially,the verification of its robustness relies on the judgment of its satisfiability,which is currently realized via finding one of the satisfiability solutions.This paper proposes another approach,in which the total number of all the solutions is counted to make a satisfiability judgment.Especially,the satisfiability counting under exclusion(≠) and binding(=) constraints is reduced to the problem of #SAT with solvers available by a polynomial-time counting reduction.Experiments show that,compared to the existing lowest-time satisfiability solving algorithm,our satisfiability counting algorithm achieves remarkable improvement in judgment efficiency and applicable scale.

Key words: workflow, authorization, constraint, resource allocation, satisfiability

中图分类号: