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. 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
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.
[1] WANG Q,Li N.Satisfiability and resiliency in workflow authorization systems[J]. ACM Transactions on Information and System Security,2010,13(4):1-35.
[2] BERTINO E,FERRARI E,ATLURI V.The specification and enforcement of authorization constraints in workflow management systems[J]. ACM Transactions on Information System Security.1999,2(1):65-104.
[3] ATLURI V,BERTINO E,FERRARI E,et al.Supporting delegation in secure workflow management systems[A]. Proceedings of the 17th Annual Conference on Data and Application of Security[C]. Berlin,GER:Springer,2003.190-202.
[4] CRAMPTON J,KHAMBHAMMETTU H.Delegation and satisfiability in workflow systems[A]. Proceedings of the 13th ACM Symposium on Access Control Models and Technologies[C]. NY,USA:ACM,2008.31-40.
[5] CRAMPTON J,GUTIN G.Constraint expressions and workflow satisfiability[A]. Proceedings of the 18th ACM Symposium on Access Control Models and Technologies[C]. NY,USA:ACM,2013.73-84.
[6] CRAMPTON J,GUTIN G,YEO A.On the parameterized complexity and kernelization of the workflow satisfiability problem[J]. ACM Transactions on Information and System Security,2013,16(1):1-31.
[7] BJORCLUND A,HUSFELDT T,KOIVISTO M.Set partitioning via inclusion-exclusion[J]. SIAM Journal on Computing,2009,39(2):546-563.
[8] THURLEY M.Sharp SAT counting models with advanced caching and implicit BCP[A]. Proc of the 9th International Conference on Theory and Applications of Satisfiability Testing[C]. Berlin,GER:Springer,2006.424-429.
[9] THURLEY M.SharpSAT[EB/OL]. https://github.com/marcthurley/sharpSAT,2013-02.
2015, Vol. 43 
