• Formal Verification of Astronaut-Rover Teams for Planetary Surface Operations

      Webster, Matt; Dennis, Louise A; Dixon, Clare; Fisher, Michael; Stocker, Richard; Sierhuis, Maarten; University of Liverpool; University of Chester; Ejenta, inc.
      This paper describes an approach to assuring the reliability of autonomous systems for Astronaut-Rover (ASRO) teams using the formal verification of models in the Brahms multi-agent modelling language. Planetary surface rovers have proven essential to several manned and unmanned missions to the moon and Mars. The first rovers were tele- or manuallyoperated, but autonomous systems are increasingly being used to increase the effectiveness and range of rover operations on missions such as the NASA Mars Science Laboratory. It is anticipated that future manned missions to the moon and Mars will use autonomous rovers to assist astronauts during extravehicular activity (EVA), including science, technical and construction operations. These ASRO teams have the potential to significantly increase the safety and efficiency of surface operations. We describe a new Brahms model in which an autonomous rover may perform several different activities including assisting an astronaut during EVA. These activities compete for the autonomous rovers “attention’ and therefore the rover must decide which activity is currently the most important and engage in that activity. The Brahms model also includes an astronaut agent, which models an astronauts predicted behaviour during an EVA. The rover must also respond to the astronauts activities. We show how this Brahms model can be simulated using the Brahms integrated development environment. The model can then also be formally verified with respect to system requirements using the SPIN model checker, through automatic translation from Brahms to PROMELA (the input language for SPIN). We show that such formal verification can be used to determine that mission- and safety critical operations are conducted correctly, and therefore increase the reliability of autonomous systems for planetary rovers in ASRO teams.
    • ParaVR: A Virtual Reality Training Simulator for Paramedic Skills maintenance

      Rees, Nigel; Dorrington, Keith; Rees, Lloyd; Day, Thomas W; Vaughan, Neil; John, Nigel W; Welsh Ambulance Services NHS Trust, University of Chester
      Background, Virtual Reality (VR) technology is emerging as a powerful educational tool which is used in medical training and has potential benefits for paramedic practice education. Aim The aim of this paper is to report development of ParaVR, which utilises VR to address skills maintenance for paramedics. Methods Computer scientists at the University of Chester and the Welsh Ambulance Services NHS Trust (WAST) developed ParaVR in four stages: 1. Identifying requirements and specifications 2. Alpha version development, 3. Beta version development 4. Management: Development of software, further funding and commercialisation. Results Needle Cricothyrotomy and Needle Thoracostomy emerged as candidates for the prototype ParaVR. The Oculus Rift head mounted display (HMD) combined with Novint Falcon haptic device was used, and a virtual environment crafted using 3D modelling software, ported (a computing term meaning transfer (software) from one system or machine to another) onto Oculus Go and Google cardboard VR platform. Conclusion VR is an emerging educational tool with the potential to enhance paramedic skills development and maintenance. The ParaVR program is the first step in our development, testing, and scaling up of this technology.
    • Quantification of the pressures generated during insertion of an epidural needle in labouring women of varying body mass indices

      Wee, M. Y. K.; Isaacs, R. A.; Vaughan, Neil; Dubey, V. N.; Parker, B.; University of Chester; Bournemouth University; Poole Hospital NHS Trust; West Hertfordshire NHS Trust; Southampton University Hospital (Heighten Science Publications, 2017-12-01)
      Objective: The primary aim of this study was to measure pressure generated on a Tuohy needle during the epidural procedure in labouring women of varying body mass indices (BMI) with a view of utilising the data for the future development of a high fi delity epidural simulator. High-fi delity epidural simulators have a role in improving training and safety but current simulators lack a realistic experience and can be improved. Methods: This study was approved by the National Research Ethics Service Committee South Central, Portsmouth (REC reference 11/SC/0196). After informed consent epidural needle insertion pressure was measured using a Portex 16-gauge Tuohy needle, loss-of-resistance syringe, a three-way tap, pressure transducer and a custom-designed wireless transmitter. This was performed in four groups of labouring women, stratified according to BMI kg/m2: 18-24.9; 25-34.9; 35-44.9 and >=45. One-way ANOVA was used to compare difference in needle insertion pressure between the BMI groups. A paired t-test was performed between BMI group 18-24.9 and the three other BMI groups. Ultrasound images of the lumbar spine were undertaken prior to the epidural procedure and lumbar magnetic resonance imaging (MRI) was performed within 72h post-delivery. These images will be used in the development of a high fi delity epidural simulator. Results: The mean epidural needle insertion pressure of labouring women with BMI 18-24.9 was 461mmHg; BMI 25-34.9 was 430mmHg; BMI 35-44.9 was 415mmHg and BMI >=45 was 376mmHg, (p=0.52). Conclusion: Although statistically insignifi cant, the study did show a decreasing trend of epidural insertion pressure with increasing body mass indices.