{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T07:03:43Z","timestamp":1742972623829,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":49,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642041662"},{"type":"electronic","value":"9783642041679"}],"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-04167-9_2","type":"book-chapter","created":{"date-parts":[[2009,8,19]],"date-time":"2009-08-19T10:45:02Z","timestamp":1250678702000},"page":"21-41","source":"Crossref","is-referenced-by-count":36,"title":["Formal Behavioral Modeling and Compliance Analysis for Service-Oriented Systems"],"prefix":"10.1007","author":[{"given":"Natallia","family":"Kokash","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Farhad","family":"Arbab","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"2_CR1","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1017\/S0960129504004153","volume":"14","author":"F. Arbab","year":"2004","unstructured":"Arbab, F.: Reo: A channel-based coordination model for component composition. Mathematical Structures in Computer Science\u00a014(3), 329\u2013366 (2004)","journal-title":"Mathematical Structures in Computer Science"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-540-72794-1_16","volume-title":"Coordination Models and Languages","author":"F. Arbab","year":"2007","unstructured":"Arbab, F., Chothia, T., Meng, S., Moon, Y.-J.: Component connectors with qoS guarantees. In: Murphy, A.L., Vitek, J. (eds.) COORDINATION 2007. LNCS, vol.\u00a04467, pp. 286\u2013304. Springer, Heidelberg (2007)"},{"issue":"1","key":"2_CR3","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s10270-006-0009-9","volume":"6","author":"F. Arbab","year":"2007","unstructured":"Arbab, F., Baier, C., Boer, F., Rutten, J.: Models and temporal logical specifications for timed component connectors. Software and Systems Modeling\u00a06(1), 59\u201382 (2007)","journal-title":"Software and Systems Modeling"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-540-72952-5_19","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"M. Sun","year":"2007","unstructured":"Sun, M., Arbab, F.: On resource-sensitive timed component connectors. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol.\u00a04468, pp. 301\u2013316. Springer, Heidelberg (2007)"},{"key":"2_CR5","first-page":"1281","volume-title":"Information and Software Technology (IST)","author":"R.M. Dijkman","year":"2008","unstructured":"Dijkman, R.M., Dumas, M., Ouyang, C.: Semantics and analysis of business process models in BPMN. In: Information and Software Technology (IST), vol.\u00a050(12), pp. 1281\u20131294. ACM Press, New York (2008)"},{"key":"2_CR6","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":"2_CR7","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.: Modeling 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)"},{"issue":"2","key":"2_CR8","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1147\/sj.462.0335","volume":"46","author":"Y. Liu","year":"2007","unstructured":"Liu, Y., M\u00fcller, S., Xu, K.: A static compliance-checking framework for business process models. IBM Systems Journal\u00a046(2), 335\u2013361 (2007)","journal-title":"IBM Systems Journal"},{"issue":"1","key":"2_CR9","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s10270-006-0009-9","volume":"6","author":"F. Arbab","year":"2007","unstructured":"Arbab, F., Baier, C., de Boer, F.S., Rutten, J.J.M.M.: Models and temporal logics for timed component connectors. Int. Journal on Software and Systems Modeling\u00a06(1), 59\u201382 (2007)","journal-title":"Int. Journal on Software and Systems Modeling"},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/j.scico.2005.10.008","volume":"61","author":"C. Baier","year":"2006","unstructured":"Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modeling component connectors in Reo by constraint automata. Science of Computer Programming\u00a061, 75\u2013113 (2006)","journal-title":"Science of Computer Programming"},{"key":"2_CR11","volume-title":"Proc. of the Int. Workshop on Formal Aspects in Component Software","author":"F. Arbab","year":"2008","unstructured":"Arbab, F., Koehler, C., Maraikar, Z., Moon, Y.J., Proenca, J.: Modeling, testing and executing Reo connectors with the Eclipse coordination tools. In: Proc. of the Int. Workshop on Formal Aspects in Component Software. Elsevier, Amsterdam (2008)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. of the Int. Symposium on Leveraging Applications of Formal Methods, Verification and Validation","author":"F. Arbab","year":"2008","unstructured":"Arbab, F., Kokash, N., Sun, M.: Towards using Reo for compliance-aware business process modelling. In: Proc. of the Int. Symposium on Leveraging Applications of Formal Methods, Verification and Validation. LNCS, vol.\u00a017. Springer, Heidelberg (2008)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-87891-9_8","volume-title":"Component-Based Software Engineering","author":"F. Arbab","year":"2008","unstructured":"Arbab, F., Sun, M.: Synthesis of connectors from scenario-based interaction specifications. In: Chaudron, M.R.V., Szyperski, C., Reussner, R. (eds.) CBSE 2008. LNCS, vol.\u00a05282, pp. 114\u2013129. Springer, Heidelberg (2008)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-79230-7_8","volume-title":"Web Services and Formal Methods","author":"S. Tasharofi","year":"2008","unstructured":"Tasharofi, S., Vakilian, M., Moghaddam, R.Z., Sirjani, M.: Modeling Web Service Interactions Using the Coordination Language Reo. In: Dumas, M., Heckel, R. (eds.) WS-FM 2007. LNCS, vol.\u00a04937, pp. 108\u2013123. Springer, Heidelberg (2008)"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Chothia, T., Kleijn, J.: Q-automata: Modelling the resource usage of concurrent components. In: Electronic Notes in Theoretical Computer Science: Proc. of the Int. Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA 2006), vol.\u00a0175(2), pp. 79\u201394 (2007)","DOI":"10.1016\/j.entcs.2007.03.009"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/978-3-642-02053-7_14","volume-title":"COORDINATION 2009","author":"F. Arbab","year":"2009","unstructured":"Arbab, F., Chothia, T., van der Mei, R., Sun, M., Moon, Y., Verhoef, C.: From coordination to stochastic models of QoS. In: COORDINATION 2009. LNCS, vol.\u00a05521, pp. 268\u2013287. Springer, Heidelberg (2009)"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/978-3-642-04167-9","volume-title":"COORDINATION 2009","author":"C. Baier","year":"2009","unstructured":"Baier, C., Blechmann, T., Klein, J., Kl\u00fcppelholz, S.: A uniform framework for modeling and verifying components and connectors. In: COORDINATION 2009. LNCS, vol.\u00a05521, pp. 268\u2013287. Springer, Heidelberg (2009)"},{"issue":"2","key":"2_CR18","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.entcs.2007.03.003","volume":"175","author":"S. Kl\u00fcppelholz","year":"2007","unstructured":"Kl\u00fcppelholz, S., Baier, C.: Symbolic model checking for channel-based component connectors. Electronic Notes in Theoretical Computer Science\u00a0175(2), 19\u201337 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2_CR19","unstructured":"Concortium, C.: Initial specification of compliance language constructs and operators. COMPAS Deliverable (2008)"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Blechmann, T., Baier, C.: Checking equivalence for Reo networks. In: Proc. of the Int. Workshop on Formal Aspects of Component Software, FACS (2007)","DOI":"10.1016\/j.entcs.2008.06.029"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Gligor, V.D., Gavrila, S.I., Ferraiolo, D.: On the formal definition of separation-of-duty policies and their composition. In: Proc. of IEEE Symposium on Research in Security and Privacy (1998)","DOI":"10.1109\/SECPRI.1998.674833"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Schaad, A., Lotz, V., Sohr, K.: A model-checking approach to analysing organisational controls in a loan origination process. In: Proc. of the eleventh ACM symposium on Access Control Models and Technologies, SACMAT (2006)","DOI":"10.1145\/1133058.1133079"},{"key":"2_CR23","first-page":"318","volume-title":"Proceedings of the ACM Symposium on Applied Computing (SAC 2009)","author":"N. Kokash","year":"2009","unstructured":"Kokash, N., Arbab, F.: Applying Reo to service coordination in long-running business transactions. In: Proceedings of the ACM Symposium on Applied Computing (SAC 2009), pp. 318\u2013319. ACM Press, New York (2009)"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-88194-0_22","volume-title":"Formal Methods and Software Engineering","author":"P.Y.H. Wong","year":"2008","unstructured":"Wong, P.Y.H., Gibbons, J.: A process semantics for BPMN. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol.\u00a05256, pp. 355\u2013374. Springer, Heidelberg (2008)"},{"key":"2_CR25","unstructured":"St\u00f6rrle, H., Hausmann, J.H.: Towards a formal semantics of UML 2.0 activities. Software Engineering, 117\u2013128 (2005)"},{"issue":"1","key":"2_CR26","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1016\/j.jlap.2006.05.007","volume":"70","author":"R. Lucchia","year":"2007","unstructured":"Lucchia, R., Mazzara, M.: A pi-calculus based semantics for WS-BPEL. Journal of Logic and Algebraic Programming\u00a070(1), 96\u2013118 (2007)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-79230-7_6","volume-title":"Web Services and Formal Methods","author":"N. Lohmann","year":"2008","unstructured":"Lohmann, N.: A feature-complete petri net semantics for WS-BPEL\u00a02.0. In: Dumas, M., Heckel, R. (eds.) WS-FM 2007. LNCS, vol.\u00a04937, pp. 77\u201391. Springer, Heidelberg (2008)"},{"issue":"2-3","key":"2_CR28","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. Science of Computer Programming\u00a067(2-3), 162\u2013198 (2007)","journal-title":"Science of Computer Programming"},{"key":"2_CR29","unstructured":"Oren, E., Haller, A.: Formal frameworks for workflow modelling. Technical Report 2005-04-07, DERI - Digital Enterprise Research Institute (2005)"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Raedts, I., Petkovi\u0107, M., Usenko, Y.S., van der Werf, J.M., Groote, J.F., Somers, L.: Transformation of BPMN models for behaviour analysis. In: Proceedings of the International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems (MSVVEIS), pp. 126\u2013137 (2007)","DOI":"10.5220\/0002428801260137"},{"issue":"3","key":"2_CR31","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/j.entcs.2008.04.098","volume":"200","author":"N. Guermouche","year":"2008","unstructured":"Guermouche, N., Perrin, O., Ringeissen, C.: Timed specification for web services compatibility analysis. Electronic Notes in Theoretical Computer Science (ENTCS)\u00a0200(3), 155\u2013170 (2008)","journal-title":"Electronic Notes in Theoretical Computer Science (ENTCS)"},{"key":"2_CR32","first-page":"593","volume-title":"Proc. of the Int. Conf. on Services Computing","author":"K. Mokhtari","year":"2008","unstructured":"Mokhtari, K., Benbernou, S., Said, M., Coquery, E., Hacid, M., Leymann, F.: Verification of privacy timed properties in web service protocols. In: Proc. of the Int. Conf. on Services Computing, pp. 593\u2013594. IEEE Computer Society, Los Alamitos (2008)"},{"key":"2_CR33","volume-title":"Proc. of the Australasian Database Conf. (ADC 2003)","author":"R. Hamadi","year":"2003","unstructured":"Hamadi, R., Benatallah, B.: A petri net-based model for web service composition. In: Proc. of the Australasian Database Conf. (ADC 2003), ACM Press, New York (2003)"},{"key":"2_CR34","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/1096967.1096977","volume-title":"Proc. of the Int. Workshop on Interoperability of Heterogeneous Information Systems","author":"Y. Yang","year":"2005","unstructured":"Yang, Y., Tan, Q., Xiao, Y.: Verifying web services composition based on hierarchical colored Petri nets. In: Proc. of the Int. Workshop on Interoperability of Heterogeneous Information Systems, pp. 47\u201354. ACM Press, New York (2005)"},{"key":"2_CR35","unstructured":"Dingwall-Smith, A., Finkelstein, A.: Checking complex compositions of web services against policy constraints. In: Proc. of the Int. Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, MSVVEIS (2007)"},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Halpern, J.Y., Weissman, V.: Using first-order logic to reason about policies. In: Proc. of the Computer Security Foundations Workshop, CSFW (2003)","DOI":"10.1109\/CSFW.2003.1212713"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"Mukherjee, S., Davulcu, H., Kifer, M., Senkul, P., Yang, G.: Logic based approaches to workflow modeling and verification. In: Logics for Emerging Applications of Databases (2003)","DOI":"10.1007\/978-3-642-18690-5_5"},{"key":"2_CR38","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1109\/EDOC.2002.1137700","volume-title":"Proc. of the Int. Enterprise Distributed Object Computing Conf.","author":"J. Koehler","year":"2002","unstructured":"Koehler, J., Tirenni, G., Kumaran, S.: From business process model to consistent implementation: A case for formal verification methods. In: Proc. of the Int. Enterprise Distributed Object Computing Conf., pp. 96\u2013107. IEEE Computer Society, Los Alamitos (2002)"},{"key":"2_CR39","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. Sadiq","year":"2007","unstructured":"Sadiq, W., 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)"},{"issue":"2","key":"2_CR40","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s10207-007-0017-y","volume":"6","author":"J. Cederquist","year":"2007","unstructured":"Cederquist, J., Corin, R., Dekker, M., Etalle, S., den Hartog, J., Lenzini, G.: Audit-based compliance control. Int. Journal of Information Security\u00a06(2), 133\u2013151 (2007)","journal-title":"Int. Journal of Information Security"},{"key":"2_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/11837862_2","volume-title":"Business Process Management Workshops","author":"S. Goedertier","year":"2006","unstructured":"Goedertier, S., Vanthienen, J.: Designing compliant business processes with obligations and permissions. In: Eder, J., Dustdar, S. (eds.) BPM Workshops 2006. LNCS, vol.\u00a04103, pp. 5\u201314. Springer, Heidelberg (2006)"},{"key":"2_CR42","first-page":"221","volume-title":"Proc. of the Int. Enterprize Distributed Object Computing Conf.","author":"G. Governatori","year":"2006","unstructured":"Governatori, G., Milosevic, Z., Sadiq, S.: Compliance checking between business processes and business contracts. In: Proc. of the Int. Enterprize Distributed Object Computing Conf., pp. 221\u2013232. IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"2_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-540-74974-5_14","volume-title":"Service-Oriented Computing \u2013 ICSOC 2007","author":"A.K. Ghose","year":"2007","unstructured":"Ghose, A.K., Koliadis, G.: Auditing business process compliance. In: Kr\u00e4mer, B.J., Lin, K.-J., Narasimhan, P. (eds.) ICSOC 2007. LNCS, vol.\u00a04749, pp. 169\u2013180. Springer, Heidelberg (2007)"},{"key":"2_CR44","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1145\/1314436.1314441","volume-title":"Proc. of the Workshop on Formal Methods in Security Engineering (FMSE 2007)","author":"J. Brunel","year":"2007","unstructured":"Brunel, J., Cuppens, F., Cuppens, N., Sans, T., Bodeveix, J.-P.: Security policy compliance with violation management. In: Proc. of the Workshop on Formal Methods in Security Engineering (FMSE 2007), pp. 31\u201340. ACM Press, New York (2007)"},{"key":"2_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-72988-4_17","volume-title":"Advanced Information Systems Engineering","author":"R. Hamadi","year":"2007","unstructured":"Hamadi, R., Paik, H.-Y., Benatallah, B.: Conceptual modeling of privacy-aware web service protocols. In: Krogstie, J., Opdahl, A.L., Sindre, G. (eds.) CAiSE 2007 and WES 2007. LNCS, vol.\u00a04495, pp. 233\u2013248. Springer, Heidelberg (2007)"},{"key":"2_CR46","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1145\/1377836.1377844","volume-title":"Proc. of the 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: Proc. of the ACM Symposium on Access Control Models and Technologies, pp. 51\u201360. ACM Press, New York (2008)"},{"key":"2_CR47","first-page":"356","volume-title":"Proc. of the ACM Conf. on Computer and Communications Security","author":"N. Li","year":"2006","unstructured":"Li, N., Wang, Q.: Beyond separation of duty: An algebra for specifying high-level security policies. In: Proc. of the ACM Conf. on Computer and Communications Security, pp. 356\u2013369. ACM Press, New York (2006)"},{"key":"2_CR48","doi-asserted-by":"crossref","unstructured":"Knorr, K., Stormer, H.: Modeling and analyzing separation of duties in workflow environments. In: Proc. of the Int. Conf. on Information Security: Trusted Information: the New Decade Challenge, pp. 199\u2013212 (2001)","DOI":"10.1007\/0-306-46998-7_14"},{"key":"2_CR49","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1109\/ICWS.2007.195","volume-title":"Proc. of the Int. Conf. on Web Services (ICWS)","author":"S. Koizumi","year":"2007","unstructured":"Koizumi, S., Koyama, K.: Workload-aware business process simulation with statistical service analysis and timed Petri net. In: Proc. of the Int. Conf. on Web Services (ICWS), pp. 70\u201377. IEEE Computer Society, Los Alamitos (2007)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04167-9_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T19:55:24Z","timestamp":1739303724000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04167-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642041662","9783642041679"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04167-9_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}