期刊文献+

Verification of workflow nets with transition conditions 被引量:2

Verification of workflow nets with transition conditions
原文传递
导出
摘要 Workflow management is concerned with automated support for business processes.Workflow management systems are driven by process models specifying the tasks that need to be executed,the order in which they can be executed,which resources are authorised to perform which tasks,and data that is required for,and produced by,these tasks.As workflow instances may run over a sustained period of time,it is important that workflow specifications be checked before they are deployed.Workflow verification is usually concerned with control-flow dependencies only;however,transition conditions based on data may further restrict possible choices between tasks.In this paper we extend workflow nets where transitions have concrete conditions associated with them,called WTC-nets.We then demonstrate that we can determine which execution paths of a WTC-net that are possible according to the control-flow dependencies,are actually possible when considering the conditions based on data.Thus,we are able to more accurately determine at design time whether a workflow net with transition conditions is sound. Workflow management is concerned with automated support for business processes. Workflow manage- ment systems are driven by process models specifying the tasks that need to be executed, the order in which they can be executed, which resources are authorised to perform which tasks, and data that is required for, and produced by, these tasks. As workflow instances may run over a sustained period of time, it is important that workflow specifica- tions be checked before they are deployed. Workflow verification is usually concerned with control-flow dependencies only; however, transition conditions based on data may further restrict possible choices between tasks. In this paper we extend workflow nets where transitions have concrete conditions associated with them, called WTC-nets. We then demonstrate that we can determine which execution paths of a WTC-net that are possible according to the control-flow dependencies, are actually possible when considering the conditions based on data. Thus, we are able to more accurately determine at design time whether a workflow net with transition conditions is sound.
出处 《Journal of Zhejiang University-Science C(Computers and Electronics)》 SCIE EI 2012年第7期483-509,共27页 浙江大学学报C辑(计算机与电子(英文版)
基金 Project supported by the National Science and Technology Major Project of China (No.2010ZX01042-002-002-01) the National Basic Research Program (973) of China (No.2009CB320700) the National Natural Science Foundation of China (Nos.61073005 and 61003099)
  • 相关文献

参考文献46

  • 1Clarke, L.A., 1976. A system to generate test data and symbolically execute programs. IEEE Trans. Software Eng., 2(3):215-222. [doi:10.1109/TSE.1976.233817].
  • 2Curran, T., Keller, G., 1998. SAP R/3 Business Blueprint: Understanding the Business Process Reference Model. Prentice Hall PTR, Upper Saddle River, N J, USA.
  • 3Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K., 1991. Efficiently computing static sin- gle assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst., 13(4):451-490. [doi:10.1145/115372.115320].
  • 4Dehnert, J., van der AMst, W.M.P., 2004. Bridging the gap between business models and workflow specifica- tions. Int. d. Cooper. Inf. Syst., 13(3):289-332. [doi: 10.1142/S0218843004000973].
  • 5Dutertre, B., de Moura, L.M., 2006a. A Fast Linear- Arithmetic Solver for DPLL(T). 18th Int. Conf. on Computer Aided Verification, p.81-94, ldoi:10.1007/ 11817963_11].
  • 6Dutertre, B., de Moura, L., 2006b. The Yices SMT Solver. Available from http://yices.csl.sri.com/tool-paper.pdf.
  • 7Fan, S., Dou, W., Chen, J., 2007. Dual Workflow Nets: Mixed Control/Data-Flow Representation for Workflow Modeling and Verification. Advances in Web and Net- work Technologies and Information Management, p.433~ 444. Idoi" 10.1007/978-3-540-72909-9 46].
  • 8Franco, j.V., 2005. Atypical case complexity of satisfiabil- ity algorithms and the threshold phenomenon. Discr. Appl. Math., 153(1-3):89-123. [doi:10.1016/j.dam. 2005.05.008].
  • 9Ganzinger, H., I:lagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C., 2004. DPLL(T): Fast Decision Procedures. 16th Int. Conf. on Computer Aided Verification, p.175- 188. [doi: 10.1007/978-3-540-27813-9 14].
  • 10Graf, S., SaYdi, H., 1997. Construction-of "Abstract State Graphs with PVS. 9th Int. Conf. on Computer Aided Verification, p.72-83. [doi:10.1007/3-540-63166-6 10].

同被引文献3

引证文献2

二级引证文献6

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部