{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T12:32:19Z","timestamp":1725798739859},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319101712"},{"type":"electronic","value":"9783319101729"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10172-9_19","type":"book-chapter","created":{"date-parts":[[2014,8,12]],"date-time":"2014-08-12T06:52:14Z","timestamp":1407826334000},"page":"301-316","source":"Crossref","is-referenced-by-count":6,"title":["User-Friendly Property Specification and Process Verification \u2013 A Case Study with Vehicle-Commissioning Processes"],"prefix":"10.1007","author":[{"given":"Richard","family":"Mrasek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jutta","family":"M\u00fclle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klemens","family":"B\u00f6hm","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Becker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Allmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"van der Aalst, W.M.P.: The Application of Petri Nets to Workflow Management. Journal of Circuits, Systems and Computers (1998)","DOI":"10.1142\/S0218126698000043"},{"key":"19_CR2","unstructured":"van der Aalst, W.M.P., van Hee, K.: Workflow Management: Models, Methods, and Systems. MIT Press (2004)"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"van der Aalst, W.M.P., ter Hofstede, A.H.M.: YAWL: Yet Another Workflow Language. Information Systems (2005)","DOI":"10.1016\/j.is.2004.02.002"},{"key":"19_CR4","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":"19_CR5","doi-asserted-by":"crossref","unstructured":"Bangor, A., Kortum, P.T., Miller, J.T.: An Empirical Evaluation of the System Usability Scale. International Journal of Human-Computer Interaction (2008)","DOI":"10.1080\/10447310802205776"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1007\/11531371_70","volume-title":"Web Engineering","author":"M. Brambilla","year":"2005","unstructured":"Brambilla, M., Deutsch, A., Sui, L., Vianu, V.: The Role of Visual Tools in a Web Application Design and Verification Framework: A Visual Notation for LTL Formulae. In: Lowe, D.G., Gaedke, M. (eds.) ICWE 2005. LNCS, vol.\u00a03579, pp. 557\u2013568. Springer, Heidelberg (2005)"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. Program. Lang. Syst. (1986)","DOI":"10.1007\/978-3-642-82453-1_1"},{"key":"19_CR8","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press (1999)"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Cobleigh, R.L., Avrunin, G.S., Clarke, L.A.: User Guidance for Creating Precise and Accessible Property Specifications. In: ACM SIGSOFT International Symposium on Foundations of Software Engineering (2006)","DOI":"10.1145\/1181775.1181801"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property Specification Patterns for Finite-State Verification. In: 2nd Workshop on Formal Methods in Software Practice (1998)","DOI":"10.1145\/298595.298598"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-03848-8_19","volume-title":"Business Process Management","author":"D. Fahland","year":"2009","unstructured":"Fahland, D., Favre, C., Jobstmann, B., Koehler, J., Lohmann, N., V\u00f6lzer, H., Wolf, K.: Instantaneous Soundness Checking of Industrial Business Process Models. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) BPM 2009. LNCS, vol.\u00a05701, pp. 278\u2013293. Springer, Heidelberg (2009)"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/11538394_15","volume-title":"Business Process Management","author":"S. Hinz","year":"2005","unstructured":"Hinz, S., Schmidt, K., Stahl, C.: Transforming BPEL to Petri Nets. In: van der Aalst, W.M.P., Benatallah, B., Casati, F., Curbera, F. (eds.) BPM 2005. LNCS, vol.\u00a03649, pp. 220\u2013235. Springer, Heidelberg (2005)"},{"key":"19_CR13","unstructured":"ISO, Geneva, Switzerland: Road vehicles \u2013 Open Test sequence eXchange format (OTX). ISO 13209 (2012)"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN Tools for Modelling and Validation of Concurrent Systems. International Journal on Software Tools for Technology Transfer (2007)","DOI":"10.1007\/s10009-007-0038-x"},{"key":"19_CR15","series-title":"LNBIP","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-642-28115-0_3","volume-title":"Business Process Management Workshops","author":"S. Rinderle-Ma","year":"2012","unstructured":"Rinderle-Ma, S., Kabicher, S., Ly, L.T.: Activity-oriented clustering techniques in large process and compliance rule repositories. In: Daniel, F., Barkaoui, K., Dustdar, S. (eds.) BPM Workshops 2011, Part II. LNBIP, vol.\u00a0100, pp. 14\u201325. Springer, Heidelberg (2012)"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-642-16373-9_24","volume-title":"Conceptual Modeling \u2013 ER 2010","author":"D. Knuplesch","year":"2010","unstructured":"Knuplesch, D., Ly, L.T., Rinderle-Ma, S., Pfeifer, H., Dadam, P.: On Enabling Data-Aware Compliance Checking of Business Process Models. In: Parsons, J., Saeki, M., Shoval, P., Woo, C., Wand, Y. (eds.) ER 2010. LNCS, vol.\u00a06412, pp. 332\u2013346. Springer, Heidelberg (2010)"},{"key":"19_CR17","unstructured":"Kopp, O., et al.: The Difference Between Graph-Based and Block-Structured Business Process Modelling Languages. Enterprise Modelling and Information Systems Architecture (2009)"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Liu, Y., Muller, S., Xu, K.: A Static Compliance-Checking Framework for Business Process Models. IBM Systems Journal (2007)","DOI":"10.1147\/sj.462.0335"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-00899-3_3","volume-title":"Transactions on Petri Nets and Other Models of Concurrency II","author":"N. Lohmann","year":"2009","unstructured":"Lohmann, N., Verbeek, E., Dijkman, R.: Petri Net Transformations for Business Processes\u2013a Survey. In: Jensen, K., van der Aalst, W.M.P. (eds.) Transactions on Petri Nets and Other Models of Concurrency II. LNCS, vol.\u00a05460, pp. 46\u201363. Springer, Heidelberg (2009)"},{"key":"19_CR20","series-title":"LNBIP","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-17722-4_6","volume-title":"Information Systems Evolution","author":"L.T. Ly","year":"2011","unstructured":"Ly, L.T., Knuplesch, D., Rinderle-Ma, S., G\u00f6ser, K., Pfeifer, H., Reichert, M., Dadam, P.: SeaFlows Toolset \u2013 Compliance Verification Made Easy for Process-Aware Information Systems. In: Soffer, P., Proper, E. (eds.) CAiSE Forum 2010. LNBIP, vol.\u00a072, pp. 76\u201391. Springer, Heidelberg (2011)"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-00899-3_12","volume-title":"Transactions on Petri Nets and Other Models of Concurrency II","author":"J. Mendling","year":"2009","unstructured":"Mendling, J.: Empirical Studies in Process Model Verification. In: Jensen, K., van der Aalst, W.M.P. (eds.) Transactions on Petri Nets and Other Models of Concurrency II. LNCS, vol.\u00a05460, pp. 208\u2013224. Springer, Heidelberg (2009)"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-38709-8_20","volume-title":"Advanced Information Systems Engineering","author":"E. Ramezani Taghiabadi","year":"2013","unstructured":"Ramezani Taghiabadi, E., Fahland, D., van Dongen, B.F., van der Aalst, W.M.P.: Diagnostic Information for Compliance Checking of Temporal Compliance Requirements. In: Salinesi, C., Norrie, M.C., Pastor, \u00d3. (eds.) CAiSE 2013. LNCS, vol.\u00a07908, pp. 304\u2013320. Springer, Heidelberg (2013)"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Schlingloff, H., Martens, A., Schmidt, K.: Modeling and Model Checking Web Services. Electronic Notes in Theoretical Computer Science (2005)","DOI":"10.1016\/j.entcs.2004.11.011"},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/3-540-44988-4_27","volume-title":"Application and Theory of Petri Nets 2000","author":"K. Schmidt","year":"2000","unstructured":"Schmidt, K.: LoLA A Low Level Analyser. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol.\u00a01825, p. 465. Springer, Heidelberg (2000)"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/3-540-48745-X_4","volume-title":"Application and Theory of Petri Nets 1999","author":"K. Schmidt","year":"1999","unstructured":"Schmidt, K.: Stubborn Sets for Standard Properties. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol.\u00a01639, pp. 46\u201365. Springer, Heidelberg (1999)"},{"key":"19_CR26","unstructured":"Schmidt, K.: Stubborn Sets for Model Checking the EF\/AG Fragment of CTL. Fundamenta Informaticae (2000)"},{"key":"19_CR27","unstructured":"Schneider, T.: Specification of Testing Workflows for Vehicles and Validation of Manually Created Testing Processes. Master\u2019s thesis, Karlsruhe Institute of Technology (May 2012) (in German)"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Smith, R.L., et al.: PROPEL: An Approach Supporting Property Elucidation. In: Conference on Software Engineering (2002)","DOI":"10.1145\/581344.581345"},{"key":"19_CR29","unstructured":"Stahl, C.: A Petri Net Semantics for BPEL, Technical Report 188. Humboldt-Universit\u00e4t zu Berlin (2005)"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/978-3-642-31095-9_28","volume-title":"Advanced Information Systems Engineering","author":"N. Syed Abdullah","year":"2012","unstructured":"Syed Abdullah, N., Sadiq, S., Indulska, M.: A Compliance Management Ontology: Developing Shared Understanding through Models. In: Ralyt\u00e9, J., Franch, X., Brinkkemper, S., Wrycza, S. (eds.) CAiSE 2012. LNCS, vol.\u00a07328, pp. 429\u2013444. Springer, Heidelberg (2012)"},{"key":"19_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-540-85758-7_10","volume-title":"Business Process Management","author":"J. Vanhatalo","year":"2008","unstructured":"Vanhatalo, J., V\u00f6lzer, H., Koehler, J.: The Refined Process Structure Tree. In: Dumas, M., Reichert, M., Shan, M.-C. (eds.) BPM 2008. LNCS, vol.\u00a05240, pp. 100\u2013115. Springer, Heidelberg (2008)"},{"key":"19_CR32","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)"},{"key":"19_CR33","doi-asserted-by":"crossref","unstructured":"Zimmermann, W., Schmidgall, R.: Bussysteme in der Fahrzeugtechnik \u2013 Protokolle, Standards und Softwarearchitektur. Vieweg + Teubner (2010)","DOI":"10.1007\/978-3-8348-9845-6"}],"container-title":["Lecture Notes in Computer Science","Business Process Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10172-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T11:29:43Z","timestamp":1558956583000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10172-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319101712","9783319101729"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10172-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}