{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,27]],"date-time":"2026-05-27T15:43:03Z","timestamp":1779896583621,"version":"3.53.1"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2016,5,28]],"date-time":"2016-05-28T00:00:00Z","timestamp":1464393600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Living with Digital Ubiquity platform","award":["EP\/M000877\/1"],"award-info":[{"award-number":["EP\/M000877\/1"]}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"crossref","award":["EP\/F033206\/1"],"award-info":[{"award-number":["EP\/F033206\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"name":"EPSRC Doctoral Prize Research Fellowship"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput.-Hum. Interact."],"published-print":{"date-parts":[[2016,5,28]]},"abstract":"<jats:p>While HCI has a long tradition of formally modelling task-based interactions with graphical user interfaces, there has been less progress in modelling emerging ubiquitous computing systems due in large part to their highly contextual nature and dependence on unreliable sensing systems. We present an exploration of modelling an example ubiquitous system, the Savannah game, using the mathematical formalism of bigraphs, which are based on a universal process algebra that encapsulates both dynamic and spatial behaviour of autonomous agents that interact and move among each other, or within each other. We establish a modelling approach based on four perspectives on ubiquitous systems\u2014Computational, Physical, Human, and Technology\u2014and explore how these interact with one another. We show how our model explains observed inconsistencies in user trials of Savannah, and then, how formal analysis reveals an incompleteness in design and guides extensions of the model and\/or possible system re-design to resolve this.<\/jats:p>","DOI":"10.1145\/2882784","type":"journal-article","created":{"date-parts":[[2016,5,31]],"date-time":"2016-05-31T12:15:09Z","timestamp":1464696909000},"page":"1-56","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["On Lions, Impala, and Bigraphs"],"prefix":"10.1145","volume":"23","author":[{"given":"Steve","family":"Benford","sequence":"first","affiliation":[{"name":"University of Nottingham, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Muffy","family":"Calder","sequence":"additional","affiliation":[{"name":"University of Glasgow, Glasgow, Scotland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tom","family":"Rodden","sequence":"additional","affiliation":[{"name":"University of Nottingham, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michele","family":"Sevegnani","sequence":"additional","affiliation":[{"name":"University of Glasgow, Glasgow, Scotland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2016,5,28]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0953-5438(92)90021-7"},{"key":"e_1_2_1_2_1","unstructured":"H. Alexander. 1987. Formally-Based Tools and Techniques for Human-Computer Dialogues. Ellis Horwood Limited.   H. Alexander. 1987. Formally-Based Tools and Techniques for Human-Computer Dialogues. Ellis Horwood Limited."},{"key":"e_1_2_1_3_1","series-title":"Lecture Notes in Computer Science","volume-title":"Quantitative Evaluation of Systems, Gethin Norman and William Sanders (Eds.)","author":"Andrei Oana","unstructured":"Oana Andrei , Muffy Calder , Matthew Higgs , and Mark Girolami . 2014. Probabilistic model checking of DTMC models of user activity patterns . In Quantitative Evaluation of Systems, Gethin Norman and William Sanders (Eds.) . Lecture Notes in Computer Science , Vol. 8657 . Springer International Publishing , 138--153. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-319-10696-0_11 10.1007\/978-3-319-10696-0_11 Oana Andrei, Muffy Calder, Matthew Higgs, and Mark Girolami. 2014. Probabilistic model checking of DTMC models of user activity patterns. In Quantitative Evaluation of Systems, Gethin Norman and William Sanders (Eds.). Lecture Notes in Computer Science, Vol. 8657. Springer International Publishing, 138--153. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-319-10696-0_11"},{"key":"e_1_2_1_4_1","volume-title":"Rajamani","author":"Ball Thomas","year":"2004","unstructured":"Thomas Ball , Byron Cook , Vladimir Levin , and Sriram K . Rajamani . 2004 . SLAM and static driver verifier: Technology transfer of formal methods inside Microsoft. In Integrated Formal Methods, Eerke A. Boiten, John Derrick, and Graeme Smith (Eds.). Lecture Notes in Computer Science, Vol. 2999 . Springer , Berlin, Germany, 1--20. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-24756-2_1 10.1007\/978-3-540-24756-2_1 Thomas Ball, Byron Cook, Vladimir Levin, and Sriram K. Rajamani. 2004. SLAM and static driver verifier: Technology transfer of formal methods inside Microsoft. In Integrated Formal Methods, Eerke A. Boiten, John Derrick, and Graeme Smith (Eds.). Lecture Notes in Computer Science, Vol. 2999. Springer, Berlin, Germany, 1--20. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-24756-2_1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/192426.192435"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/223904.223923"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1054972.1055072"},{"key":"e_1_2_1_8_1","first-page":"1","article-title":"Using formal verification to evaluate human-automation interaction, a review","volume":"99","author":"Bolton M. L.","year":"2013","unstructured":"M. L. Bolton , E. J. Bass , and R. I. Siminiceanu . 2013 . Using formal verification to evaluate human-automation interaction, a review . IEEE Trans. Syst. Man Cybern. A, Syst. Humans 99 , 1 -- 16 . M. L. Bolton, E. J. Bass, and R. I. Siminiceanu. 2013. Using formal verification to evaluate human-automation interaction, a review. IEEE Trans. Syst. Man Cybern. A, Syst. Humans 99, 1--16.","journal-title":"IEEE Trans. Syst. Man Cybern. A, Syst. Humans"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1821748.1821778"},{"key":"e_1_2_1_10_1","volume-title":"What use are formal design and analysis methods to telecommunications services? In Feature Interactions in Telecommunications and Software Systems","author":"Calder M.","unstructured":"M. Calder . 1998. What use are formal design and analysis methods to telecommunications services? In Feature Interactions in Telecommunications and Software Systems , K. Kimbler and L. G. Bouma (Eds.), Vol. V . IOS Press , 23--31. M. Calder. 1998. What use are formal design and analysis methods to telecommunications services? In Feature Interactions in Telecommunications and Software Systems, K. Kimbler and L. G. Bouma (Eds.), Vol. V. IOS Press, 23--31."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2748144.2748392"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0270-3"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/358886.358895"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_62"},{"key":"e_1_2_1_15_1","volume-title":"Dix and Colin Runciman","author":"Alan","year":"1985","unstructured":"Alan J. Dix and Colin Runciman . 1985 . Abstract models of interactive systems. People and Computers: Designing the Interface, P. J. and S. Cook (Eds.). Cambridge University Press , 13--22. Alan J. Dix and Colin Runciman. 1985. Abstract models of interactive systems. People and Computers: Designing the Interface, P. J. and S. Cook (Eds.). Cambridge University Press, 13--22."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00779-003-0253-8"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180875.1180921"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.03.007"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92698-6_28"},{"key":"#cr-split#-e_1_2_1_20_1.1","doi-asserted-by":"crossref","unstructured":"S. Dupuy-Chessa G. Godet-Bar J.-L. Prez-Medina D. Rieu and D. Juras. 2010. A software engineering method for the design of mixed reality systems. In The Engineering of Mixed Reality Systems Emmanuel Dubois Philip Gray and Laurence Nigay (Eds.). Springer London 313--334. DOI:http:\/\/dx.doi.org\/ 10.1007\/978-1-84882-733-2_16 10.1007\/978-1-84882-733-2_16","DOI":"10.1007\/978-1-84882-733-2_16"},{"key":"#cr-split#-e_1_2_1_20_1.2","doi-asserted-by":"crossref","unstructured":"S. Dupuy-Chessa G. Godet-Bar J.-L. Prez-Medina D. Rieu and D. Juras. 2010. A software engineering method for the design of mixed reality systems. In The Engineering of Mixed Reality Systems Emmanuel Dubois Philip Gray and Laurence Nigay (Eds.). Springer London 313--334. DOI:http:\/\/dx.doi.org\/ 10.1007\/978-1-84882-733-2_16","DOI":"10.1007\/978-1-84882-733-2_16"},{"key":"e_1_2_1_21_1","unstructured":"D. Gentner and A. L. Stevens. 1983. Mental Models. Taylor & Francis.  D. Gentner and A. L. Stevens. 1983. Mental Models. Taylor & Francis."},{"key":"e_1_2_1_22_1","volume-title":"MAUI: an interface design tool based on matrix algebra","author":"Gow Jeremy","unstructured":"Jeremy Gow and Harold Thimbleby . 2005. MAUI: an interface design tool based on matrix algebra . In Computer-Aided Design of User Interfaces IV. Springer , 81--94. Jeremy Gow and Harold Thimbleby. 2005. MAUI: an interface design tool based on matrix algebra. In Computer-Aided Design of User Interfaces IV. Springer, 81--94."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1006\/jvlc.1996.0009"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 13th IFIP TC 13 International Conference on Human-Computer Interaction -","author":"Greenberg Saul","year":"2011","unstructured":"Saul Greenberg . 2011 . Opportunities for proxemic interactions in ubicomp . In Proceedings of the 13th IFIP TC 13 International Conference on Human-Computer Interaction - Volume Part I (INTERACT\u201911). Springer-Verlag, Berlin, Germany, 3--10. Saul Greenberg. 2011. Opportunities for proxemic interactions in ubicomp. In Proceedings of the 13th IFIP TC 13 International Conference on Human-Computer Interaction - Volume Part I (INTERACT\u201911). Springer-Verlag, Berlin, Germany, 3--10."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/210079.210088"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/97243.97284"},{"key":"e_1_2_1_27_1","volume-title":"The Hidden Dimension","author":"Hall Edward T.","unstructured":"Edward T. Hall . 1966. The Hidden Dimension . Anchor Books , New York . Edward T. Hall. 1966. The Hidden Dimension. Anchor Books, New York."},{"key":"e_1_2_1_28_1","volume-title":"The Social Logic of Space","author":"Hillier Bill","unstructured":"Bill Hillier and Julienne Hanson . 1984. The Social Logic of Space . Cambridge University Press. http:\/\/dx.doi.org\/10.1017\/CBO9780511597237 Cambridge Books Online . 10.1017\/CBO9780511597237 Bill Hillier and Julienne Hanson. 1984. The Social Logic of Space. Cambridge University Press. http:\/\/dx.doi.org\/10.1017\/CBO9780511597237 Cambridge Books Online."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362364.2362371"},{"key":"e_1_2_1_31_1","volume-title":"Cognition in the Wild","author":"Hutchins Edwin","unstructured":"Edwin Hutchins . 1995. Cognition in the Wild . MIT press . Edwin Hutchins. 1995. Cognition in the Wild. MIT press."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/235833.236054"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.10.006"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1958824.1958893"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-013-0202-2"},{"key":"e_1_2_1_36_1","volume-title":"The Space and Motion of Communicating Agents","author":"Milner Robin","unstructured":"Robin Milner . 2009. The Space and Motion of Communicating Agents . Cambridge University Press . Robin Milner. 2009. The Space and Motion of Communicating Agents. Cambridge University Press."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-7373(81)80022-3"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-7373(86)80028-1"},{"key":"e_1_2_1_40_1","unstructured":"Donald A. Norman. 1983. Some observations on mental models. Mental Models 7 112 7--14.  Donald A. Norman. 1983. Some observations on mental models. Mental Models 7 112 7--14."},{"key":"e_1_2_1_41_1","unstructured":"Donald A. Norman. 1988. The Psychology of Everyday Things. Basic books.  Donald A. Norman. 1988. The Psychology of Everyday Things. Basic books."},{"key":"e_1_2_1_42_1","volume-title":"Computer Aided Verification","author":"Owre Sam","unstructured":"Sam Owre , Sreeranga Rajan , John M. Rushby , Natarajan Shankar , and Mandayam Srivas . 1996. PVS: combining specification, proof checking, and model checking . In Computer Aided Verification . Springer , 411--414. Sam Owre, Sreeranga Rajan, John M. Rushby, Natarajan Shankar, and Mandayam Srivas. 1996. PVS: combining specification, proof checking, and model checking. In Computer Aided Verification. Springer, 411--414."},{"key":"e_1_2_1_43_1","volume-title":"Software Engineering","author":"Parnas David Lorge","year":"2008","unstructured":"David Lorge Parnas . 2008. Connecting good theory to good practice: Software documentation: A case study . In Software Engineering 2008 . Fachtagung des GI-Fachbereichs Softwaretechnik, 18.-22.2.2008 in M\u00fcnchen . 17--20. http:\/\/subs.emis.de\/LNI\/Proceedings\/Proceedings121\/article1978.html. David Lorge Parnas. 2008. Connecting good theory to good practice: Software documentation: A case study. In Software Engineering 2008. Fachtagung des GI-Fachbereichs Softwaretechnik, 18.-22.2.2008 in M\u00fcnchen. 17--20. http:\/\/subs.emis.de\/LNI\/Proceedings\/Proceedings121\/article1978.html."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/3019322"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2007.47"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0097-8493(99)00120-X"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.02.011"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/211382.211385"},{"key":"e_1_2_1_49_1","volume-title":"Geographic Information Systems: An Introduction","author":"Star Jeffrey","unstructured":"Jeffrey Star and John Estes . 1990. Geographic Information Systems: An Introduction . Prentice Hall , Englewood Cliffs , New Jersey. Jeffrey Star and John Estes. 1990. Geographic Information Systems: An Introduction. Prentice Hall, Englewood Cliffs, New Jersey."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1177\/030631289019003001"},{"key":"e_1_2_1_51_1","volume-title":"Plans and Situated Actions: The Problem of Human-Machine Communication","author":"Suchman Lucy A.","unstructured":"Lucy A. Suchman . 1987. Plans and Situated Actions: The Problem of Human-Machine Communication . Cambridge University Press . Lucy A. Suchman. 1987. Plans and Situated Actions: The Problem of Human-Machine Communication. Cambridge University Press."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(82)90014-4"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2383396"},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of ECCE8: 8th European Conference on Cognitive Ergonomics. European Association of Cognitive Ergonomics, 10--13","author":"Wright Peter C.","unstructured":"Peter C. Wright , Bob Fields , and Michael D. Harrison . 1996. Distributed information resources: a new approach to interaction modelling . In Proceedings of ECCE8: 8th European Conference on Cognitive Ergonomics. European Association of Cognitive Ergonomics, 10--13 . Peter C. Wright, Bob Fields, and Michael D. Harrison. 1996. Distributed information resources: a new approach to interaction modelling. In Proceedings of ECCE8: 8th European Conference on Cognitive Ergonomics. European Association of Cognitive Ergonomics, 10--13."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1207\/S15327051HCI1501_01"}],"container-title":["ACM Transactions on Computer-Human Interaction"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2882784","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2882784","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:04:28Z","timestamp":1750273468000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2882784"}},"subtitle":["Modelling Interactions in Physical\/Virtual Spaces"],"short-title":[],"issued":{"date-parts":[[2016,5,28]]},"references-count":56,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,5,28]]}},"alternative-id":["10.1145\/2882784"],"URL":"https:\/\/doi.org\/10.1145\/2882784","relation":{},"ISSN":["1073-0516","1557-7325"],"issn-type":[{"value":"1073-0516","type":"print"},{"value":"1557-7325","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,5,28]]},"assertion":[{"value":"2015-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-05-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}