{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,7]],"date-time":"2026-02-07T19:14:19Z","timestamp":1770491659632,"version":"3.49.0"},"reference-count":88,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T00:00:00Z","timestamp":1596412800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Competitiveness and Internationalisation","award":["POCI-01-0145-FEDER-016826"],"award-info":[{"award-number":["POCI-01-0145-FEDER-016826"]}]},{"name":"European Regional Development"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput.-Hum. Interact."],"published-print":{"date-parts":[[2020,10,31]]},"abstract":"<jats:p>Use error due to user interface design defects is a major concern in many safety critical domains, for example avionics and health care. Early detection of latent user interface problems can be facilitated by user-centered design methods that integrate formal verification technologies. This article considers the role that formal verification technologies can play in the context of user-centered design by considering the following three existing tools: CIRCUS, PVSio-web, and IVY. These tools have been developed to support the model based analysis of critical user interfaces. They have their foundations in existing formal verification technologies, but each of them is focused towards particular issues relating to user interface design. The article explores the different phases of the user-centered design process and the extent to which each of these tools supports these phases. Criteria are developed for assessing their role at each stage of the design process. The results of the evaluation provide guidance to developers to help choose the most appropriate tool based on their analysis needs while at the same time setting challenges for future developments.<\/jats:p>","DOI":"10.1145\/3404199","type":"journal-article","created":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T10:34:25Z","timestamp":1596450865000},"page":"1-48","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Supporting the Analysis of Safety Critical User Interfaces"],"prefix":"10.1145","volume":"27","author":[{"given":"Jos\u00e9 Creissac","family":"Campos","sequence":"first","affiliation":[{"name":"HASLab\/INESC TEC and Universidade do Minho"}]},{"given":"Camille","family":"Fayollas","sequence":"additional","affiliation":[{"name":"University of Toulouse"}]},{"given":"Michael D.","family":"Harrison","sequence":"additional","affiliation":[{"name":"Newcastle University"}]},{"given":"C\u00e9lia","family":"Martinie","sequence":"additional","affiliation":[{"name":"University of Toulouse"}]},{"given":"Paolo","family":"Masci","sequence":"additional","affiliation":[{"name":"National Institute of Aerospace"}]},{"given":"Philippe","family":"Palanque","sequence":"additional","affiliation":[{"name":"University of Toulouse"}]}],"member":"320","published-online":{"date-parts":[[2020,8,3]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 4th International Eurographics Workshop (Eurographics). M. D. Harrison and J. C. Torres (Eds.). Springer, 143--159","author":"Accot J.","unstructured":"J. Accot , S. Chatty , S. Maury , and P. Palanque . 1997. Formal transducers: Models of devices and building bricks for the design of highly interactive systems . In Proceedings of the 4th International Eurographics Workshop (Eurographics). M. D. Harrison and J. C. Torres (Eds.). Springer, 143--159 . DOI:https:\/\/doi.org\/10.1007\/978-3-7091-6878-3_10 10.1007\/978-3-7091-6878-3_10 J. Accot, S. Chatty, S. Maury, and P. Palanque. 1997. Formal transducers: Models of devices and building bricks for the design of highly interactive systems. In Proceedings of the 4th International Eurographics Workshop (Eurographics). M. D. Harrison and J. C. Torres (Eds.). Springer, 143--159. DOI:https:\/\/doi.org\/10.1007\/978-3-7091-6878-3_10"},{"key":"e_1_2_1_2_1","unstructured":"SAS Airbus. 2016. Airbus A380 Flight Crew Operating Manual. Retrieved from http:\/\/www.airbus.com\/.  SAS Airbus. 2016. Airbus A380 Flight Crew Operating Manual. Retrieved from http:\/\/www.airbus.com\/."},{"key":"e_1_2_1_3_1","volume-title":"ARINC 661 specification: Cockpit Display System Interfaces to User Systems","author":"Airlines Electronic Engineering Committee","unstructured":"Airlines Electronic Engineering Committee . 2002. ARINC 661 specification: Cockpit Display System Interfaces to User Systems . Aeronautical Radio Inc . Airlines Electronic Engineering Committee. 2002. ARINC 661 specification: Cockpit Display System Interfaces to User Systems. Aeronautical Radio Inc."},{"key":"#cr-split#-e_1_2_1_4_1.1","doi-asserted-by":"crossref","unstructured":"E. Barboni S. Conversy D. Navarre and P. Palanque. 2006. Model-based engineering of widgets user applications and servers compliant with ARINC 661 specification. In Interactive Systems. Design Specification and Verification. Springer 25--38. DOI:https:\/\/doi.org\/10.1007\/978-3-540-69554-7_3 10.1007\/978-3-540-69554-7_3","DOI":"10.1007\/978-3-540-69554-7_3"},{"key":"#cr-split#-e_1_2_1_4_1.2","doi-asserted-by":"crossref","unstructured":"E. Barboni S. Conversy D. Navarre and P. Palanque. 2006. Model-based engineering of widgets user applications and servers compliant with ARINC 661 specification. In Interactive Systems. Design Specification and Verification. Springer 25--38. DOI:https:\/\/doi.org\/10.1007\/978-3-540-69554-7_3","DOI":"10.1007\/978-3-540-69554-7_3"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 2nd ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201910)","author":"Barboni E.","year":"1822","unstructured":"E. Barboni , J.-F. Ladry , D. Navarre , P. Palanque , and M. Winckler . 2010. Beyond modelling: An integrated environment supporting co-execution of tasks and systems models . In Proceedings of the 2nd ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201910) . ACM, 165--174. DOI:https:\/\/doi.org\/10.1145\/ 1822 018.1822043 10.1145\/1822018.1822043 E. Barboni, J.-F. Ladry, D. Navarre, P. Palanque, and M. Winckler. 2010. Beyond modelling: An integrated environment supporting co-execution of tasks and systems models. In Proceedings of the 2nd ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201910). ACM, 165--174. DOI:https:\/\/doi.org\/10.1145\/1822018.1822043"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the HCI Aero Conference (HCI Aero\u201906)","author":"Barboni E.","unstructured":"E. Barboni , D. Navarre , P. Palanque , and S. Basnyat . 2006. Exploitation of formal specification techniques for ARINC 661 interactive cockpit applications . In Proceedings of the HCI Aero Conference (HCI Aero\u201906) . Cepadues, 81--89. E. Barboni, D. Navarre, P. Palanque, and S. Basnyat. 2006. Exploitation of formal specification techniques for ARINC 661 interactive cockpit applications. In Proceedings of the HCI Aero Conference (HCI Aero\u201906). Cepadues, 81--89."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 6th International Conference on Multimodal Interfaces (ICMI\u201904)","author":"Bastide R.","unstructured":"R. Bastide , D. Navarre , P. Palanque , A. Schyn , and P. Dragicevic . 2004. A model-based approach for real-time embedded multimodal systems in military aircrafts . In Proceedings of the 6th International Conference on Multimodal Interfaces (ICMI\u201904) . ACM, 243--250. DOI:https:\/\/doi.org\/10.1145\/1027933.1027974 10.1145\/1027933.1027974 R. Bastide, D. Navarre, P. Palanque, A. Schyn, and P. Dragicevic. 2004. A model-based approach for real-time embedded multimodal systems in military aircrafts. In Proceedings of the 6th International Conference on Multimodal Interfaces (ICMI\u201904). ACM, 243--250. DOI:https:\/\/doi.org\/10.1145\/1027933.1027974"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/332040.332473"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the International Conference on Human-Centred Software Engineering. Springer, 181--202","author":"Billman D.","unstructured":"D. Billman , C. Fayollas , M. Feary , C. Martinie , and P. Palanque . 2016. Complementary tools and techniques for supporting fitness-for-purpose of interactive critical systems . In Proceedings of the International Conference on Human-Centred Software Engineering. Springer, 181--202 . D. Billman, C. Fayollas, M. Feary, C. Martinie, and P. Palanque. 2016. Complementary tools and techniques for supporting fitness-for-purpose of interactive critical systems. In Proceedings of the International Conference on Human-Centred Software Engineering. Springer, 181--202."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the Human Factors and Ergonomics Society Annual Meeting.","volume":"60","author":"Billman D.","unstructured":"D. Billman , S.-C. Wu , and C. Fan . 2016. Representing work for device design and evaluation using biclustering . In Proceedings of the Human Factors and Ergonomics Society Annual Meeting. Vol. 60 . SAGE Publications, CA: Los Angeles, 138--142. D. Billman, S.-C. Wu, and C. Fan. 2016. Representing work for device design and evaluation using biclustering. In Proceedings of the Human Factors and Ergonomics Society Annual Meeting. Vol. 60. SAGE Publications, CA: Los Angeles, 138--142."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/12944.12948"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/THMS.2014.2329476"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"J. Bowen and S. Reeves. 2017. Combining models for interactive system modelling. In The Handbook of Formal Methods in Human-Computer Interaction. Springer 161--182.  J. Bowen and S. Reeves. 2017. Combining models for interactive system modelling. In The Handbook of Formal Methods in Human-Computer Interaction. Springer 161--182.","DOI":"10.1007\/978-3-319-51838-1_6"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijhcs.2013.10.005"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201916)","author":"Campos J. C.","unstructured":"J. C. Campos , C. Fayollas , C. Martinie , D. Navarre , P. Palanque , and M. Pinto . 2016. Systematic automation of scenario-based testing of user interfaces . In Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201916) . ACM, 138--148. DOI:https:\/\/doi.org\/10.1145\/2933242.2948735 10.1145\/2933242.2948735 J. C. Campos, C. Fayollas, C. Martinie, D. Navarre, P. Palanque, and M. Pinto. 2016. Systematic automation of scenario-based testing of user interfaces. In Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201916). ACM, 138--148. DOI:https:\/\/doi.org\/10.1145\/2933242.2948735"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011265604021"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"J. C. Campos and M. D. Harrison. 2008. Systematic analysis of control panel interfaces using formal tools. In Interactive Systems: Design Specification and Verification DSVIS\u201908 (LNCS) Vol. 5136. N. Graham and P. Palanque (Eds.). Springer 72--85.  J. C. Campos and M. D. Harrison. 2008. Systematic analysis of control panel interfaces using formal tools. In Interactive Systems: Design Specification and Verification DSVIS\u201908 (LNCS) Vol. 5136. N. Graham and P. Palanque (Eds.). Springer 72--85.","DOI":"10.1007\/978-3-540-70569-7_6"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 1st ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201909)","author":"Campos J. C.","unstructured":"J. C. Campos and M. D. Harrison . 2009. Interaction engineering using the IVY tool . In Proceedings of the 1st ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201909) . ACM, 35--44. DOI:https:\/\/doi.org\/10.1145\/1570433.1570442 10.1145\/1570433.1570442 J. C. Campos and M. D. Harrison. 2009. Interaction engineering using the IVY tool. In Proceedings of the 1st ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201909). ACM, 35--44. DOI:https:\/\/doi.org\/10.1145\/1570433.1570442"},{"key":"e_1_2_1_19_1","first-page":"225","article-title":"SCADE: Implementation and Applications. ISTE Ltd","volume":"6","author":"Camus J. L.","year":"2012","unstructured":"J. L. Camus . 2012 . SCADE: Implementation and Applications. ISTE Ltd , Chapter 6 , 225 -- 272 . J. L. Camus. 2012. SCADE: Implementation and Applications. ISTE Ltd, Chapter 6, 225--272.","journal-title":"Chapter"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM\u201905)","author":"Cerone A.","unstructured":"A. Cerone , P. A. Lindsay , and S. Connelly . 2005. Formal analysis of human-computer interaction using model-checking . In Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM\u201905) . IEEE, 352--361. A. Cerone, P. A. Lindsay, and S. Connelly. 2005. Formal analysis of human-computer interaction using model-checking. In Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM\u201905). IEEE, 352--361."},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the International Conference on Computer Aided Verification. Springer, 359--364","author":"Cimatti A.","unstructured":"A. Cimatti , E. Clarke , E. Giunchiglia , F. Giunchiglia , M. Pistore , M. Roveri , R. Sebastiani , and A. Tacchella . 2002. Nusmv 2: An opensource tool for symbolic model checking . In Proceedings of the International Conference on Computer Aided Verification. Springer, 359--364 . A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. 2002. Nusmv 2: An opensource tool for symbolic model checking. In Proceedings of the International Conference on Computer Aided Verification. Springer, 359--364."},{"key":"e_1_2_1_22_1","unstructured":"E. M. Clarke O. Grumberg and D. A. Peled. 1999. Model Checking. MIT Press.  E. M. Clarke O. Grumberg and D. A. Peled. 1999. Model Checking. MIT Press."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/THMS.2015.2424851"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 2018 CHI Conference on Human Factors in Computing Systems (CHI\u201918)","author":"Ledo","unstructured":"Ledo D., Houben S., Vermeulen J., Marquardt N., Oehlberg L., and Greenberg S . 2018. Evaluation strategies for HCI toolkit research . In Proceedings of the 2018 CHI Conference on Human Factors in Computing Systems (CHI\u201918) . ACM, New York, NY, Article Paper 36, 17 pages. DOI:https:\/\/doi.org\/10.1145\/3173574.3173610 10.1145\/3173574.3173610 Ledo D., Houben S., Vermeulen J., Marquardt N., Oehlberg L., and Greenberg S. 2018. Evaluation strategies for HCI toolkit research. In Proceedings of the 2018 CHI Conference on Human Factors in Computing Systems (CHI\u201918). ACM, New York, NY, Article Paper 36, 17 pages. DOI:https:\/\/doi.org\/10.1145\/3173574.3173610"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the 1998 International Conference on Software Engineering. K. Torii, K. Futatsugi, and R. A. Kemmerer (Eds.). IEEE Computer Society, 219--228","author":"Ausbourg B.","year":"1998","unstructured":"B. d\u2019 Ausbourg , C. Seguin , G. Durrieu , and P. Roch\u00e9 . 1998. Helping the automated validation process of user interfaces systems . In Proceedings of the 1998 International Conference on Software Engineering. K. Torii, K. Futatsugi, and R. A. Kemmerer (Eds.). IEEE Computer Society, 219--228 . DOI:https:\/\/doi.org\/10.1109\/ICSE. 1998 .671121 10.1109\/ICSE.1998.671121 B. d\u2019Ausbourg, C. Seguin, G. Durrieu, and P. Roch\u00e9. 1998. Helping the automated validation process of user interfaces systems. In Proceedings of the 1998 International Conference on Software Engineering. K. Torii, K. Futatsugi, and R. A. Kemmerer (Eds.). IEEE Computer Society, 219--228. DOI:https:\/\/doi.org\/10.1109\/ICSE.1998.671121"},{"key":"e_1_2_1_26_1","volume-title":"Taming HAL: Designing Interfaces Beyond","author":"Degani A.","year":"2001","unstructured":"A. Degani . 2003. Taming HAL: Designing Interfaces Beyond 2001 . Palgrave, Macmillan. A. Degani. 2003. Taming HAL: Designing Interfaces Beyond 2001. Palgrave, Macmillan."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1111\/1467-8659.1230025"},{"key":"#cr-split#-e_1_2_1_28_1.1","doi-asserted-by":"crossref","unstructured":"R. Fahssi C. Martinie and P. A. Palanque. 2015. Enhanced task modelling for systematic identification and explicit representation of human errors. In Proceedings of the 15th IFIP TC International Conference on Human-Computer Interaction.Lecture Notes in Computer Science J. Abascal S. D. J. Barbosa M. Fetter T. Gross P. A. Palanque and M. Winckler (Eds.) Vol. 9299. Springer 192--212. DOI:https:\/\/doi.org\/10.1007\/978-3-319-22723-8_16 10.1007\/978-3-319-22723-8_16","DOI":"10.1007\/978-3-319-22723-8_16"},{"key":"#cr-split#-e_1_2_1_28_1.2","doi-asserted-by":"crossref","unstructured":"R. Fahssi C. Martinie and P. A. Palanque. 2015. Enhanced task modelling for systematic identification and explicit representation of human errors. In Proceedings of the 15th IFIP TC International Conference on Human-Computer Interaction.Lecture Notes in Computer Science J. Abascal S. D. J. Barbosa M. Fetter T. Gross P. A. Palanque and M. Winckler (Eds.) Vol. 9299. Springer 192--212. DOI:https:\/\/doi.org\/10.1007\/978-3-319-22723-8_16","DOI":"10.1007\/978-3-319-22723-8_16"},{"key":"e_1_2_1_29_1","unstructured":"Camille Fayollas. 2015. Generic Software Architecture and Model-Based Approach for the Dependability of Interactive Critical Systems. (Architecture logicielle g\u00e9n\u00e9rique et approche \u00e0 base de mod\u00e8les pour la s\u00fbret\u00e9 de fonctionnement des syst\u00e8mes interactifs critiques). Ph.D. Dissertation. University of Toulouse France. Retrieved from https:\/\/tel.archives-ouvertes.fr\/tel-01241504.  Camille Fayollas. 2015. Generic Software Architecture and Model-Based Approach for the Dependability of Interactive Critical Systems. (Architecture logicielle g\u00e9n\u00e9rique et approche \u00e0 base de mod\u00e8les pour la s\u00fbret\u00e9 de fonctionnement des syst\u00e8mes interactifs critiques). Ph.D. Dissertation. University of Toulouse France. Retrieved from https:\/\/tel.archives-ouvertes.fr\/tel-01241504."},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"C. Fayollas C. Martinie D. Navarre and P. Palanque. 2015. A generic approach for assessing compatibility between task descriptions and interactive systems: Application to the effectiveness of a flight control unit. i-com 14 3 (2015) 170\u2013191.  C. Fayollas C. Martinie D. Navarre and P. Palanque. 2015. A generic approach for assessing compatibility between task descriptions and interactive systems: Application to the effectiveness of a flight control unit. i-com 14 3 (2015) 170\u2013191.","DOI":"10.1515\/icom-2015-0037"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"C. Fayollas C. Martinie P. Palanque E. Barboni R. Fahssi and A. Hamon. 2017. Exploiting action theory as a framework for analysis and design of formal methods approaches: Application to the CIRCUS integrated development environment. In The Handbook of Formal Methods in Human-Computer Interaction. B. Weyers J. Bowen A. J. Dix and P. Palanque (Eds.). Springer 465--504.  C. Fayollas C. Martinie P. Palanque E. Barboni R. Fahssi and A. Hamon. 2017. Exploiting action theory as a framework for analysis and design of formal methods approaches: Application to the CIRCUS integrated development environment. In The Handbook of Formal Methods in Human-Computer Interaction. B. Weyers J. Bowen A. J. Dix and P. Palanque (Eds.). Springer 465--504.","DOI":"10.1007\/978-3-319-51838-1_17"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/EDCC.2014.17"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 3rd Workshop on Formal Integrated Development Environment (Electronic Proceedings in Theoretical Computer Science).","volume":"240","author":"Fayollas C.","unstructured":"C. Fayollas , C. Martinie , P. Palanque , P. Masci , M. D. Harrison , J. C. Campos , and S. R. Silva . 2017. Evaluation of formal IDEs for human-machine interface design and analysis: The case of CIRCUS and PVSio-web . In Proceedings of the 3rd Workshop on Formal Integrated Development Environment (Electronic Proceedings in Theoretical Computer Science). Vol. 240 . 1--19. DOI:https:\/\/doi.org\/10.4204\/EPTCS.240.1 10.4204\/EPTCS.240.1 C. Fayollas, C. Martinie, P. Palanque, P. Masci, M. D. Harrison, J. C. Campos, and S. R. Silva. 2017. Evaluation of formal IDEs for human-machine interface design and analysis: The case of CIRCUS and PVSio-web. In Proceedings of the 3rd Workshop on Formal Integrated Development Environment (Electronic Proceedings in Theoretical Computer Science). Vol. 240. 1--19. DOI:https:\/\/doi.org\/10.4204\/EPTCS.240.1"},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems. 101--106","author":"Gimblett A.","unstructured":"A. Gimblett and H. W. Thimbleby . 2013. Applying theorem discovery to automatically find and check usability heuristics . In Proceedings of the 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems. 101--106 . A. Gimblett and H. W. Thimbleby. 2013. Applying theorem discovery to automatically find and check usability heuristics. In Proceedings of the 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems. 101--106."},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201913)","author":"Hamon A.","unstructured":"A. Hamon , P. Palanque , J. L. Silva , Y. Deleris , and E. Barboni . 2013. Formal description of multi-touch interactions . In Proceedings of the 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201913) . ACM, 207--216. DOI:https:\/\/doi.org\/10.1145\/2494603.2480311 10.1145\/2494603.2480311 A. Hamon, P. Palanque, J. L. Silva, Y. Deleris, and E. Barboni. 2013. Formal description of multi-touch interactions. In Proceedings of the 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201913). ACM, 207--216. DOI:https:\/\/doi.org\/10.1145\/2494603.2480311"},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the 13th IEEE International Conference on Industrial Informatics. IEEE, 980--987","author":"Hamon A.","year":"2015","unstructured":"A. Hamon , P. A. Palanque , and M. Cronel . 2015. Dependable multi-touch interactions in safety critical industrial contexts: Application to aeronautics . In Proceedings of the 13th IEEE International Conference on Industrial Informatics. IEEE, 980--987 . DOI:https:\/\/doi.org\/10.1109\/INDIN. 2015 .7281868 10.1109\/INDIN.2015.7281868 A. Hamon, P. A. Palanque, and M. Cronel. 2015. Dependable multi-touch interactions in safety critical industrial contexts: Application to aeronautics. In Proceedings of the 13th IEEE International Conference on Industrial Informatics. IEEE, 980--987. DOI:https:\/\/doi.org\/10.1109\/INDIN.2015.7281868"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201914)","author":"Hamon A.","unstructured":"A. Hamon , P.A. Palanque , M. Cronel , R. Andr\u00e9 , E. Barboni , and D. Navarre . 2014. Formal modelling of dynamic instantiation of input devices and interaction techniques: Application to multi-touch interactions . In Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201914) . F. Patern\u00f2, C. Santoro, and J. Ziegler (Eds.). ACM, 173--178. DOI:https:\/\/doi.org\/10.1145\/2607023.2610286 10.1145\/2607023.2610286 A. Hamon, P.A. Palanque, M. Cronel, R. Andr\u00e9, E. Barboni, and D. Navarre. 2014. Formal modelling of dynamic instantiation of input devices and interaction techniques: Application to multi-touch interactions. In Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201914). F. Patern\u00f2, C. Santoro, and J. Ziegler (Eds.). ACM, 173--178. DOI:https:\/\/doi.org\/10.1145\/2607023.2610286"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-013-0201-3"},{"key":"e_1_2_1_40_1","doi-asserted-by":"crossref","unstructured":"M. D. Harrison P. Masci and J. C. Campos. 2018. Formal modelling as a component of user interface design. In Software Technologies: Applications and Foundations STAF 2018 Collocated Workshops (Revised Selected Papers) (Lecture Notes in Computer Science) M. Mazzara I. Ober and G. Sala\u00fcn (Eds.). Lecture Notes in Computer Science vol. 11176. Springer Cham.  M. D. Harrison P. Masci and J. C. Campos. 2018. Formal modelling as a component of user interface design. In Software Technologies: Applications and Foundations STAF 2018 Collocated Workshops (Revised Selected Papers) (Lecture Notes in Computer Science) M. Mazzara I. Ober and G. Sala\u00fcn (Eds.). Lecture Notes in Computer Science vol. 11176. Springer Cham.","DOI":"10.1007\/978-3-030-04771-9_21"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2018.2804939"},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems. ACM, 194--203","author":"Harrison M. D.","unstructured":"M. D. Harrison , J. C. Campos , R. Ruksenas , and P. Curzon . 2016. Modelling information resources and their salience in medical device design . In Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems. ACM, 194--203 . M. D. Harrison, J. C. Campos, R. Ruksenas, and P. Curzon. 2016. Modelling information resources and their salience in medical device design. In Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems. ACM, 194--203."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.02.003"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/THMS.2017.2717910"},{"key":"e_1_2_1_45_1","volume-title":"FRAM: The Functional Resonance Analysis Method: Modelling Complex Socio-technical Systems","author":"Hollnagel E.","unstructured":"E. Hollnagel . 2017. FRAM: The Functional Resonance Analysis Method: Modelling Complex Socio-technical Systems . CRC Press . E. Hollnagel. 2017. FRAM: The Functional Resonance Analysis Method: Modelling Complex Socio-technical Systems. CRC Press."},{"key":"e_1_2_1_46_1","volume-title":"Constructing the User Interface with Statecharts","author":"Horrocks I.","unstructured":"I. Horrocks . 1999. Constructing the User Interface with Statecharts . Addison-Wesley Longman Publishing Co., Inc. I. Horrocks. 1999. Constructing the User Interface with Statecharts. Addison-Wesley Longman Publishing Co., Inc."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/24032.24033"},{"key":"e_1_2_1_48_1","volume-title":"Cognition in the Wild","author":"Hutchins E.","unstructured":"E. Hutchins . 1994. Cognition in the Wild . MIT Press . E. Hutchins. 1994. Cognition in the Wild. MIT Press."},{"key":"e_1_2_1_49_1","volume-title":"Proceedings of the INTERACT\u201993 and CHI\u201993 Conference on Human Factors in Computing Systems. 56","author":"Johnson P.","unstructured":"P. Johnson , S. Wilson , P. Markopoulos , and J. Pycock . 1993. Adept: Advanced design environment for prototyping with task models . In Proceedings of the INTERACT\u201993 and CHI\u201993 Conference on Human Factors in Computing Systems. 56 . P. Johnson, S. Wilson, P. Markopoulos, and J. Pycock. 1993. Adept: Advanced design environment for prototyping with task models. In Proceedings of the INTERACT\u201993 and CHI\u201993 Conference on Human Factors in Computing Systems. 56."},{"key":"e_1_2_1_50_1","doi-asserted-by":"crossref","unstructured":"B. Kirwan and L. Ainsworth. 1992. A Guide to Task Analysis. Taylor and Francis.  B. Kirwan and L. Ainsworth. 1992. A Guide to Task Analysis. Taylor and Francis.","DOI":"10.1201\/b16826"},{"key":"e_1_2_1_51_1","first-page":"3","article-title":"A cookbook for using the model-view controller user interface paradigm in smalltalk-80","volume":"1","author":"Krasner G. E.","year":"1988","unstructured":"G. E. Krasner and S. T. Pope . 1988 . A cookbook for using the model-view controller user interface paradigm in smalltalk-80 . Journal of Object Oriented Programming 1 , 3 (Aug. 1988), 26--49. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=50757.50759. G. E. Krasner and S. T. Pope. 1988. A cookbook for using the model-view controller user interface paradigm in smalltalk-80. Journal of Object Oriented Programming 1, 3 (Aug. 1988), 26--49. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=50757.50759.","journal-title":"Journal of Object Oriented Programming"},{"key":"e_1_2_1_52_1","unstructured":"T. Le Sergent A. Bouakaz and G. Goretkin. 2018. SCADE AADL.  T. Le Sergent A. Bouakaz and G. Goretkin. 2018. SCADE AADL."},{"key":"e_1_2_1_53_1","volume-title":"Proceedings of the 13th IFIP TC International Conference on Human-Computer Interaction, part III. Lecture Notes in Computer Science","volume":"6948","author":"Martinie C.","unstructured":"C. Martinie , E. Barboni , D. Navarre , P. Palanque , R. Fahssi , E. Poupart , and E. Cubero-Castan . 2014. Multi-models-based engineering of collaborative systems: Application to collision avoidance operations for spacecraft . In Proceedings of the 13th IFIP TC International Conference on Human-Computer Interaction, part III. Lecture Notes in Computer Science , Vol. 6948 , Springer, Berlin, 589--609. DOI:https:\/\/doi.org\/10.1007\/978-3-642-23765-2_40 10.1007\/978-3-642-23765-2_40 C. Martinie, E. Barboni, D. Navarre, P. Palanque, R. Fahssi, E. Poupart, and E. Cubero-Castan. 2014. Multi-models-based engineering of collaborative systems: Application to collision avoidance operations for spacecraft. In Proceedings of the 13th IFIP TC International Conference on Human-Computer Interaction, part III. Lecture Notes in Computer Science, Vol. 6948, Springer, Berlin, 589--609. DOI:https:\/\/doi.org\/10.1007\/978-3-642-23765-2_40"},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of the 13th IFIP TC International Conference on Human-Computer Interaction, part III. Lecture Notes in Computer Science","volume":"6948","author":"Martinie C.","unstructured":"C. Martinie , P. Palanque , and M. Winckler . 2011. Structuring and composition mechanisms to address scalability issues in task models . In Proceedings of the 13th IFIP TC International Conference on Human-Computer Interaction, part III. Lecture Notes in Computer Science , Vol. 6948 , Springer, Berlin, 589--609. DOI:https:\/\/doi.org\/10.1007\/978-3-642-23765-2_40 10.1007\/978-3-642-23765-2_40 C. Martinie, P. Palanque, and M. Winckler. 2011. Structuring and composition mechanisms to address scalability issues in task models. In Proceedings of the 13th IFIP TC International Conference on Human-Computer Interaction, part III. Lecture Notes in Computer Science, Vol. 6948, Springer, Berlin, 589--609. DOI:https:\/\/doi.org\/10.1007\/978-3-642-23765-2_40"},{"key":"e_1_2_1_55_1","volume-title":"Proceedings of the ACM on Human-Computer Interaction. DOI:https:\/\/doi.org\/10","author":"Martinie C.","unstructured":"C. Martinie , P. A. Palanque , E. Bouzekri , A. Cockburn , A. Canny , and E. Barboni . 2019. Analysing and demonstrating tool-supported customizable task notations . In Proceedings of the ACM on Human-Computer Interaction. DOI:https:\/\/doi.org\/10 .1145\/3331154 10.1145\/3331154 C. Martinie, P. A. Palanque, E. Bouzekri, A. Cockburn, A. Canny, and E. Barboni. 2019. Analysing and demonstrating tool-supported customizable task notations. In Proceedings of the ACM on Human-Computer Interaction. DOI:https:\/\/doi.org\/10.1145\/3331154"},{"key":"e_1_2_1_56_1","volume-title":"Proceedings of the 32nd International Conference on Computer Safety, Reliability, and Security. Lecture Notes in Computer Science, F. Bitsch, J. Guiochet, and M. Ka\u00e2niche (Eds.)","volume":"8153","author":"Martinie C.","unstructured":"C. Martinie , P. A. Palanque , M. Ragosta , M. A. Sujan , D. Navarre , and A. Pasquini . 2013. Understanding functional resonance through a federation of models: Preliminary findings of an avionics case study . In Proceedings of the 32nd International Conference on Computer Safety, Reliability, and Security. Lecture Notes in Computer Science, F. Bitsch, J. Guiochet, and M. Ka\u00e2niche (Eds.) , Vol. 8153 . Springer, 216--227. DOI:https:\/\/doi.org\/10.1007\/978-3-642-40793-2_20 10.1007\/978-3-642-40793-2_20 C. Martinie, P. A. Palanque, M. Ragosta, M. A. Sujan, D. Navarre, and A. Pasquini. 2013. Understanding functional resonance through a federation of models: Preliminary findings of an avionics case study. In Proceedings of the 32nd International Conference on Computer Safety, Reliability, and Security. Lecture Notes in Computer Science, F. Bitsch, J. Guiochet, and M. Ka\u00e2niche (Eds.), Vol. 8153. Springer, 216--227. DOI:https:\/\/doi.org\/10.1007\/978-3-642-40793-2_20"},{"key":"e_1_2_1_57_1","volume-title":"Proceedings ACM Symposium Engineering Interactive Systems (EICS\u201913)","author":"Masci P.","unstructured":"P. Masci , A. Ayoub , P. Curzon , M. D. Harrison , I. Lee , O. Sokolsky , and H. Thimbleby . 2013. Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example . In Proceedings ACM Symposium Engineering Interactive Systems (EICS\u201913) . ACM, 81--90. P. Masci, A. Ayoub, P. Curzon, M. D. Harrison, I. Lee, O. Sokolsky, and H. Thimbleby. 2013. Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. In Proceedings ACM Symposium Engineering Interactive Systems (EICS\u201913). ACM, 81--90."},{"key":"e_1_2_1_58_1","volume-title":"Proceedings of the Verisure 2015, Workshop on Verification and Assurance, Co-located with CAV.","author":"Masci P.","unstructured":"P. Masci , P. Mallozzi , F. L. De Angelis , G. Di Marzo Serugendo, and P. Curzon. 2015. Using PVSio-web and SAPERE for rapid prototyping of user interfaces in integrated clinical environments . In Proceedings of the Verisure 2015, Workshop on Verification and Assurance, Co-located with CAV. P. Masci, P. Mallozzi, F. L. De Angelis, G. Di Marzo Serugendo, and P. Curzon. 2015. Using PVSio-web and SAPERE for rapid prototyping of user interfaces in integrated clinical environments. In Proceedings of the Verisure 2015, Workshop on Verification and Assurance, Co-located with CAV."},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of the 27th International Conference on Computer Aided Verification. D. Kroening and S. C. P\u0103s\u0103reanu (Eds.). Springer, 470--478","author":"Masci P.","unstructured":"P. Masci , P. Oladimeji , Y. Zhang , P. Jones , P. Curzon , and H. Thimbleby . 2015. PVSio-web 2.0: Joining PVS to HCI . In Proceedings of the 27th International Conference on Computer Aided Verification. D. Kroening and S. C. P\u0103s\u0103reanu (Eds.). Springer, 470--478 . DOI:https:\/\/doi.org\/10.1007\/978-3-319-21690-4_30 Tool available at http:\/\/www.pvsioweb.org. 10.1007\/978-3-319-21690-4_30 P. Masci, P. Oladimeji, Y. Zhang, P. Jones, P. Curzon, and H. Thimbleby. 2015. PVSio-web 2.0: Joining PVS to HCI. In Proceedings of the 27th International Conference on Computer Aided Verification. D. Kroening and S. C. P\u0103s\u0103reanu (Eds.). Springer, 470--478. DOI:https:\/\/doi.org\/10.1007\/978-3-319-21690-4_30 Tool available at http:\/\/www.pvsioweb.org."},{"key":"e_1_2_1_60_1","volume-title":"Proceedings of the 3rd Workshop on Formal Integrated Development Environment (F-IDE), Satellite Workshop of Formal Methods 2016. Electronic Proceedings in Theoretical Computer Science (EPTCS).","author":"Mauro G.","unstructured":"G. Mauro , H. Thimbleby , A. Domenici , and C. Bernardeschi . 2016. Extending a user interface prototyping tool with automatic MISRA C code generation . In Proceedings of the 3rd Workshop on Formal Integrated Development Environment (F-IDE), Satellite Workshop of Formal Methods 2016. Electronic Proceedings in Theoretical Computer Science (EPTCS). G. Mauro, H. Thimbleby, A. Domenici, and C. Bernardeschi. 2016. Extending a user interface prototyping tool with automatic MISRA C code generation. In Proceedings of the 3rd Workshop on Formal Integrated Development Environment (F-IDE), Satellite Workshop of Formal Methods 2016. Electronic Proceedings in Theoretical Computer Science (EPTCS)."},{"key":"e_1_2_1_61_1","doi-asserted-by":"crossref","unstructured":"A. F. Monk M. Curry and P. C. Wright. 1991. Why industry doesn\u2019t use the wonderful notations we researchers have given them to reason about their designs. In User-centred Requirements for Software Engineering. D. J. Gilmore R. L. Winder and F. Detienne (Eds.). Springer 185--189.  A. F. Monk M. Curry and P. C. Wright. 1991. Why industry doesn\u2019t use the wonderful notations we researchers have given them to reason about their designs. In User-centred Requirements for Software Engineering. D. J. Gilmore R. L. Winder and F. Detienne (Eds.). Springer 185--189.","DOI":"10.1007\/978-3-662-03035-6_15"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2002.1027801"},{"key":"e_1_2_1_63_1","unstructured":"C. A. Mu\u00f1oz and R. Butler. 2003. Rapid prototyping in PVS. Retrieved from http:\/\/ntrs.nasa.gov\/search.jsp?R=20040046914 NASA\/CR-2003-212418 NIA Report No.2003-03.  C. A. Mu\u00f1oz and R. Butler. 2003. Rapid prototyping in PVS. Retrieved from http:\/\/ntrs.nasa.gov\/search.jsp?R=20040046914 NASA\/CR-2003-212418 NIA Report No.2003-03."},{"key":"e_1_2_1_64_1","doi-asserted-by":"crossref","unstructured":"D. Navarre P. Dragicevic P. Palanque R. Bastide and A. Schyn. 2005. Very-high-fidelity prototyping for both presentation and dialogue parts of multimodal interactive systems. In Engineering Human Computer Interaction and Interactive Systems. R. Bastide P. Palanque and J. Roth (Eds.). Springer Berlin 179--199.  D. Navarre P. Dragicevic P. Palanque R. Bastide and A. Schyn. 2005. Very-high-fidelity prototyping for both presentation and dialogue parts of multimodal interactive systems. In Engineering Human Computer Interaction and Interactive Systems. R. Bastide P. Palanque and J. Roth (Eds.). Springer Berlin 179--199.","DOI":"10.1007\/11431879_11"},{"key":"e_1_2_1_65_1","volume-title":"Proceedings of the 12th International Workshop on Rapid System Prototyping (RSP\u201901)","author":"Navarre D.","unstructured":"D. Navarre , P. Palanque , R. Bastide , and O. Sy . 2001. A model-based tool for interactive prototyping of highly interactive applications . In Proceedings of the 12th International Workshop on Rapid System Prototyping (RSP\u201901) . IEEE Computer Society, 136. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=882480.883731. D. Navarre, P. Palanque, R. Bastide, and O. Sy. 2001. A model-based tool for interactive prototyping of highly interactive applications. In Proceedings of the 12th International Workshop on Rapid System Prototyping (RSP\u201901). IEEE Computer Society, 136. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=882480.883731."},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/1614390.1614393"},{"key":"e_1_2_1_67_1","volume-title":"Proceedings of the 12th IEEE International Workshop on Rapid System Prototyping (RSP\u201901)","author":"Navarre D.","year":"2001","unstructured":"D. Navarre , P. A. Palanque , R. Bastide , and O. Sy . 2001. A model-based tool for interactive prototyping of highly interactive applications . In Proceedings of the 12th IEEE International Workshop on Rapid System Prototyping (RSP\u201901) . IEEE Computer Society, 136--141. DOI:https:\/\/doi.org\/10.1109\/IWRSP. 2001 .933851 10.1109\/IWRSP.2001.933851 D. Navarre, P. A. Palanque, R. Bastide, and O. Sy. 2001. A model-based tool for interactive prototyping of highly interactive applications. In Proceedings of the 12th IEEE International Workshop on Rapid System Prototyping (RSP\u201901). IEEE Computer Society, 136--141. DOI:https:\/\/doi.org\/10.1109\/IWRSP.2001.933851"},{"key":"e_1_2_1_68_1","volume-title":"Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction (CADE\u201911)","author":"Owre S.","unstructured":"S. Owre , J. M. Rushby , and N. Shankar . 1992. PVS: A prototype verification system . In Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction (CADE\u201911) . Springer, Berlin, 748--752. DOI:https:\/\/doi.org\/10.1007\/3-540-55602-8_217 10.1007\/3-540-55602-8_217 S. Owre, J. M. Rushby, and N. Shankar. 1992. PVS: A prototype verification system. In Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction (CADE\u201911). Springer, Berlin, 748--752. DOI:https:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"e_1_2_1_69_1","volume-title":"Proceedings of the 3rd ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201911)","author":"Palanque P.","year":"1996","unstructured":"P. Palanque , E. Barboni , C. Martinie , D. Navarre , and M. Winckler . 2011. A model-based approach for supporting engineering usability evaluation of interaction techniques . In Proceedings of the 3rd ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201911) . ACM, 21--30. DOI:https:\/\/doi.org\/10.1145\/ 1996 461.1996490 10.1145\/1996461.1996490 P. Palanque, E. Barboni, C. Martinie, D. Navarre, and M. Winckler. 2011. A model-based approach for supporting engineering usability evaluation of interaction techniques. In Proceedings of the 3rd ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS\u201911). ACM, 21--30. DOI:https:\/\/doi.org\/10.1145\/1996461.1996490"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0953-5438(97)00013-1"},{"key":"e_1_2_1_71_1","volume-title":"Proceedings of the International Conference on Software Engineering and Formal Methods. Springer, 423--437","author":"Palmieri M.","unstructured":"M. Palmieri , Cinzia B., and P. Masci . 2017. Co-simulation of semi-autonomous systems: The line follower robot case study . In Proceedings of the International Conference on Software Engineering and Formal Methods. Springer, 423--437 . M. Palmieri, Cinzia B., and P. Masci. 2017. Co-simulation of semi-autonomous systems: The line follower robot case study. In Proceedings of the International Conference on Software Engineering and Formal Methods. Springer, 423--437."},{"key":"e_1_2_1_72_1","volume-title":"Proceedings of the Software and Systems Modeling","author":"Palmieri M.","unstructured":"M. Palmieri , C. Bernardeschi , and P. Masci . 2019. A framework for FMI-based co-simulation of human\u2013machine interfaces . In Proceedings of the Software and Systems Modeling . Cambridge University Press, 1--23. M. Palmieri, C. Bernardeschi, and P. Masci. 2019. A framework for FMI-based co-simulation of human\u2013machine interfaces. In Proceedings of the Software and Systems Modeling. Cambridge University Press, 1--23."},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-019-00754-9"},{"key":"e_1_2_1_74_1","volume-title":"Proceedings of the conference on People and Computers VII. A. Monk, D. Diaper, and M. D. Harrison (Eds.). BCS HCI Specialist Group","author":"Patern\u00f2 F.","unstructured":"F. Patern\u00f2 and G. Faconti . 1992. On the use of LOTOS to describe graphical interaction . In Proceedings of the conference on People and Computers VII. A. Monk, D. Diaper, and M. D. Harrison (Eds.). BCS HCI Specialist Group , Cambridge University Press, 155--174. F. Patern\u00f2 and G. Faconti. 1992. On the use of LOTOS to describe graphical interaction. In Proceedings of the conference on People and Computers VII. A. Monk, D. Diaper, and M. D. Harrison (Eds.). BCS HCI Specialist Group, Cambridge University Press, 155--174."},{"key":"e_1_2_1_75_1","volume-title":"Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control. ACM, 267--268","author":"Rajhans A.","unstructured":"A. Rajhans , S. Avadhanula , A. Chutinan , P. J. Mosterman , and F. Zhang . 2018. Graphical hybrid automata with simulink and stateflow . In Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control. ACM, 267--268 . A. Rajhans, S. Avadhanula, A. Chutinan, P. J. Mosterman, and F. Zhang. 2018. Graphical hybrid automata with simulink and stateflow. In Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control. ACM, 267--268."},{"key":"e_1_2_1_76_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69968-9","volume-title":"Petri Nets: An Introduction. EATCS Monographs on Theoretical Computer Science","author":"Reisig W.","year":"1985","unstructured":"W. Reisig . 1985 . Petri Nets: An Introduction. EATCS Monographs on Theoretical Computer Science , Vol. 4 . Springer . DOI:https:\/\/doi.org\/10.1007\/978-3-642-69968-9 10.1007\/978-3-642-69968-9 W. Reisig. 1985. Petri Nets: An Introduction. EATCS Monographs on Theoretical Computer Science, Vol. 4. Springer. DOI:https:\/\/doi.org\/10.1007\/978-3-642-69968-9"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.4271\/2009-01-3140"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-008-0102-7"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0951-8320(01)00092-8"},{"key":"e_1_2_1_80_1","volume-title":"Theoretical Aspects of Computer Software. Lecture Notes in Computer Science","volume":"526","author":"Ryan M.","unstructured":"M. Ryan , J. Fiadeiro , and T. Maibaum . 1991. Sharing actions and attributes in modal action logic . In Theoretical Aspects of Computer Software. Lecture Notes in Computer Science , Vol. 526 . Springer, 569--593. M. Ryan, J. Fiadeiro, and T. Maibaum. 1991. Sharing actions and attributes in modal action logic. In Theoretical Aspects of Computer Software. Lecture Notes in Computer Science, Vol. 526. Springer, 569--593."},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijhcs.2014.02.001"},{"key":"e_1_2_1_82_1","volume-title":"Electronic Communications of the EASST","volume":"69","author":"Silva J. L.","unstructured":"J. L. Silva , C. Fayollas , A. Hamon , P. A. Palanque , C. Martinie , and E. Barboni . 2013. Analysis of WIMP and post WIMP interactive systems based on formal specification . In Electronic Communications of the EASST , Vol. 69 . MIT press. DOI:https:\/\/doi.org\/10.14279\/tuj.eceasst.69.967 10.14279\/tuj.eceasst.69.967 J. L. Silva, C. Fayollas, A. Hamon, P. A. Palanque, C. Martinie, and E. Barboni. 2013. Analysis of WIMP and post WIMP interactive systems based on formal specification. In Electronic Communications of the EASST, Vol. 69. MIT press. DOI:https:\/\/doi.org\/10.14279\/tuj.eceasst.69.967"},{"key":"e_1_2_1_84_1","volume-title":"Press on: Principles of Interaction Programming","author":"Thimbleby H. W.","unstructured":"H. W. Thimbleby . 2007. Press on: Principles of Interaction Programming . MIT Press . H. W. Thimbleby. 2007. Press on: Principles of Interaction Programming. MIT Press."},{"key":"e_1_2_1_85_1","volume-title":"Cognitive Work Analysis","author":"Vicente K. J.","unstructured":"K. J. Vicente . 1999. Cognitive Work Analysis . Lawrence Erlbaum Associates . K. J. Vicente. 1999. Cognitive Work Analysis. Lawrence Erlbaum Associates."},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1006\/ijhc.2001.0474"},{"key":"e_1_2_1_87_1","volume-title":"S. Dobson, J. L. Fernandez-Marquez, A. Ferscha, M. Mamei, S. Marianib, A. Molesinib, S. Montagnab, J. Nieminenc, D. Pianinib, M. Risoldid, A. Rosia, G. Stevensone& J. Yee.","author":"Zambonelli F.","year":"2015","unstructured":"F. Zambonelli , A. Omicini , B. Anzengruber , G. Castelli , F. L. De Angelis , G. Di Marzo Serugendo , S. Dobson, J. L. Fernandez-Marquez, A. Ferscha, M. Mamei, S. Marianib, A. Molesinib, S. Montagnab, J. Nieminenc, D. Pianinib, M. Risoldid, A. Rosia, G. Stevensone& J. Yee. 2015 . Developing pervasive multi-agent systems with nature-inspired coordination. Pervasive and Mobile Computing 17, Part B (2015), 236--252. F. Zambonelli, A. Omicini, B. Anzengruber, G. Castelli, F. L. De Angelis, G. Di Marzo Serugendo, S. Dobson, J. L. Fernandez-Marquez, A. Ferscha, M. Mamei, S. Marianib, A. Molesinib, S. Montagnab, J. Nieminenc, D. Pianinib, M. Risoldid, A. Rosia, G. Stevensone& J. Yee. 2015. Developing pervasive multi-agent systems with nature-inspired coordination. Pervasive and Mobile Computing 17, Part B (2015), 236--252."}],"container-title":["ACM Transactions on Computer-Human Interaction"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3404199","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3404199","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:42Z","timestamp":1750195902000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3404199"}},"subtitle":["An Exploration of Three Formal Tools"],"short-title":[],"issued":{"date-parts":[[2020,8,3]]},"references-count":88,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2020,10,31]]}},"alternative-id":["10.1145\/3404199"],"URL":"https:\/\/doi.org\/10.1145\/3404199","relation":{},"ISSN":["1073-0516","1557-7325"],"issn-type":[{"value":"1073-0516","type":"print"},{"value":"1557-7325","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,8,3]]},"assertion":[{"value":"2019-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-08-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}