{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T10:34:02Z","timestamp":1742985242833,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030549930"},{"type":"electronic","value":"9783030549947"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-54994-7_31","type":"book-chapter","created":{"date-parts":[[2020,8,12]],"date-time":"2020-08-12T20:03:45Z","timestamp":1597262625000},"page":"409-423","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Examples of the Application of Formal Methods to Interactive Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5567-9650","authenticated-orcid":false,"given":"Michael D.","family":"Harrison","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,8,13]]},"reference":[{"key":"31_CR1","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, 888\u2013906 (2012)","journal-title":"Int. J. Hum. Comput Stud."},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"Bowen, J., Reeves, S.: Design patterns for models of interactive systems. In: 2015 24th Australasian Software Engineering Conference (ASWEC), pp. 223\u2013232. IEEE (2015)","DOI":"10.1109\/ASWEC.2015.30"},{"key":"31_CR3","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1023\/A:1011265604021","volume":"8","author":"JC Campos","year":"2001","unstructured":"Campos, J.C., Harrison, M.D.: Model checking interactor specifications. Autom. Softw. Eng. 8, 275\u2013310 (2001)","journal-title":"Autom.. Softw. Eng."},{"issue":"2","key":"31_CR4","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1109\/THMS.2015.2421511","volume":"46","author":"JC Campos","year":"2016","unstructured":"Campos, J.C., Sousa, M., Alves, M.C.B., Harrison, M.D.: Formal verification of a space system\u2019s user interface with the IVY workbench. IEEE Trans. Hum. Mach. Syst. 46(2), 303\u2013316 (2016)","journal-title":"IEEE Trans. Hum. Mach. Syst."},{"key":"31_CR5","doi-asserted-by":"crossref","unstructured":"Campos, J., Sousa, N.: The MAL interactors animator: supporting model validation through animation. In: Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems, pp. 11:1\u201311:7. ACM (2018)","DOI":"10.1145\/3220134.3220142"},{"key":"31_CR6","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-7091-6878-3_8","volume-title":"Design, Specification and Verification of Interactive Systems 1997","author":"JC Campos","year":"1997","unstructured":"Campos, J.C., Harrison, M.D.: Formally verifying interactive systems: a review. In: Harrison, M., Torres, J. (eds.) Design, Specification and Verification of Interactive Systems 1997, pp. 119\u2013134. Springer, Vienna (1997). \nhttps:\/\/doi.org\/10.1007\/978-3-7091-6878-3_8"},{"key":"31_CR7","unstructured":"Cimatti, A., et al.: NuSMV 2.3 user manual. Technical report, ITC-IRST, Trento, Italy (2007). \nhttp:\/\/nusmv.irst.itc.it\/NuSMV\/tutorial\/v23\/tutorial.pdf"},{"key":"31_CR8","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"31_CR9","doi-asserted-by":"crossref","unstructured":"Couto, R., Campos, J.: IVY 2 - a model-based analysis tool. In: The 11th ACM SIGCHI Symposium on Engineering Interactive Computing Systems - EICS 2019, pp. 5:1\u20135:6. ACM (2019)","DOI":"10.1145\/3319499.3328228"},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"Dwyer, M., Avrunin, G., Corbett, J.: Property specification patterns for finite-state verification. In: Ardis, M. (ed.) 2nd Workshop on Formal Methods in Software Practice, pp. 7\u201315, March 1998","DOI":"10.1145\/298595.298598"},{"key":"31_CR11","doi-asserted-by":"publisher","unstructured":"Fayollas, C., et al.: Evaluation of formal IDEs for human-machine interface design and analysis: the case of CIRCUS and PVSio-web. In: Proceedings of the Third Workshop on Formal Integrated Development Environment. Electronic Proceedings in Theoretical Computer Science, vol. 240, pp. 1\u201319 (2017). \nhttps:\/\/doi.org\/10.4204\/EPTCS.240.1","DOI":"10.4204\/EPTCS.240.1"},{"key":"31_CR12","unstructured":"Freitas, L., Stabler, A.: Translation strategies for medical device control software. Technical report, Newcastle University, August 2015"},{"key":"31_CR13","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8, 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"Harrison, M.D., Campos, J.C., Loer, K.: Formal analysis of interactive systems: opportunities and weaknesses. In: Cairns, P., Cox, A. (eds.) Research Methods for Human Computer Interaction, Chap. 5, pp. 88\u2013111. Cambridge University Press, Cambridge (2008)","DOI":"10.1017\/CBO9780511814570.006"},{"key":"31_CR15","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.scico.2019.02.003","volume":"175","author":"MD Harrison","year":"2019","unstructured":"Harrison, M.D., Freitas, L., Drinnan, M., Campos, J.C., Masci, P., di Maria, C., Whitaker, M.: Formal techniques in the safety analysis of software components of a new dialysis machine. Sci. Comput. Program. 175, 17\u201334 (2019)","journal-title":"Sci. Comput. Program."},{"volume-title":"Formal Methods in Human Computer Interaction","year":"1990","key":"31_CR16","unstructured":"Harrison, M.D., Thimbleby, H.W. (eds.): Formal Methods in Human Computer Interaction. Cambridge University Press, Cambridge (1990)"},{"key":"31_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-030-04771-9_21","volume-title":"Software Technologies: Applications and Foundations","author":"MD Harrison","year":"2018","unstructured":"Harrison, M.D., Masci, P., Campos, J.C.: Formal modelling as a component of user centred design. In: Mazzara, M., Ober, I., Sala\u00fcn, G. (eds.) STAF 2018. LNCS, vol. 11176, pp. 274\u2013289. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-030-04771-9_21"},{"issue":"8","key":"31_CR18","doi-asserted-by":"publisher","first-page":"802","DOI":"10.1109\/TSE.2018.2804939","volume":"45","author":"M Harrison","year":"2019","unstructured":"Harrison, M., Masci, P., Campos, J.: Verification templates for the analysis of user interface software design. IEEE Trans. Software Eng. 45(8), 802\u2013822 (2019)","journal-title":"IEEE Trans. Software Eng."},{"issue":"3","key":"31_CR19","first-page":"26","volume":"1","author":"GE Krasner","year":"1988","unstructured":"Krasner, G.E., Pope, S.T.: A cookbook for using the model-view controller user interface paradigm in smalltalk-80. JOOP 1(3), 26\u201349 (1988)","journal-title":"JOOP"},{"issue":"4","key":"31_CR20","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/s10515-006-7999-y","volume":"13","author":"K Loer","year":"2006","unstructured":"Loer, K., Harrison, M.: An integrated framework for the analysis of dependable interactive systems (IFADIS): its tool support and evaluation. Autom. Softw. Eng. 13(4), 469\u2013496 (2006)","journal-title":"Autom. Softw. Eng."},{"key":"31_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-319-21690-4_30","volume-title":"Computer Aided Verification","author":"P Masci","year":"2015","unstructured":"Masci, P., Oladimeji, P., Zhang, Y., Jones, P., Curzon, P., Thimbleby, H.: PVSio-web 2.0: joining PVS to HCI. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 470\u2013478. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21690-4_30"},{"key":"31_CR22","volume-title":"Improving Your Human-Computer Interface: A Practical Technique","author":"A Monk","year":"1993","unstructured":"Monk, A., Wright, P., Haber, J., Davenport, L.: Improving Your Human-Computer Interface: A Practical Technique. Prentice-Hall, New York (1993)"},{"key":"31_CR23","doi-asserted-by":"crossref","unstructured":"Nielsen, J., Molich, R.: Heuristic evaluation of user interfaces. In: Chew, J., Whiteside, J. (eds.) ACM CHI Proceedings CHI 1990: Empowering People, pp. 249\u2013256 (1990)","DOI":"10.1145\/97243.97281"},{"issue":"1","key":"31_CR24","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s10009-015-0374-110.1007\/s10009-015-0374-1","volume":"18","author":"A Osaiweran","year":"2016","unstructured":"Osaiweran, A., Schuts, M., Hooman, J., Groote, J.F., van Rijnsoever, B.: Evaluating the effect of a lightweight formal technique in industry. Int. J. Softw. Tools Technol. Transfer 18(1), 93\u2013108 (2016). \nhttps:\/\/doi.org\/10.1007\/s10009-015-0374-110.1007\/s10009-015-0374-1","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"31_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). \nhttps:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"31_CR26","unstructured":"Owre, S., Shankar, N.: Writing PVS proof strategies. In: Design and Application of Strategies\/Tactics in Higher Order Logics (STRATA 2003), Number CP-2003-212448 in NASA Conference Publication, pp. 1\u201315 (2003)"},{"key":"31_CR27","series-title":"Formal Approaches to Computing and Information Technology Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3425-1","volume-title":"Formal Methods in Human-Computer Interaction","year":"1998","unstructured":"Palanque, P., Patern\u00f2, F. (eds.): Formal Methods in Human-Computer Interaction. Formal Approaches to Computing and Information Technology Series. Springer, London (1998). \nhttps:\/\/doi.org\/10.1007\/978-1-4471-3425-1"},{"key":"31_CR28","unstructured":"Shankar, N., Owre, S., Rushby, J.M., Stringer-Calvert, D.: PVS System Guide, PVS Language Reference, PVS Prover Guide, PVS Prelude Library, Abstract Datatypes in PVS, and Theory Interpretations in PVS. Computer Science Laboratory, SRI International, Menlo Park, CA (1999). \nhttp:\/\/pvs.csl.sri.com\/documentation.shtml"},{"key":"31_CR29","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-1-4471-0279-3_30","volume-title":"Tools for Working with Guidelines","author":"M van Welie","year":"2001","unstructured":"van Welie, M., van der Veer, G.C., Eli\u00ebns, A.: Patterns as tools for user interface design. In: Vanderdonckt, J., Farenc, C. (eds.) Tools for Working with Guidelines, pp. 313\u2013324. Springer, London (2001). \nhttps:\/\/doi.org\/10.1007\/978-1-4471-0279-3_30"},{"key":"31_CR30","series-title":"Human\u2013Computer Interaction Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-51838-1","volume-title":"The Handbook of Formal Methods in Human-Computer Interaction","year":"2017","unstructured":"Weyers, B., Bowen, J., Dix, A., Palanque, P. (eds.): The Handbook of Formal Methods in Human-Computer Interaction. HIS. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-51838-1"},{"key":"31_CR31","doi-asserted-by":"crossref","unstructured":"Zamansky, A., Spichkova, M., Rodr\u00edguez-Navas, G., Herrmann, P., Blech, J.O.: Towards classification of lightweight formal methods. In: Damiani, E., Spanoudakis, G., Maciaszek, L. (eds.) Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2018), pp. 305\u2013313 (2018)","DOI":"10.5220\/0006770803050313"}],"container-title":["Lecture Notes in Computer Science","Formal Methods. FM 2019 International Workshops"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-54994-7_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,12]],"date-time":"2020-08-12T20:09:35Z","timestamp":1597262975000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-54994-7_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030549930","9783030549947"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-54994-7_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"13 August 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2019.inesctec.pt\/?page_id=84","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":"129","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":"44","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":"34% - 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":"5,5","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}