{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T18:40:59Z","timestamp":1771008059496,"version":"3.50.1"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031331626","type":"print"},{"value":"9783031331633","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-33163-3_23","type":"book-chapter","created":{"date-parts":[[2023,5,15]],"date-time":"2023-05-15T12:45:38Z","timestamp":1684154738000},"page":"303-320","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Task Model Design and\u00a0Analysis with\u00a0Alloy"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2714-8027","authenticated-orcid":false,"given":"Alcino","family":"Cunha","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4817-948X","authenticated-orcid":false,"given":"Nuno","family":"Macedo","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7891-6885","authenticated-orcid":false,"given":"Eunsuk","family":"Kang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,5,15]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Barboni, E., Ladry, J.F., Navarre, D., Palanque, P., Winckler, M.: Beyond modelling: an integrated environment supporting co-execution of tasks and systems models. In: EICS, pp. 165\u2013174. ACM (2010)","DOI":"10.1145\/1822018.1822043"},{"key":"23_CR2","unstructured":"Ben Amor, M.: Hamsters: a new task model for interactive systems. Master\u2019s thesis, University of Namur (2009)"},{"issue":"11","key":"23_CR3","doi-asserted-by":"publisher","first-page":"888","DOI":"10.1016\/j.ijhcs.2012.05.010","volume":"70","author":"ML Bolton","year":"2012","unstructured":"Bolton, M.L., Bass, E.J., Siminiceanu, R.I.: Generating phenotypical erroneous human behavior to evaluate human-automation interaction using model checking. Int. J. Hum Comput Stud. 70(11), 888\u2013906 (2012)","journal-title":"Int. J. Hum Comput Stud."},{"issue":"5","key":"23_CR4","doi-asserted-by":"publisher","first-page":"961","DOI":"10.1109\/TSMCA.2011.2109709","volume":"41","author":"ML Bolton","year":"2011","unstructured":"Bolton, M.L., Siminiceanu, R.I., Bass, E.J.: A systematic approach to model checking human-automation interaction using task analytic models. IEEE Trans. Syst. Man Cybern. - Part A: Syst. Humans 41(5), 961\u2013976 (2011)","journal-title":"IEEE Trans. Syst. Man Cybern. - Part A: Syst. Humans"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"Brunel, J., Chemouil, D., Cunha, A., Macedo, N.: The electrum analyzer: model checking relational first-order temporal specifications. In: ASE, pp. 884\u2013887. ACM (2018)","DOI":"10.1145\/3238147.3240475"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Campos, J.C., Fayollas, C., Martinie, C., Navarre, D., Palanque, P., Pinto, M.: Systematic automation of scenario-based testing of user interfaces. In: EICS, pp. 138\u2013148. ACM (2016)","DOI":"10.1145\/2933242.2948735"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"Campos, J.C., et al.: A more intelligent test case generation approach through task models manipulation. In: Proceedings of the ACM on Human-computer Interaction 1(EICS), pp. 1\u201320 (2017)","DOI":"10.1145\/3095811"},{"key":"23_CR8","unstructured":"Campos, J.C., Harrison, M.: Modelling and analysing the interactive behaviour of an infusion pump. Electron. Commun. EASST 45 (2011)"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"Cerone, A., Lindsay, P.A., Connelly, S.: Formal analysis of human-computer interaction using model-checking. In: SEFM, pp. 352\u2013362. IEEE Computer Society (2005)","DOI":"10.1109\/SEFM.2005.19"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-319-22723-8_16","volume-title":"Human-Computer Interaction \u2013 INTERACT 2015","author":"R Fahssi","year":"2015","unstructured":"Fahssi, R., Martinie, C., Palanque, P.: Enhanced task modelling for systematic identification and explicit representation of human errors. In: Abascal, J., Barbosa, S., Fetter, M., Gross, T., Palanque, P., Winckler, M. (eds.) INTERACT 2015. LNCS, vol. 9299, pp. 192\u2013212. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22723-8_16"},{"key":"23_CR11","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2016","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2016)"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight specification and analysis of dynamic systems with rich configurations. In: SIGSOFT FSE, pp. 373\u2013383. ACM (2016)","DOI":"10.1145\/2950290.2950318"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Martinie, C., Navarre, D., Palanque, P., Fayollas, C.: A generic tool-supported framework for coupling task models and interactive applications. In: EICS, pp. 244\u2013253. ACM (2015)","DOI":"10.1145\/2774225.2774845"},{"issue":"2","key":"23_CR14","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1109\/THMS.2014.2365956","volume":"46","author":"C Martinie","year":"2015","unstructured":"Martinie, C., Palanque, P., Fahssi, R., Blanquart, J.P., Fayollas, C., Seguin, C.: Task model-based systematic analysis of both system failures and human errors. IEEE Trans. Human-Mach. Syst. 46(2), 243\u2013254 (2015)","journal-title":"IEEE Trans. Human-Mach. Syst."},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/978-3-642-23765-2_40","volume-title":"Human-Computer Interaction \u2013 INTERACT 2011","author":"C Martinie","year":"2011","unstructured":"Martinie, C., Palanque, P., Winckler, M.: Structuring and composition mechanisms to address scalability issues in task models. In: Campos, P., Graham, N., Jorge, J., Nunes, N., Palanque, P., Winckler, M. (eds.) INTERACT 2011. LNCS, vol. 6948, pp. 589\u2013609. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23765-2_40"},{"issue":"8","key":"23_CR16","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1109\/TSE.2002.1027801","volume":"28","author":"G Mori","year":"2002","unstructured":"Mori, G., Patern\u00f2, F., Santoro, C.: CTTE: support for developing and analyzing task models for interactive system design. IEEE Trans. Software Eng. 28(8), 797\u2013813 (2002)","journal-title":"IEEE Trans. Software Eng."},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Palanque, P., Campos, J.C.: AMAN case study (2022)","DOI":"10.1007\/978-3-031-33163-3_21"},{"key":"23_CR18","volume-title":"Model-Based Design and Evaluation of Interactive Applications","author":"F Paterno","year":"1999","unstructured":"Paterno, F.: Model-Based Design and Evaluation of Interactive Applications. Springer, Cham (1999)"},{"key":"23_CR19","doi-asserted-by":"crossref","unstructured":"Patern\u00f2, F., Mancini, C., Meniconi, S.: ConcurTaskTrees: a diagrammatic notation for specifying task models. In: INTERACT. IFIP Conference Proceedings, vol. 96, pp. 362\u2013369. Chapman & Hall (1997)","DOI":"10.1007\/978-0-387-35175-9_58"},{"issue":"2","key":"23_CR20","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1006\/ijhc.2001.0523","volume":"56","author":"F Paterno","year":"2002","unstructured":"Paterno, F., Santoro, C.: Preventing user errors by systematic analysis of deviations from the system task model. Int. J. Hum Comput Stud. 56(2), 225\u2013245 (2002)","journal-title":"Int. J. Hum Comput Stud."},{"key":"23_CR21","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198861270.001.0001","volume-title":"Fix IT: How to See and Solve the Problems of Digital Healthcare","author":"H Thimbleby","year":"2021","unstructured":"Thimbleby, H.: Fix IT: How to See and Solve the Problems of Digital Healthcare. Oxford University Press, Oxford (2021)"}],"container-title":["Lecture Notes in Computer Science","Rigorous State-Based Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-33163-3_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,10]],"date-time":"2023-06-10T08:04:11Z","timestamp":1686384251000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-33163-3_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031331626","9783031331633"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-33163-3_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"15 May 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ABZ","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Rigorous State-Based Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 May 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 June 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"abz2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/abz2023.loria.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"47","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}