Skip to main content
Erschienen in: Innovations in Systems and Software Engineering 2/2015

01.06.2015 | SI: FMIS

Using PVS to support the analysis of distributed cognition systems

verfasst von: Paolo Masci, Paul Curzon, Dominic Furniss, Ann Blandford

Erschienen in: Innovations in Systems and Software Engineering | Ausgabe 2/2015

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

The rigorous analysis of socio-technical systems is challenging, because people are inherent parts of the system, together with devices and artefacts. In this paper, we report on the use of PVS as a way of analysing such systems in terms of distributed cognition. Distributed cognition is a conceptual framework that allows us to derive insights about plausible user trajectories in socio-technical systems by exploring what information in the environment provides resources for user action, but its application has traditionally required substantial craft skill. DiCoT adds structure and method to the analysis of socio-technical systems from a distributed cognition perspective. In this work, we demonstrate how PVS can be used with DiCoT to conduct a systematic analysis. We illustrate how a relatively simple use of PVS can help a field researcher to (i) externalise assumptions and facts, (ii) verify the consistency of the logical argument framed in the descriptions, (iii) help uncover latent situations that may warrant further investigation, and (iv) verify conjectures about potential hazards linked to the observed use of information resources. Evidence is also provided that formal methods and empirical studies are not alternative approaches for studying a socio-technical system, but that they can complement and refine each other. The combined use of PVS and DiCoT is illustrated through a case study concerning a real-world emergency medical dispatch system.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Fußnoten
1
Field study data considered here consist of written notes produced by the field investigator during the observations.
 
Literatur
2.
Zurück zum Zitat 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 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
3.
Zurück zum Zitat 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) 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)
4.
Zurück zum Zitat 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–359. Springer, Berlin 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–359. Springer, Berlin
5.
Zurück zum Zitat 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–119. Springer, Berlin 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–119. Springer, Berlin
6.
Zurück zum Zitat Blandford A, Furniss D (2006) DiCoT: A Methodology for Applying Distributed Cognition to the Design of Teamworking Systems. Interactive Systems, pp 26–38 Blandford A, Furniss D (2006) DiCoT: A Methodology for Applying Distributed Cognition to the Design of Teamworking Systems. Interactive Systems, pp 26–38
7.
Zurück zum Zitat Bolton ML, Bass EJ (2010) Formally verifying human–automation interaction as part of a system model: limitations and tradeoffs. Innovations in Systems and Software Engineering 6(3):219–231. doi:10.1007/s11334-010-0129-9 Bolton ML, Bass EJ (2010) Formally verifying human–automation interaction as part of a system model: limitations and tradeoffs. Innovations in Systems and Software Engineering 6(3):219–231. doi:10.​1007/​s11334-010-0129-9
8.
Zurück zum Zitat 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 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
9.
Zurück zum Zitat 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) 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)
10.
Zurück zum Zitat 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–976 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–976
11.
Zurück zum Zitat Butler R, Sjogren J (1998) A PVS Graph Theory Library. NASA Technical Memorandum 1998–206923, NASA Langley Research Center, Hampton, Virginia Butler R, Sjogren J (1998) A PVS Graph Theory Library. NASA Technical Memorandum 1998–206923, NASA Langley Research Center, Hampton, Virginia
12.
Zurück zum Zitat 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 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
13.
Zurück zum Zitat Dun H, Xu H, Wang L (2008) Transformation of BPEL Processes to Petri Nets. In: Theoretical Aspects of Software Engineering, 2008. TASE ’08. 2nd IFIP/IEEE International Symposium on, pp 166–173 Dun H, Xu H, Wang L (2008) Transformation of BPEL Processes to Petri Nets. In: Theoretical Aspects of Software Engineering, 2008. TASE ’08. 2nd IFIP/IEEE International Symposium on, pp 166–173
14.
Zurück zum Zitat Fields R (2001) Analysis of erroneour actions in the design of critical systems. Ph.D. thesis, University of York Fields R (2001) Analysis of erroneour actions in the design of critical systems. Ph.D. thesis, University of York
15.
Zurück zum Zitat 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–144 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–144
16.
Zurück zum Zitat Furniss D (2004) Codifying distributed cognition: A case study of emergency medical dispatch. Master’s thesis, UCLIC, UCL Interaction Centre Furniss D (2004) Codifying distributed cognition: A case study of emergency medical dispatch. Master’s thesis, UCLIC, UCL Interaction Centre
17.
Zurück zum Zitat Furniss D, Blandford A (2006) Understanding emergency medical dispatch in terms of distributed cognition: a case study. Ergonomics J 49:1174–1203 Furniss D, Blandford A (2006) Understanding emergency medical dispatch in terms of distributed cognition: a case study. Ergonomics J 49:1174–1203
19.
Zurück zum Zitat Hutchins E (1995) How a cockpit remembers its speed. Cognitive Sci 19:265–288 Hutchins E (1995) How a cockpit remembers its speed. Cognitive Sci 19:265–288
20.
Zurück zum Zitat Kirsh D, Maglio P (1994) On distinguishing epistemic from pragmatic action. Cognitive Sci 18:513–549 Kirsh D, Maglio P (1994) On distinguishing epistemic from pragmatic action. Cognitive Sci 18:513–549
21.
Zurück zum Zitat Larsen KG, Pettersson P, Yi W (1997) Uppaal in a nutshell. Int J Software Tools Technol Transf 1:134–152MATH Larsen KG, Pettersson P, Yi W (1997) Uppaal in a nutshell. Int J Software Tools Technol Transf 1:134–152MATH
22.
Zurück zum Zitat 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) 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)
23.
Zurück zum Zitat 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 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
24.
Zurück zum Zitat 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) 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)
25.
Zurück zum Zitat 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) 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)
26.
Zurück zum Zitat McKnight J, Doherty G (2008) Distributed cognition and mobile healthcare work. In: Proc. of BCS-HCI ’08, pp 35–38. British Computer Society, Swinton, UK McKnight J, Doherty G (2008) Distributed cognition and mobile healthcare work. In: Proc. of BCS-HCI ’08, pp 35–38. British Computer Society, Swinton, UK
27.
Zurück zum Zitat 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–500. Springer, Berlin 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–500. Springer, Berlin
28.
Zurück zum Zitat Movaghar A, Meyer J (1984) Performability modelling with stochastic activity networks. In: Proc of the 1984 Real-Time Systems, Symposium, pp 215–224 Movaghar A, Meyer J (1984) Performability modelling with stochastic activity networks. In: Proc of the 1984 Real-Time Systems, Symposium, pp 215–224
29.
Zurück zum Zitat Muñoz C (2003) Rapid prototyping in PVS. Tech. Rep. NIA Report No. 2003–03, NASA/CR-2003-212418, National Institute of Aerospace, Hampton, VA Muñoz C (2003) Rapid prototyping in PVS. Tech. Rep. NIA Report No. 2003–03, NASA/CR-2003-212418, National Institute of Aerospace, Hampton, VA
30.
Zurück zum Zitat 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 ’96, no. 1102 in Lecture Notes in Computer Science, pp 411–414. Springer-Verlag, New Brunswick, NJ 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 ’96, no. 1102 in Lecture Notes in Computer Science, pp 411–414. Springer-Verlag, New Brunswick, NJ
34.
Zurück zum Zitat Rushby JM (2001) Modeling the human in human factors. In: SAFECOMP, pp 86–91 Rushby JM (2001) Modeling the human in human factors. In: SAFECOMP, pp 86–91
35.
Zurück zum Zitat 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 ’99, Lecture Notes in Computer Science, vol 1827. Springer, Toulouse, pp 37–52 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 ’99, Lecture Notes in Computer Science, vol 1827. Springer, Toulouse, pp 37–52
36.
Zurück zum Zitat 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–75. IEEE Computer Society, Washington, DC, USA 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–75. IEEE Computer Society, Washington, DC, USA
37.
Zurück zum Zitat Vicente KJ (1999) Cognitive Work Analysis : Toward Safe, Productive, and Healthy Computer-Based Work. Lawrence Erlbaum, New Jersey Vicente KJ (1999) Cognitive Work Analysis : Toward Safe, Productive, and Healthy Computer-Based Work. Lawrence Erlbaum, New Jersey
38.
Zurück zum Zitat Werth J, Furniss D (2012) Medical equipment library design: revealing issues and best practice with DiCoT. International Health Informatics Symposium (IHI, In (2011) Werth J, Furniss D (2012) Medical equipment library design: revealing issues and best practice with DiCoT. International Health Informatics Symposium (IHI, In (2011)
39.
Zurück zum Zitat Westbrook JI, Ampt A (2009) Design, application and testing of the work observation method by activity timing (wombat) to measure clinicians’ patterns of work and communication. Int J Med Inform 78. doi:10.1016/j.ijmedinf.2008.09.003 Westbrook JI, Ampt A (2009) Design, application and testing of the work observation method by activity timing (wombat) to measure clinicians’ patterns of work and communication. Int J Med Inform 78. doi:10.​1016/​j.​ijmedinf.​2008.​09.​003
40.
Zurück zum Zitat 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–10. EACE 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–10. EACE
41.
Zurück zum Zitat Wright P, Fields B, Harrison M (2000) Analyzing human-computer interaction as distributed cognition: the resources model. Hum Comput Intact J 15(1):1–42 Wright P, Fields B, Harrison M (2000) Analyzing human-computer interaction as distributed cognition: the resources model. Hum Comput Intact J 15(1):1–42
42.
Zurück zum Zitat Wright P, Fields B, Merriam N (1997) From formal models to empirical evaluation and back again, chap. 13, pp 283–314. Formal methods in human-computer interaction. Springer, Berlin Wright P, Fields B, Merriam N (1997) From formal models to empirical evaluation and back again, chap. 13, pp 283–314. Formal methods in human-computer interaction. Springer, Berlin
43.
Zurück zum Zitat 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–12. doi:10.1007/s10270-010-0149-9 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–12. doi:10.​1007/​s10270-010-0149-9
Metadaten
Titel
Using PVS to support the analysis of distributed cognition systems
verfasst von
Paolo Masci
Paul Curzon
Dominic Furniss
Ann Blandford
Publikationsdatum
01.06.2015
Verlag
Springer London
Erschienen in
Innovations in Systems and Software Engineering / Ausgabe 2/2015
Print ISSN: 1614-5046
Elektronische ISSN: 1614-5054
DOI
https://doi.org/10.1007/s11334-013-0202-2

Weitere Artikel der Ausgabe 2/2015

Innovations in Systems and Software Engineering 2/2015 Zur Ausgabe

Editorial

Preface