{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:22:51Z","timestamp":1755998571552,"version":"3.41.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"EICS","license":[{"start":{"date-parts":[[2022,6,14]],"date-time":"2022-06-14T00:00:00Z","timestamp":1655164800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Hum.-Comput. Interact."],"published-print":{"date-parts":[[2022,6,14]]},"abstract":"<jats:p>Critical systems, particularly aeronautical systems, contain newly highly interactive devices: for example, the new generation cockpits use sophisticated electronics. They are driven by complex reactive software applications able to react to various kinds of inputs and to provide a representation of their internal state. In this context, the certification processes described in DO-178C and in DO-333 give an important place to formal verification of the requirements of these systems. Many formal methods have been proposed for this verification. However properties related to the graphical elements of these systems like position, overlapping, color, etc. have not received the same attention as others like safety, liveness, reachability or boundary ones. In this paper, we propose an original approach based on deductive verification to check graphically oriented requirements. On the basis of a semantic of reactive applications based on the weakest precondition calculus, we propose an algorithm for the verification of graphical requirements. This algorithm is developed in the context of Smala\/Djnn: an environment for developing interactive systems. We illustrate our approach on the Traffic alert and Collision Avoidance System (TCAS), an aeronautical case study, and some of its graphical requirements.<\/jats:p>","DOI":"10.1145\/3534521","type":"journal-article","created":{"date-parts":[[2022,6,17]],"date-time":"2022-06-17T17:36:27Z","timestamp":1655487387000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Verification of Graphical Properties of Interactive Systems"],"prefix":"10.1145","volume":"6","author":[{"given":"Daniel","family":"Prun","sequence":"first","affiliation":[{"name":"ENAC, Universit\u00e9 de Toulouse, Toulouse, France"}]},{"given":"Pascal","family":"B\u00e9ger","sequence":"additional","affiliation":[{"name":"ENAC, Universit\u00e9 de Toulouse, Toulouse, France"}]}],"member":"320","published-online":{"date-parts":[[2022,6,17]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2013. ED 143 - Minimum Operational Performance Standards for Traffic Alert and Collision Avoidance System II (TCAS II). 2013. ED 143 - Minimum Operational Performance Standards for Traffic Alert and Collision Avoidance System II (TCAS II)."},{"key":"e_1_2_1_2_1","volume-title":"in Eurographics Workshop on Design, Specification, and Verification of Interactive Systems (DSVIS'98)","volume":"352","author":"Yamine","year":"1998","unstructured":"Yamine Ait-ameur, Patrick Girard , and Francis Jambon . 1998 . A Uniform Approach for Specification and Design of Interactive Systems: the B Method . In in Eurographics Workshop on Design, Specification, and Verification of Interactive Systems (DSVIS'98) , Vol. Proceedings (Eds, Markopoulos. 333-- 352 . Yamine Ait-ameur, Patrick Girard, and Francis Jambon. 1998. A Uniform Approach for Specification and Design of Interactive Systems: the B Method. In in Eurographics Workshop on Design, Specification, and Verification of Interactive Systems (DSVIS'98), Vol. Proceedings (Eds, Markopoulos. 333--352."},{"key":"e_1_2_1_3_1","volume-title":"The 2003 International Conference on Software Engineering Research and Practice - SERP 2003. CSREA Press.","author":"Ameur Yamine Ait","year":"2003","unstructured":"Yamine Ait Ameur , Mickael Baron , and Patrick Girard . 2003 . Formal validation of HCI user tasks. In In Al-Ani Ban, Arabnia H.R, and Mum Youngsong, editors , The 2003 International Conference on Software Engineering Research and Practice - SERP 2003. CSREA Press. Yamine Ait Ameur, Mickael Baron, and Patrick Girard. 2003. Formal validation of HCI user tasks. In In Al-Ani Ban, Arabnia H.R, and Mum Youngsong, editors, The 2003 International Conference on Software Engineering Research and Practice - SERP 2003. CSREA Press."},{"key":"e_1_2_1_4_1","volume-title":"MEA","author":"Antoine Philippe","year":"2017","unstructured":"Philippe Antoine and St\u00e9phane Conversy . 2017 . Volta: the first all-electric conventional helicopter . In MEA 2017, More Electric Aircraft. Bordeaux, France. https:\/\/hal-enac.archives-ouvertes.fr\/hal-01609233 Philippe Antoine and St\u00e9phane Conversy. 2017. Volta: the first all-electric conventional helicopter. In MEA 2017, More Electric Aircraft. Bordeaux, France. https:\/\/hal-enac.archives-ouvertes.fr\/hal-01609233"},{"key":"e_1_2_1_5_1","unstructured":"Pascal B\u00e9ger. 2020. V\u00e9rification formelle des propri\u00e9t\u00e9s graphiques des syst\u00e8mes informatiques interactifs. Theses. INSA Toulouse. https:\/\/tel.archives-ouvertes.fr\/tel-02990362 Pascal B\u00e9ger. 2020. V\u00e9rification formelle des propri\u00e9t\u00e9s graphiques des syst\u00e8mes informatiques interactifs. Theses. INSA Toulouse. https:\/\/tel.archives-ouvertes.fr\/tel-02990362"},{"key":"e_1_2_1_6_1","unstructured":"Jacques Bertin and Marc Barbut. 1973. S\u00e9miologie graphique: les diagrammes les r\u00e9seaux les cartes. Gauthier Villars. https:\/\/books.google.fr\/books?id=F4weAAAAMAAJ Jacques Bertin and Marc Barbut. 1973. S\u00e9miologie graphique: les diagrammes les r\u00e9seaux les cartes. Gauthier Villars. https:\/\/books.google.fr\/books?id=F4weAAAAMAAJ"},{"volume-title":"Formal Testing of Multimodal Interactive Systems","author":"Bouchet Jullien","key":"e_1_2_1_7_1","unstructured":"Jullien Bouchet , Laya Madani , Laurence Nigay , Catherine Oriat , and Ioannis Parissis . 2008. Formal Testing of Multimodal Interactive Systems . In Engineering Interactive Systems, Jan Gulliksen, Morton Borup Harning, Philippe Palanque, Gerrit C. van der Veer, and Janet Wesson (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 36--52. Jullien Bouchet, Laya Madani, Laurence Nigay, Catherine Oriat, and Ioannis Parissis. 2008. Formal Testing of Multimodal Interactive Systems. In Engineering Interactive Systems, Jan Gulliksen, Morton Borup Harning, Philippe Palanque, Gerrit C. van der Veer, and Janet Wesson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 36--52."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3095807"},{"key":"e_1_2_1_9_1","unstructured":"Fabrizio Banci Buonamici Gina Belmonte Vincenzo Ciancia Diego Latella and Mieke Massink. 2018. Spatial Logics and Model Checking for Medical Imaging (Extended Version). arXiv:1811.06065 [cs.LO] Fabrizio Banci Buonamici Gina Belmonte Vincenzo Ciancia Diego Latella and Mieke Massink. 2018. Spatial Logics and Model Checking for Medical Imaging (Extended Version). arXiv:1811.06065 [cs.LO]"},{"key":"e_1_2_1_10_1","volume-title":"Harrison","author":"Campos Jos\u00e9 Creissac","year":"1997","unstructured":"Jos\u00e9 Creissac Campos and Michael D . Harrison . 1997 . Formally verifying interactive systems: A review. In DSV-IS. Jos\u00e9 Creissac Campos and Michael D. Harrison. 1997. Formally verifying interactive systems: A review. In DSV-IS."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2774225.2774848"},{"key":"e_1_2_1_12_1","volume-title":"Model Checking Spatial Logics for Closure Spaces. 12 (09","author":"Ciancia Vincenzo","year":"2016","unstructured":"Vincenzo Ciancia , Diego Latella , Michele Loreti , and Mieke Massink . 2016. Model Checking Spatial Logics for Closure Spaces. 12 (09 2016 ). https:\/\/doi.org\/10.2168\/LMCS-12(4:2)2016 10.2168\/LMCS-12(4:2)2016 Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. 2016. Model Checking Spatial Logics for Closure Spaces. 12 (09 2016). https:\/\/doi.org\/10.2168\/LMCS-12(4:2)2016"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242587.3242623"},{"key":"e_1_2_1_15_1","first-page":"115","article-title":"Four easy pieces for assessing the usability of multimodal interaction: the CARE properties","volume":"95","author":"Coutaz Jo\u00eblle","year":"1995","unstructured":"Jo\u00eblle Coutaz , Laurence Nigay , Daniel Salber , Ann Blandford , Jon May , and Richard M Young . 1995 . Four easy pieces for assessing the usability of multimodal interaction: the CARE properties .. In InterAct , Vol. 95. 115 -- 120 . Jo\u00eblle Coutaz, Laurence Nigay, Daniel Salber, Ann Blandford, Jon May, and Richard M Young. 1995. Four easy pieces for assessing the usability of multimodal interaction: the CARE properties.. In InterAct, Vol. 95. 115--120.","journal-title":"InterAct"},{"volume-title":"Design, Specification and Verification of Interactive Systems '98","author":"Ausbourg Bruno","key":"e_1_2_1_16_1","unstructured":"Bruno d' Ausbourg . 1998. Using Model Checking for the Automatic Validation of User Interfaces Systems . In Design, Specification and Verification of Interactive Systems '98 , Panos Markopoulos and Peter Johnson (Eds.). Springer Vienna , Vienna , 242--260. Bruno d'Ausbourg. 1998. Using Model Checking for the Automatic Validation of User Interfaces Systems. In Design, Specification and Verification of Interactive Systems '98, Panos Markopoulos and Peter Johnson (Eds.). Springer Vienna, Vienna, 242--260."},{"key":"e_1_2_1_17_1","first-page":"337","article-title":"Z3: an efficient SMT solver","volume":"4963","author":"de Moura Leonardo","year":"2008","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner . 2008 . Z3: an efficient SMT solver . Tools and Algorithms for the Construction and Analysis of Systems 4963 , 337 -- 340 . https:\/\/doi.org\/10.1007\/978--3--540--78800--3_24 10.1007\/978--3--540--78800--3_24 Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: an efficient SMT solver. Tools and Algorithms for the Construction and Analysis of Systems 4963, 337--340. https:\/\/doi.org\/10.1007\/978--3--540--78800--3_24","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_19_1","volume-title":"Tom Van Cutsem, MOSTINCKX STIJN, and Wolfgang De Meuter.","author":"Engineer BAINOMUGISHA","year":"2012","unstructured":"BAINOMUGISHA Engineer , Andoni Lombide Carreton , Tom Van Cutsem, MOSTINCKX STIJN, and Wolfgang De Meuter. 2012 . A Survey on Reactive Programming. Comput. Surveys 45 (01 2012). https:\/\/doi.org\/10.1145\/ 2501654.2501666 BAINOMUGISHA Engineer, Andoni Lombide Carreton, Tom Van Cutsem, MOSTINCKX STIJN, and Wolfgang De Meuter. 2012. A Survey on Reactive Programming. Comput. Surveys 45 (01 2012). https:\/\/doi.org\/10.1145\/ 2501654.2501666"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/EDCC.2014.17"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Nadjet Kamel and Yamine Ait-Ameur. 2004. Mod\u00e8le formel g\u00e9n\u00e9ral pour le traitement d'interactions multimodales. In IHM 04. Namure Belgique 219--222. Nadjet Kamel and Yamine Ait-Ameur. 2004. Mod\u00e8le formel g\u00e9n\u00e9ral pour le traitement d'interactions multimodales. In IHM 04. Namure Belgique 219--222.","DOI":"10.1145\/1148613.1148651"},{"key":"e_1_2_1_24_1","volume-title":"INAIR 2019, 8th International Conference on Air Transport (Transportation Research Procedia","volume":"268","author":"Letondal Catherine","year":"2020","unstructured":"Catherine Letondal , Jean-Luc Vinot , Sylvain Pauchet , and S\u00e9bastien Leriche . 2020 . Exploring a touch-based flight control panel for pilots using tangible design principles . In INAIR 2019, 8th International Conference on Air Transport (Transportation Research Procedia , Vol. 43). Elsevier, Reno, NV, United States, pp 257-- 268 . https:\/\/doi.org\/10.1016\/j. trpro.2019.12.041 10.1016\/j Catherine Letondal, Jean-Luc Vinot, Sylvain Pauchet, and S\u00e9bastien Leriche. 2020. Exploring a touch-based flight control panel for pilots using tangible design principles. In INAIR 2019, 8th International Conference on Air Transport (Transportation Research Procedia, Vol. 43). Elsevier, Reno, NV, United States, pp 257--268. https:\/\/doi.org\/10.1016\/j. trpro.2019.12.041"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229094"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3102113.3102161"},{"key":"e_1_2_1_27_1","unstructured":"C\u00e9cile Marcon Nicolas Nalpon Cyril Allignol and C\u00e9lia Picard. 2021. Repr\u00e9sentation de programmes SMALA gr\u00e2ce \u00e0 la th\u00e9orie des bigraphes. In AFADL. En ligne France. https:\/\/hal-enac.archives-ouvertes.fr\/hal-03457039 C\u00e9cile Marcon Nicolas Nalpon Cyril Allignol and C\u00e9lia Picard. 2021. Repr\u00e9sentation de programmes SMALA gr\u00e2ce \u00e0 la th\u00e9orie des bigraphes. In AFADL. En ligne France. https:\/\/hal-enac.archives-ouvertes.fr\/hal-03457039"},{"volume-title":"Engineering distributed systems: how efficient is a computational model?","author":"Martin Alice","key":"e_1_2_1_28_1","unstructured":"Alice Martin and Mathieu Magnaudet . 2019. Engineering distributed systems: how efficient is a computational model? . In International Association for Computing and Philosophy - - Annual Meeting. Mexico, Mexico. https:\/\/hal-enac.archivesouvertes.fr\/hal-02127381 Alice Martin and Mathieu Magnaudet. 2019. Engineering distributed systems: how efficient is a computational model?. In International Association for Computing and Philosophy -- Annual Meeting. Mexico, Mexico. https:\/\/hal-enac.archivesouvertes.fr\/hal-02127381"},{"key":"#cr-split#-e_1_2_1_29_1.1","doi-asserted-by":"crossref","unstructured":"Alice Martin Mathieu Magnaudet and St\u00e9phane Conversy. 2021. Vers la compl\u00e9tude interactive: exigences pour une machine abstraite orient\u00e9e interaction: Toward Interactive Completeness: Requirements for an Interactive Abstract Machine. 1--6. https:\/\/doi.org\/10.1145\/3451148.3458644 10.1145\/3451148.3458644","DOI":"10.1145\/3451148.3458644"},{"key":"#cr-split#-e_1_2_1_29_1.2","doi-asserted-by":"crossref","unstructured":"Alice Martin Mathieu Magnaudet and St\u00e9phane Conversy. 2021. Vers la compl\u00e9tude interactive: exigences pour une machine abstraite orient\u00e9e interaction: Toward Interactive Completeness: Requirements for an Interactive Abstract Machine. 1--6. https:\/\/doi.org\/10.1145\/3451148.3458644","DOI":"10.1145\/3451148.3458644"},{"volume-title":"Joining PVS to HCI","author":"Masci Paolo","key":"e_1_2_1_30_1","unstructured":"Paolo Masci , Patrick Oladimeji , Yi Zhang , Paul Jones , Paul Curzon , and Harold Thimbleby . 2015. PVSio-web 2.0 : Joining PVS to HCI , Vol. 9206 . https:\/\/doi.org\/10.1007\/978--3--319--21690--4 10.1007\/978--3--319--21690--4 Paolo Masci, Patrick Oladimeji, Yi Zhang, Paul Jones, Paul Curzon, and Harold Thimbleby. 2015. PVSio-web 2.0: Joining PVS to HCI, Vol. 9206. https:\/\/doi.org\/10.1007\/978--3--319--21690--4"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640091"},{"key":"e_1_2_1_32_1","volume-title":"AFADL 2020 - 19\u00e8mes journ\u00e9es Approches Formelles dans l'Assistance au D\u00e9veloppement de Logiciels","author":"Nalpon Nicolas","year":"2020","unstructured":"Nicolas Nalpon , C\u00e9lia Picard , Cyril Allignol , and S\u00e9bastien Leriche . 2020 . Vers la v\u00e9rification de SMALA, un langage r\u00e9actif interactif . In AFADL 2020 - 19\u00e8mes journ\u00e9es Approches Formelles dans l'Assistance au D\u00e9veloppement de Logiciels . Vannes, France. https:\/\/hal-enac.archives-ouvertes.fr\/hal-02916890 Nicolas Nalpon, C\u00e9lia Picard, Cyril Allignol, and S\u00e9bastien Leriche. 2020. Vers la v\u00e9rification de SMALA, un langage r\u00e9actif interactif. In AFADL 2020 - 19\u00e8mes journ\u00e9es Approches Formelles dans l'Assistance au D\u00e9veloppement de Logiciels. Vannes, France. https:\/\/hal-enac.archives-ouvertes.fr\/hal-02916890"},{"key":"#cr-split#-e_1_2_1_33_1.1","doi-asserted-by":"crossref","unstructured":"Raquel Oliveira Sophie Dupuy-Chessa and Gaelle Calvary. 2015. Equivalence checking for comparing user interfaces. 266--275. https:\/\/doi.org\/10.1145\/2774225.2774844 10.1145\/2774225.2774844","DOI":"10.1145\/2774225.2774844"},{"key":"#cr-split#-e_1_2_1_33_1.2","doi-asserted-by":"crossref","unstructured":"Raquel Oliveira Sophie Dupuy-Chessa and Gaelle Calvary. 2015. Equivalence checking for comparing user interfaces. 266--275. https:\/\/doi.org\/10.1145\/2774225.2774844","DOI":"10.1145\/2774225.2774844"},{"key":"e_1_2_1_34_1","volume-title":"DIS '18, Designing Interactive Systems Conference (DIS '18 Proceedings of the 2018 Designing Interactive Systems Conference Pages 1193--1205). ACM, Hong-Kong, China, P.1193--1205","author":"Pauchet Sylvain","year":"1967","unstructured":"Sylvain Pauchet , Catherine Letondal , Jean-Luc Vinot , Micka\u00ebl Causse , Mathieu Cousy , Valentin Becquet , and Guillaume Crouzet . 2018. GazeForm: Dynamic Gaze-adaptive Touch Surface for Eyes-free Interaction in Airliner Cockpits . In DIS '18, Designing Interactive Systems Conference (DIS '18 Proceedings of the 2018 Designing Interactive Systems Conference Pages 1193--1205). ACM, Hong-Kong, China, P.1193--1205 ; ISBN : 978--1--4503--5198--0. https:\/\/doi.org\/10.1145\/3 1967 09. 3196712 10.1145\/3196709 Sylvain Pauchet, Catherine Letondal, Jean-Luc Vinot, Micka\u00ebl Causse, Mathieu Cousy, Valentin Becquet, and Guillaume Crouzet. 2018. GazeForm: Dynamic Gaze-adaptive Touch Surface for Eyes-free Interaction in Airliner Cockpits. In DIS '18, Designing Interactive Systems Conference (DIS '18 Proceedings of the 2018 Designing Interactive Systems Conference Pages 1193--1205). ACM, Hong-Kong, China, P.1193--1205 ; ISBN: 978--1--4503--5198--0. https:\/\/doi.org\/10.1145\/3196709. 3196712"},{"key":"e_1_2_1_35_1","unstructured":"David Randell and Anthony Cohn. 1989. Modelling Topological and Metrical Properties in Physical Processes. 357--368. David Randell and Anthony Cohn. 1989. Modelling Topological and Metrical Properties in Physical Processes. 357--368."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/3087223.3087240"},{"key":"#cr-split#-e_1_2_1_37_1.1","doi-asserted-by":"crossref","unstructured":"Guido Salvaneschi Gerold Hintz and Mira Mezini. 2014. REScala: bridging between object-oriented and functional style in reactive applications. 25--36. https:\/\/doi.org\/10.1145\/2584469.2577083 10.1145\/2584469.2577083","DOI":"10.1145\/2584469.2577083"},{"key":"#cr-split#-e_1_2_1_37_1.2","doi-asserted-by":"crossref","unstructured":"Guido Salvaneschi Gerold Hintz and Mira Mezini. 2014. REScala: bridging between object-oriented and functional style in reactive applications. 25--36. https:\/\/doi.org\/10.1145\/2584469.2577083","DOI":"10.1145\/2577080.2577083"},{"key":"e_1_2_1_38_1","unstructured":"RTCA (Firm). SC-205 and EUROCAE (Agency). Working Group 71. 2011. RTCA\/DO-178C Software Considerations in Airborne Systems and Equipment Certification. RTCA (Firm). SC-205 and EUROCAE (Agency). Working Group 71. 2011. RTCA\/DO-178C Software Considerations in Airborne Systems and Equipment Certification."},{"key":"e_1_2_1_39_1","unstructured":"RTCA (Firm). SC-205 and EUROCAE (Agency). Working Group 71. 2011. RTCA\/DO-333 Formal Methods Supplement to DO-178C and DO-278A. RTCA (Firm). SC-205 and EUROCAE (Agency). Working Group 71. 2011. RTCA\/DO-333 Formal Methods Supplement to DO-178C and DO-278A."},{"volume-title":"The Visual Display of Quantitative Information","author":"Tufte Edward R.","key":"e_1_2_1_40_1","unstructured":"Edward R. Tufte . 1986. The Visual Display of Quantitative Information . Graphics Press , Cheshire, CT, USA . Edward R. Tufte. 1986. The Visual Display of Quantitative Information. Graphics Press, Cheshire, CT, USA."},{"key":"e_1_2_1_41_1","volume-title":"Information Visualization: Perception for Design (3 ed.). Morgan Kaufmann","author":"Ware Colin","year":"2012","unstructured":"Colin Ware . 2012 . Information Visualization: Perception for Design (3 ed.). Morgan Kaufmann , Amsterdam . http: \/\/www.sciencedirect.com\/science\/book\/9780123814647 Colin Ware. 2012. Information Visualization: Perception for Design (3 ed.). Morgan Kaufmann, Amsterdam. http: \/\/www.sciencedirect.com\/science\/book\/9780123814647"},{"volume-title":"The Grammar of Graphics (Statistics and Computing)","author":"Wilkinson Leland","key":"e_1_2_1_42_1","unstructured":"Leland Wilkinson . 2005. The Grammar of Graphics (Statistics and Computing) . Springer-Verlag , Berlin, Heidelberg . Leland Wilkinson. 2005. The Grammar of Graphics (Statistics and Computing). Springer-Verlag, Berlin, Heidelberg."},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the 9th Australian Workshop on Safety Critical Systems and Software -","volume":"47","author":"Williams Ed","year":"2004","unstructured":"Ed Williams . 2004 . Airborne Collision Avoidance System . In Proceedings of the 9th Australian Workshop on Safety Critical Systems and Software - Volume 47 (Brisbane, Australia) (SCS '04). Australian Computer Society, Inc., Darlinghurst, Australia, Australia, 97--110. http:\/\/dl.acm.org\/citation.cfm?id=1082338.1082349 Ed Williams. 2004. Airborne Collision Avoidance System. In Proceedings of the 9th Australian Workshop on Safety Critical Systems and Software - Volume 47 (Brisbane, Australia) (SCS '04). Australian Computer Society, Inc., Darlinghurst, Australia, Australia, 97--110. http:\/\/dl.acm.org\/citation.cfm?id=1082338.1082349"}],"container-title":["Proceedings of the ACM on Human-Computer Interaction"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3534521","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3534521","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:09Z","timestamp":1750186809000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3534521"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,14]]},"references-count":46,"journal-issue":{"issue":"EICS","published-print":{"date-parts":[[2022,6,14]]}},"alternative-id":["10.1145\/3534521"],"URL":"https:\/\/doi.org\/10.1145\/3534521","relation":{},"ISSN":["2573-0142"],"issn-type":[{"type":"electronic","value":"2573-0142"}],"subject":[],"published":{"date-parts":[[2022,6,14]]},"assertion":[{"value":"2022-06-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}