{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:12:06Z","timestamp":1763467926865,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642001987"},{"type":"electronic","value":"9783642001994"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-00199-4_1","type":"book-chapter","created":{"date-parts":[[2009,3,26]],"date-time":"2009-03-26T13:26:36Z","timestamp":1238073996000},"page":"1-15","source":"Crossref","is-referenced-by-count":19,"title":["Verification of Business Process Entailment Constraints Using SPIN"],"prefix":"10.1007","author":[{"given":"Christian","family":"Wolter","sequence":"first","affiliation":[]},{"given":"Philip","family":"Miseldine","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Meinel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3-4","key":"1_CR1","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1023\/B:ITEM.0000031582.55219.2b","volume":"5","author":"M. Muehlen Zur","year":"2004","unstructured":"Zur Muehlen, M.: Organizational Management in Workflow Applications \u2013 Issues and Perspectives. Inf. Technol. and Management\u00a05(3-4), 271\u2013291 (2004)","journal-title":"Inf. Technol. and Management"},{"key":"1_CR2","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1145\/1143120.1143124","volume-title":"SOUPS 2006: Proceedings of the second symposium on Usable privacy and security","author":"X. Cao","year":"2006","unstructured":"Cao, X., Iverson, L.: Intentional Access Management: Making Access Control Usable for End-Users. In: SOUPS 2006: Proceedings of the second symposium on Usable privacy and security, vol.\u00a02, pp. 20\u201331. ACM Press, New York (2006)"},{"key":"1_CR3","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1109\/ITCC.2004.1286497","volume-title":"ITCC 2004: Proceedings of the International Conference on Information Technology: Coding and Computing (ITCC 2004)","author":"F.T. Alotaiby","year":"2004","unstructured":"Alotaiby, F.T., Chen, J.X.: A model for team-based access control (tmac 2004). In: ITCC 2004: Proceedings of the International Conference on Information Technology: Coding and Computing (ITCC 2004), Washington, DC, USA, p. 450. IEEE Computer Society, Los Alamitos (2004)"},{"issue":"6","key":"1_CR4","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1016\/S0306-4379(02)00029-7","volume":"28","author":"S. Oh","year":"2003","unstructured":"Oh, S., Park, S.: Task-role-based access control model. Inf. Syst.\u00a028(6), 533\u2013562 (2003)","journal-title":"Inf. Syst."},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1145\/1029133.1029140","volume-title":"FMSE 2004: Proceedings of the 2004 ACM workshop on Formal methods in security engineering","author":"L. Wang","year":"2004","unstructured":"Wang, L., Wijesekera, D., Jajodia, S.: A logic-based framework for attribute based access control. In: FMSE 2004: Proceedings of the 2004 ACM workshop on Formal methods in security engineering, pp. 45\u201355. ACM, New York (2004)"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Thomas, R.K.: Task-based Authorization Controls (TBAC): A Family of Models for Active and Enterprise-oriented Authorization Management. pp. 166\u2013181 (1997)","DOI":"10.1007\/978-0-387-35285-5_10"},{"key":"1_CR7","first-page":"139","volume-title":"SACMAT 2006: ACM symposium on Access control models and technologies","author":"A. Schaad","year":"2006","unstructured":"Schaad, A., Lotz, V., Sohr, K.: A model-checking approach to analysing organisational controls in a loan origination process. In: SACMAT 2006: ACM symposium on Access control models and technologies, pp. 139\u2013149. ACM, New York (2006)"},{"key":"1_CR8","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1145\/373256.373283","volume-title":"SACMAT 2001: Proceedings of the sixth ACM symposium on Access control models and technologies","author":"T. Jeager","year":"2001","unstructured":"Jeager, T.: Managing access control complexity using metrics. In: SACMAT 2001: Proceedings of the sixth ACM symposium on Access control models and technologies, pp. 131\u2013139. ACM Press, New York (2001)"},{"key":"1_CR9","first-page":"51","volume-title":"SACMAT 2008: Proceedings of the 13th ACM symposium on Access control models and technologies","author":"C. Wolter","year":"2008","unstructured":"Wolter, C., Schaad, A., Meinel, C.: Task-based entailment constraints for basic workflow patterns. In: SACMAT 2008: Proceedings of the 13th ACM symposium on Access control models and technologies, pp. 51\u201360. ACM, New York (2008)"},{"key":"1_CR10","first-page":"1278","volume-title":"Proc. IEEE","author":"J.H. Saltzer","year":"1975","unstructured":"Saltzer, J.H., Schroeder, M.D.: The Protection of Information in Computer Systems. In: Proc. IEEE, vol.\u00a063, pp. 1278\u20131308. IEEE Computer Society Press, Los Alamitos (1975)"},{"key":"1_CR11","unstructured":"Tan, K., Crampton, J., Gunter, C.A.: The Consistency of Task-Based Authorization Constraints in Workflow Systems. In: CSFW, p. 155- (2004)"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-540-74835-9_7","volume-title":"Computer Security \u2013 ESORICS 2007","author":"Q. Wang","year":"2007","unstructured":"Wang, Q., Li, N.: Satisfiability and Resiliency in Workflow Systems. In: Biskup, J., L\u00f3pez, J. (eds.) ESORICS 2007. LNCS, vol.\u00a04734, pp. 90\u2013105. Springer, Heidelberg (2007)"},{"issue":"1","key":"1_CR13","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1145\/300830.300837","volume":"2","author":"E. Bertino","year":"1999","unstructured":"Bertino, E., Ferrari, E., Atluri, V.: The specification and enforcement of authorization constraints in workflow management systems. ACM Trans. Inf. Syst. Secur.\u00a02(1), 65\u2013104 (1999)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"issue":"3","key":"1_CR14","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10009-007-0038-x","volume":"9","author":"K. Jensen","year":"2007","unstructured":"Jensen, K., Kristensen, L., Wells, L.: Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems. International Journal on Software Tools for Technology Transfer (STTT)\u00a09(3), 213\u2013254 (2007)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"issue":"2","key":"1_CR15","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1147\/sj.462.0335","volume":"46","author":"Y. Liu","year":"2007","unstructured":"Liu, Y., Mueller, S., Xu, K.: A static compliance-checking framework for business process models. IBM Syst. J.\u00a046(2), 335\u2013361 (2007)","journal-title":"IBM Syst. J."},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-85758-7_24","volume-title":"Business Process Management","author":"A. Awad","year":"2008","unstructured":"Awad, A., Decker, G., Weske, M.: Efficient Compliance Checking Using BPMN-Q and Temporal Logic. In: Dumas, M., Reichert, M., Shan, M.-C. (eds.) BPM 2008. LNCS, vol.\u00a05240, pp. 326\u2013341. Springer, Heidelberg (2008)"},{"key":"1_CR17","unstructured":"Object\u00a0Management Group. Business Process Modeling Notation Specification (2006), http:\/\/www.bpmn.org"},{"key":"1_CR18","volume-title":"The SPIN Model Checker : Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/11431855_16","volume-title":"Advanced Information Systems Engineering","author":"N. Russell","year":"2005","unstructured":"Russell, N., van der Aalst, W.M.P., ter Hofstede, A.H.M., Edmond, D.: Workflow Resource Patterns: Identification, Representation and Tool Support. In: Pastor, \u00d3., Falc\u00e3o e Cunha, J. (eds.) CAiSE 2005. LNCS, vol.\u00a03520, pp. 216\u2013232. Springer, Heidelberg (2005)"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/11841760_12","volume-title":"Business Process Management","author":"P. Wohed","year":"2006","unstructured":"Wohed, P., van der Aalst, W.M.P., Dumas, M., ter Hofstede, A.H.M., Russell, N.: On the Suitability of BPMN for Business Process Modelling. In: Dustdar, S., Fiadeiro, J.L., Sheth, A.P. (eds.) BPM 2006. LNCS, vol.\u00a04102, pp. 161\u2013176. Springer, Heidelberg (2006)"},{"issue":"3","key":"1_CR21","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1147\/sj.403.0666","volume":"40","author":"R.A. Botha","year":"2001","unstructured":"Botha, R.A., Eloff, J.H.P.: Separation of Duties for Access Control Enforcement in Workflow Environments. IBM System Journal\u00a040(3), 666\u2013682 (2001)","journal-title":"IBM System Journal"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-75183-0_5","volume-title":"Business Process Management","author":"C. Wolter","year":"2007","unstructured":"Wolter, C., Schaad, A.: Modelling of Task-Based Authorization Constraints in BPMN. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol.\u00a04714, pp. 64\u201379. Springer, Heidelberg (2007)"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-75183-0_12","volume-title":"Business Process Management","author":"W.S. Sadiq","year":"2007","unstructured":"Sadiq, W.S., Governatori, G., Namiri, K.: Modeling Control Objectives for Business Process Compliance. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol.\u00a04714, pp. 149\u2013164. Springer, Heidelberg (2007)"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","volume-title":"Lectures on Concurrency and Petri Nets","year":"2004","unstructured":"Desel, J., Reisig, W., Rozenberg, G. (eds.): Lectures on Concurrency and Petri Nets. LNCS, vol.\u00a03098. Springer, Heidelberg (2004)"},{"key":"1_CR25","unstructured":"Dijkman, R.M., Dumas, M., Ouyang, C.: Formal semantics and analysis of bpmn process models. Technical report, Queensland University of Technology (2007)"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Ribeiro, O.R., Fernandes, J.M.: Translating Synchronous Petri Nets into PROMELA for Verifying Behavioural Properties. In: International Symposium on Industrial Embedded Systems, SIES 2007 (2007)","DOI":"10.1109\/SIES.2007.4297344"},{"issue":"2-3","key":"1_CR27","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.scico.2007.03.002","volume":"67","author":"C. Ouyang","year":"2007","unstructured":"Ouyang, C., Verbeek, E., van der Aalst, W.M.P., Breutel, S., Dumas, M., ter Hofstede, A.H.M.: Formal semantics and analysis of control flow in ws-bpel. Sci. Comput. Program.\u00a067(2-3), 162\u2013198 (2007)","journal-title":"Sci. Comput. Program."},{"key":"1_CR28","first-page":"116","volume-title":"SAINT 2006: Proceedings of the International Symposium on Applications on Internet","author":"Y. Yang","year":"2006","unstructured":"Yang, Y., Tan, Q., Xiao, Y., Yu, J., Liu, F.: Exploiting Hierarchical CP-Nets to Increase the Reliability of Web Services Workflow. In: SAINT 2006: Proceedings of the International Symposium on Applications on Internet, pp. 116\u2013122. IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"1_CR29","doi-asserted-by":"publisher","first-page":"57","DOI":"10.2201\/NiiPi.2005.2.5","volume":"2","author":"Nakajima","year":"2005","unstructured":"Nakajima, Shin: Lightweight formal analysis of Web service flows. Progress in informatics: PI\u00a02, 57\u201376 (2005)","journal-title":"Progress in informatics : PI"},{"key":"1_CR30","first-page":"621","volume-title":"WWW 2004: Proceedings of the 13th international conference on World Wide Web","author":"X. Fu","year":"2004","unstructured":"Fu, X., Bultan, T., Su, J.: Analysis of interacting BPEL web services. In: WWW 2004: Proceedings of the 13th international conference on World Wide Web, pp. 621\u2013630. ACM Press, New York (2004)"},{"key":"1_CR31","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1145\/1007512.1007547","volume-title":"ISSTA 2004: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis","author":"X. Fu","year":"2004","unstructured":"Fu, X., Bultan, T., Su, J.: Model checking XML manipulating software. In: ISSTA 2004: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, pp. 252\u2013262. ACM, New York (2004)"},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science","first-page":"826","volume-title":"Selected Areas in Cryptography","author":"J.A. Fisteus","year":"2006","unstructured":"Fisteus, J.A., Fern\u00e1ndez, L.S., Kloos, C.D.: Applying model checking to BPEL4WS business collaborations. In: Preneel, B., Tavares, S. (eds.) SAC 2005. LNCS, vol.\u00a03897, pp. 826\u2013830. Springer, Heidelberg (2006)"},{"key":"1_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/11841760_36","volume-title":"Business Process Management","author":"Z. Xiangpeng","year":"2006","unstructured":"Xiangpeng, Z., Cerone, A., Krishnan, P.: Verifying BPEL Workflows Under Authorisation Constraints. In: Dustdar, S., Fiadeiro, J.L., Sheth, A.P. (eds.) BPM 2006. LNCS, vol.\u00a04102, pp. 439\u2013444. Springer, Heidelberg (2006)"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","first-page":"439","volume-title":"BPM","author":"A. Masood","year":"2006","unstructured":"Masood, A., Bhatti, R., Ghafoor, A., Mathur, A.: Model-based Testing of Access Control Systems that Employ RBAC Policies. In: BPM 2006. LNCS, pp. 439\u2013444. Springer, Heidelberg (2006)"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Huang, W.-k., Atluri, V.: SecureFlow: A Secure Web-Enabled Workflow Management System. In: ACM Workshop on Role-Based Access Control, pp. 83\u201394 (1999)","DOI":"10.1145\/319171.319179"},{"key":"1_CR36","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1145\/1063979.1063986","volume-title":"SACMAT 2005: Proceedings of the tenth ACM Symposium on Access Control Models and Technologies","author":"J. Crampton","year":"2005","unstructured":"Crampton, J.: A Reference Monitor for Workflow Systems with Constrained Task Execution. In: SACMAT 2005: Proceedings of the tenth ACM Symposium on Access Control Models and Technologies, pp. 38\u201347. ACM, New York (2005)"}],"container-title":["Lecture Notes in Computer Science","Engineering Secure Software and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00199-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,3]],"date-time":"2021-10-03T16:39:08Z","timestamp":1633279148000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00199-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642001987","9783642001994"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00199-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}