{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T15:25:00Z","timestamp":1744039500122},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,4,3]],"date-time":"2013-04-03T00:00:00Z","timestamp":1364947200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2015,6]]},"DOI":"10.1007\/s11334-013-0202-2","type":"journal-article","created":{"date-parts":[[2013,4,2]],"date-time":"2013-04-02T10:44:21Z","timestamp":1364899461000},"page":"113-130","source":"Crossref","is-referenced-by-count":11,"title":["Using PVS to support the analysis of distributed cognition systems"],"prefix":"10.1007","volume":"11","author":[{"given":"Paolo","family":"Masci","sequence":"first","affiliation":[]},{"given":"Paul","family":"Curzon","sequence":"additional","affiliation":[]},{"given":"Dominic","family":"Furniss","sequence":"additional","affiliation":[]},{"given":"Ann","family":"Blandford","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,4,3]]},"reference":[{"key":"202_CR1","unstructured":"Formal specification of the London Ambulance Service in PVS (2012). http:\/\/tinyurl.com\/PVS-LAS"},{"key":"202_CR2","unstructured":"Bass EJ, Feigh KM, Gunter E, Rushby J (2011) Formal modeling and analysis for interactive hybrid systems. In: 4th International Workshop on Formal Methods for Interactive Systems"},{"key":"202_CR3","unstructured":"Bernardeschi C, Cassano L, Domenici A, Masci P (2010) Debugging PVS specifications of control logics via event-driven simulation. In: Proc. 1st Intl. Conf. on Computational Logics, Algebras, Programming, Tools, and Benchmarking (Computation Tools 2010)"},{"key":"202_CR4","doi-asserted-by":"crossref","unstructured":"Bernardeschi C, Masci P, Pfeifer H (2008) Early prototyping of wireless sensor network algorithms in pvs. In: Harrison MD, Sujan MA (eds) Proc. of SAFECOMP08, Lecture Notes in Computer Science, vol 5219, pp 346\u2013359. Springer, Berlin","DOI":"10.1007\/978-3-540-87698-4_29"},{"key":"202_CR5","doi-asserted-by":"crossref","unstructured":"Bernardeschi C, Masci P, Pfeifer H (2009) Analysis of wireless sensor network protocols in dynamic scenarios. In: Proc. of SSS09, Lecture Notes in Computer Science, vol 5873, pp 105\u2013119. Springer, Berlin","DOI":"10.1007\/978-3-642-05118-0_8"},{"key":"202_CR6","doi-asserted-by":"crossref","unstructured":"Blandford A, Furniss D (2006) DiCoT: A Methodology for Applying Distributed Cognition to the Design of Teamworking Systems. Interactive Systems, pp 26\u201338","DOI":"10.1007\/11752707_3"},{"key":"202_CR7","doi-asserted-by":"crossref","unstructured":"Bolton ML, Bass EJ (2010) Formally verifying human\u2013automation interaction as part of a system model: limitations and tradeoffs. Innovations in Systems and Software Engineering 6(3):219\u2013231. doi: 10.1007\/s11334-010-0129-9","DOI":"10.1007\/s11334-010-0129-9"},{"key":"202_CR8","doi-asserted-by":"crossref","unstructured":"Bolton ML, Bass EJ, Siminiceanu RI (2012) Generating phenotypical erroneous human behavior to evaluate human-automation interaction using model checking. Int J Hum Comput Stud. doi: 10.1016\/j.ijhcs.2012.05.010","DOI":"10.1016\/j.ijhcs.2012.05.010"},{"key":"202_CR9","doi-asserted-by":"crossref","unstructured":"Bolton ML, Bass EJ, Siminiceanu RI 2012 Using formal verification to evaluate human-automation interaction, a review. IEEE Trans Syst Man Cybern A Syst Hum. (in press)","DOI":"10.1109\/TSMCA.2012.2210406"},{"key":"202_CR10","doi-asserted-by":"crossref","unstructured":"Bolton ML, Siminiceanu RI, Bass EJ (2011) A systematic approach to model checking human-automation interaction using task analytic models. IEEE Trans Syst Man Cybern A Syst Hum 41(5): 961\u2013976","DOI":"10.1109\/TSMCA.2011.2109709"},{"key":"202_CR11","unstructured":"Butler R, Sjogren J (1998) A PVS Graph Theory Library. NASA Technical Memorandum 1998\u2013206923, NASA Langley Research Center, Hampton, Virginia"},{"key":"202_CR12","volume-title":"Evaluating, testing, and animating PVS specifications","author":"J Crow","year":"2001","unstructured":"Crow J, Owre S, Rushby J, Shankar N, Stringer-Calvert D (2001) Evaluating, testing, and animating PVS specifications. Tech. rep, Computer Science Laboratory, SRI International, Menlo Park"},{"key":"202_CR13","doi-asserted-by":"crossref","unstructured":"Dun H, Xu H, Wang L (2008) Transformation of BPEL Processes to Petri Nets. In: Theoretical Aspects of Software Engineering, 2008. TASE \u201908. 2nd IFIP\/IEEE International Symposium on, pp 166\u2013173","DOI":"10.1109\/TASE.2008.27"},{"key":"202_CR14","unstructured":"Fields R (2001) Analysis of erroneour actions in the design of critical systems. Ph.D. thesis, University of York"},{"issue":"2","key":"202_CR15","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1109\/TSC.2010.19","volume":"3","author":"H Foster","year":"2010","unstructured":"Foster H, Uchitel S, Magee J, Kramer J (2010) An integrated workbench for model-based engineering of service compositions. Services Comput IEEE Trans 3(2):131\u2013144","journal-title":"Services Comput IEEE Trans"},{"key":"202_CR16","unstructured":"Furniss D (2004) Codifying distributed cognition: A case study of emergency medical dispatch. Master\u2019s thesis, UCLIC, UCL Interaction Centre"},{"key":"202_CR17","doi-asserted-by":"crossref","first-page":"1174","DOI":"10.1080\/00140130600612663","volume":"49","author":"D Furniss","year":"2006","unstructured":"Furniss D, Blandford A (2006) Understanding emergency medical dispatch in terms of distributed cognition: a case study. Ergonomics J 49:1174\u20131203","journal-title":"Ergonomics J"},{"key":"202_CR18","unstructured":"Hutchins E (1995) Cognition in the Wild, new edn. The MIT Press. http:\/\/www.amazon.co.uk\/Cognition-Bradford-Books-Edwin-Hutchins\/dp\/0262581469"},{"key":"202_CR19","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1207\/s15516709cog1903_1","volume":"19","author":"E Hutchins","year":"1995","unstructured":"Hutchins E (1995) How a cockpit remembers its speed. Cognitive Sci 19:265\u2013288","journal-title":"Cognitive Sci"},{"key":"202_CR20","doi-asserted-by":"crossref","first-page":"513","DOI":"10.1207\/s15516709cog1804_1","volume":"18","author":"D Kirsh","year":"1994","unstructured":"Kirsh D, Maglio P (1994) On distinguishing epistemic from pragmatic action. Cognitive Sci 18:513\u2013549","journal-title":"Cognitive Sci"},{"key":"202_CR21","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen KG, Pettersson P, Yi W (1997) Uppaal in a nutshell. Int J Software Tools Technol Transf 1:134\u2013152","journal-title":"Int J Software Tools Technol Transf"},{"key":"202_CR22","doi-asserted-by":"crossref","unstructured":"Masci P, Curzon P (2011) Checking user-centred design principles in distributed cognition models: a case study in the healthcare domain. In: USAB 2011: Information Quality in eHealth, 7th Conference of the Austrian Computer Society. Springer Lecture Notes in Computer Science (LNCS)","DOI":"10.1007\/978-3-642-25364-5_10"},{"key":"202_CR23","unstructured":"Masci P, Curzon P, Blandford A, Furniss D (2011) Modelling distributed cognition systems in pvs. In: FMIS2011, the 4th Intl. Workshop on Formal Methods for Interactive Systems"},{"key":"202_CR24","doi-asserted-by":"crossref","unstructured":"Masci P, Furniss D, Curzon P, Harrison MD, Blandford A (2012) Supporting field investigators with PVS: a case study in the healthcare domain In: SERENE 2012: 4th International Workshop Software Engineering for Resilient Systems, Lecture Notes in Computer Science (LNCS)","DOI":"10.1007\/978-3-642-33176-3_11"},{"key":"202_CR25","doi-asserted-by":"crossref","unstructured":"Masci P, Huang H, Curzon P, Harrison M (2012) Using pvs to investigate incidents through the lens of distributed cognition. In: NASAFM 2012: 4th Nasa Formal Methods Symposium. Springer Lecture Notes in Computer Science (LNCS)","DOI":"10.1007\/978-3-642-28891-3_27"},{"key":"202_CR26","doi-asserted-by":"crossref","unstructured":"McKnight J, Doherty G (2008) Distributed cognition and mobile healthcare work. In: Proc. of BCS-HCI \u201908, pp 35\u201338. British Computer Society, Swinton, UK","DOI":"10.14236\/ewic\/HCI2008.28"},{"key":"202_CR27","doi-asserted-by":"crossref","unstructured":"de Moura L, Owre S, Ruess H, Rushby J, Shankar N, Sorea M, Tiwari A (2004) SAL 2. In: Alur R, Peled DA (eds) Computer Aided Verification: CAV 2004, Lecture Notes in Computer Science, vol 3114, pp 496\u2013500. Springer, Berlin","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"202_CR28","unstructured":"Movaghar A, Meyer J (1984) Performability modelling with stochastic activity networks. In: Proc of the 1984 Real-Time Systems, Symposium, pp 215\u2013224"},{"key":"202_CR29","unstructured":"Mu\u00f1oz C (2003) Rapid prototyping in PVS. Tech. Rep. NIA Report No. 2003\u201303, NASA\/CR-2003-212418, National Institute of Aerospace, Hampton, VA"},{"key":"202_CR30","doi-asserted-by":"crossref","unstructured":"Owre S, Rajan S, Rushby J, Shankar N, Srivas M (1996) PVS: combining specification, proof checking, and model checking. In: Alur R, Henzinger TA (eds) Computer-Aided Verification, CAV \u201996, no. 1102 in Lecture Notes in Computer Science, pp 411\u2013414. Springer-Verlag, New Brunswick, NJ","DOI":"10.1007\/3-540-61474-5_91"},{"key":"202_CR31","unstructured":"Priority Dispatch Corp. Inc. (2005) ProQA 3.4, emergency dispatch software. http:\/\/www.prioritydispatch.net\/support\/pdf\/ProQA_User_Guide.pdf"},{"key":"202_CR32","doi-asserted-by":"crossref","unstructured":"Rajkomar A, Blandford A (2012) Understanding infusion administration in the icu through distributed cognition. Journal of Biomedical Informatics (0). doi: 10.1016\/j.jbi.2012.02.003 . http:\/\/www.sciencedirect.com\/science\/article\/pii\/S15320464120","DOI":"10.1016\/j.jbi.2012.02.003"},{"key":"202_CR33","doi-asserted-by":"crossref","unstructured":"Rushby J (2002) Using model checking to help discover mode confusions and other automation surprises. Reliability Engineering and System Safety 75(2), 167\u2013177. Available at http:\/\/www.csl.sri.com\/users\/rushby\/abstracts\/ress02","DOI":"10.1016\/S0951-8320(01)00092-8"},{"key":"202_CR34","doi-asserted-by":"crossref","unstructured":"Rushby JM (2001) Modeling the human in human factors. In: SAFECOMP, pp 86\u201391","DOI":"10.1007\/3-540-45416-0_9"},{"key":"202_CR35","doi-asserted-by":"crossref","unstructured":"Shankar N, Owre S (1999) Principles and pragmatics of subtyping in PVS. In: Bert D, Choppy C, Mosses P (eds) Recent Trends in Algebraic Development Techniques, WADT \u201999, Lecture Notes in Computer Science, vol 1827. Springer, Toulouse, pp 37\u201352","DOI":"10.1007\/978-3-540-44616-3_3"},{"key":"202_CR36","doi-asserted-by":"crossref","unstructured":"Sharp H, Robinson H, Segal J, Furniss D (2006) The role of story cards and the wall in xp teams: A distributed cognition perspective. In: Proceedings of the conference on AGILE 2006, pp 65\u201375. IEEE Computer Society, Washington, DC, USA","DOI":"10.1109\/AGILE.2006.56"},{"key":"202_CR37","unstructured":"Vicente KJ (1999) Cognitive Work Analysis : Toward Safe, Productive, and Healthy Computer-Based Work. Lawrence Erlbaum, New Jersey"},{"key":"202_CR38","doi-asserted-by":"crossref","unstructured":"Werth J, Furniss D (2012) Medical equipment library design: revealing issues and best practice with DiCoT. International Health Informatics Symposium (IHI, In (2011)","DOI":"10.1145\/2110363.2110428"},{"key":"202_CR39","doi-asserted-by":"crossref","unstructured":"Westbrook JI, Ampt A (2009) Design, application and testing of the work observation method by activity timing (wombat) to measure clinicians\u2019 patterns of work and communication. Int J Med Inform 78. doi: 10.1016\/j.ijmedinf.2008.09.003","DOI":"10.1016\/j.ijmedinf.2008.09.003"},{"key":"202_CR40","unstructured":"Wright P, Fields B, Harrison MD (1996) Distributed information resources: A new approach to interaction modelling. In: Proceedings of ECCE8: European Conference on Cognitive Ergonomics, pp 5\u201310. EACE"},{"issue":"1","key":"202_CR41","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1207\/S15327051HCI1501_01","volume":"15","author":"P Wright","year":"2000","unstructured":"Wright P, Fields B, Harrison M (2000) Analyzing human-computer interaction as distributed cognition: the resources model. Hum Comput Intact J 15(1):1\u201342","journal-title":"Hum Comput Intact J"},{"key":"202_CR42","doi-asserted-by":"crossref","unstructured":"Wright P, Fields B, Merriam N (1997) From formal models to empirical evaluation and back again, chap. 13, pp 283\u2013314. Formal methods in human-computer interaction. Springer, Berlin","DOI":"10.1007\/978-1-4471-3425-1_14"},{"key":"202_CR43","doi-asserted-by":"crossref","unstructured":"Zha H, van der Aalst W, Wang J, Wen L, Sun J (2010) Verifying workflow processes: a transformation-based approach. Software and Systems Modeling pp 1\u201312. doi: 10.1007\/s10270-010-0149-9","DOI":"10.1007\/s10270-010-0149-9"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-013-0202-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-013-0202-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-013-0202-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,24]],"date-time":"2020-07-24T18:23:19Z","timestamp":1595614999000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-013-0202-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,4,3]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["202"],"URL":"https:\/\/doi.org\/10.1007\/s11334-013-0202-2","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,4,3]]}}}