Reusing models and properties in the analysis of similar
Contents
1. however the cost of using an infusion device extends beyond making a good deal on price and ongoing main tenance The work described here is part of the ongoing analysis of a range of infusion devices with the aim of re ducing these costs Part of this process should include a comparison with empirical techniques and with usabil ity evaluation methods in terms of the range problems that can be uncovered by these different methods Acknowledgements This project was inspired by the goals of and partly funded by the CHI MED project Multidisci plinary Computer Human Interaction Research for the de sign and safe use of interactive medical devices project UK EPSRC Grant Number EP G059063 1 Computing resources and office space were also provided to Michael Harrison at Newcastle University Patrick Oladimeji of Swansea Univer sity provided help with the Alaris pump and Chris Vincent of UCL provided access to the B Braun simulation References 1 T Amnell G Behrmann J Bengtsson P R D Argenio A David A Fehnker T Hune B Jeannet K G Larsen M O M ller P Pettersson C Weise and W Yi UP PAAL Now Next and Future In F Cassez C Jard B Rozoy and M Ryan editors Modelling and Verifica tion of Parallel Processes number 2067 in Lecture Notes in Computer Science Tutorial pages 100 125 Springer Verlag 2001 2 David Arney BaekGyu Kim Raoul Jetley Paul Jones Insup Lee Arnab Ray Oleg Sokolsky and Yi Zh2. The analysis of mode in the two devices has revealed an Alaris device that has a considerably more complex mode structure than the B Braun It is possible in the case of the Alaris to perform a number of activities while the pump is infusing which is not possible with the B Braun The Alaris supports four different vtbi entry modes when the device is holding and two of them can be used when the device is infusing This additional complexity is not necessarily a bad thing Rather the analysis raises issues that can be further ex plored from a domain or human factors perspective It is possible for example that this complexity improves the efficiency if supported by training and a natural and supportive work structure 5 3 Checking feedback of actions A number of issues may be explored that relate to checking feedback of actions Here the feedback tem plate 7 can be applied These issues include 1 will a function key change mode and will this change of mode be visible 2 does a data entry key always change the pump at tribute relevant to the mode and is this change vis ible These issues are explored through sets of properties The first set relates to the visible expression of mode while the second relates to the internal representation Hence in the case of the Alaris these properties are in vestigated via the following templates The visibility properties are AG topline value gt 16 AX function topl
3. by requiring that the meta state attribute phasevtbi is set to confirmed confirmutbt phasevtbi confirmed amp keep phasetime phaserate phaseinfuse The confirmutbi activity is only permitted if phasevtbi is entering and and the value of vtbi is equal to the required volume contained in the prescription This ac tivity is generic in the sense that nothing in its descrip tion depends on the Alaris or B Braun interface This is expressed in MAL as per confirmutbi mvolume vtbi amp phasevtbi entering These meta attributes are used to resource the ac tions 15 described in the interface layer In the case of the Alaris pump the chevron key it is permitted only if entering the vtbi or entering the infusion rate as part of an activity defined at the outer layer These actions are now assumed to bear a specific relation to the pre scribed value that the clinician has taken from the pre scription Hence the fast up chevron is only used if the current value is less than the required value by more than big step in the appropriate activity This is spec ified using the following permission axiom per fup Reusing models and properties in the analysis of similar interactive devices 9 phasevtbi entering amp topline disputbi amp middisp dutbi topline vtbitime amp entrymode vttmode amp bigstep device vtbi lt mwvolume phasetime entering amp topline
4. o hod hold o TRUE TRUE TRUE FALSE SL ESA TESE FEA ETE E o TRUE FALSE 7 mainmenu mannens n Sims asm Soman 3 A aa amen daman Saen damen dance fcr nullmode tune 1 15 z a 1 1 o 1 o SELES dae Samen amen e tune Putrose rumoge slammed slarmmode o pas 2 m o E ready read ready ready ready ready mr e a eae mg tat an og eee cea ea mg a mg me a e eae e a TE EN ready ready ready ready ready ready ready ready ready readh Ea n ready ready read E entering entering entering confirmed confirmed confirmed confirmed confirmed entering entering entering enering entering rea E nm sores Leontine fone ebm fee e e fe anes enamel e a eater Eee EAS disprate __disprat isprate _disprate disprate disprate disprate disprate disprate disprate disprate _disprate disprate disprate tt i mbi mbi mbi ml Mbi Fig 7 The B Braun activity counter example device model The middle layer will be created afresh for each new device In practice this part of the model continues to be substantial perhaps a week s work for the second author Further work is required to develop methods of reusing models that have similar structure or drive particular mode structures It can be argued that there is still some distance to go before procurers will find the techniques described here cost effective
5. the shelf state of the art devices These specifications are approximately ten times the size of specifications produced before and demonstrate the scale up of these techniques The paper also shows how the analysis tech niques allow an exploration of subtle issues relating to the interactive behaviour of the two devices and points towards a plausible method of comparison between in teractive system designs Rigorous assessment is made particularly relevant by well documented concerns about the safety of infu sion devices in general see for example 18 Failure to set up infusions accurately and reliably can have seri ous consequences A number of incidents with a range of types of infusion pump indicate how the wrong ma terial or the wrong volume at the wrong rate may in Michael D Harrison et al rare cases have disastrous consequences for the patient to whom the infusion was being administered see for example 32 Part of the problem is due to vulner abilities caused by interaction failure Infusion pumps are designed to be used in a variety of settings from general hospital wards critical and intensive care op erating rooms to accident and emergency rooms Some versions of the device are designed to be used at home or to be administered by the patients themselves The two pumps considered in the paper allow num ber entry relating to the volume to be infused and rate of infusion prior to starting the infusion proc
6. vtbitime amp entrymode ttmode amp device time bigstep lt mtime phaserate entering amp topline holding amp entrymode rmode amp device infusionrate bigstep lt mrate phasetime ready phasevtbi ready amp topline options This permission axiom provides all the circumstances in which the button may need to be used and expresses them as constraints on the use of the button For ex ample during the phase of the activity in which vtbi is being entered the top line of the device should either show vtbi and the vtbi should be visible or vtbi over time in vttmode that is the cursor indicating mode should be in the upper part of the display The permis sion also requires that the distance between the current value of vtbi and the prescribed value of vtbi should exceed the step that is made by the fast chevron key These constraints make assumptions about activities for example they assume that the clinician does not use bag mode to select the correct value of vtbi This is the kind of assumption that is outside the province of the analyst and requires input from the domain or hu man factors specialist This particular permission also describes the constraints that apply when entering time or entering infusion rate and also allows use of the key to select appropriate options Implementing the con straints for the B Braun demonstrates differences be tween the two devices Th
7. The challenge for ergonomics Applied Ergonomics 39 271283 2008 Paolo Masci Rimvydas Ruk nas Patrick Oladimeji Abigail Cauchi Andy Gimblett Yunqiu Li Paul Cur zon and Harold Thimbleby On formalising interactive number entry on infusion pumps ECEASST 45 2011 P Oladimeji H Thimbleby and A Cox Number entry and their effects on error detection In P Campos et al editor Interact 2011 number 6949 in Springer Lecture Notes in Computer Science pages 178 185 Springer Verlag 2011 F Paternd and G Faconti On the Use of LOTOS to Describe Graphical Interaction In A Monk D Diaper and M D Harrison editors People and Computers VII HCTI 92 Conference pages 155 174 BCS HCI Specialist Group Cambridge University Press 1992 R Ruksenas J Back P Curzon and A Blandford Verification guided modelling of salience and cognitive load Formal Aspects of Computing 2009 DOI 10 1007 s00165 008 0102 7 M Ryan J Fiadeiro and T Maibaum Sharing actions and attributes in modal action logic In Ito and Meyer editors Theoretical Aspects of Computer Software vol ume 526 of Springer Lecture Notes in Computer Science Springer Verlag 1991 H Thimbleby and P Cairns Reducing number entry errors Solving a widespread serious problem Journal Royal Society Interface 7 51 1429 1439 2010 Harold W Thimbleby and Andy Gimblett Dependable keyed data entry for interactive systems ECEASST 45 2011 32 J
8. about the design relevant to safety both in the context of design and procurement It is important to expand the analysis to safety in relation to use of these de vices In the context of procurement a number of anal ysis techniques have been proposed for example cogni tive walkthrough 4 heuristic evaluation 32 and hu man reliability assessment techniques SHERPA 22 The methods have not been adopted in practice be cause the cost of using them outweighs their perceived benefit Often price is the overwhelming factor in decid ing purchase The manual and non exhaustive nature of the techniques referenced above means that alternatives must be sought Empirical studies have been performed for investi gating how different design options may affect the out come of the task of programming a medical device Thimbleby and Oladimeji 26 for instance used eye tracking to investigate the ability of users to detect er rors on serial interfaces with 12 key numeric keypad and incremental interfaces with chevron keys Their re sults point out that incremental interfaces are likely to facilitate error detection They argue that this is po tentially linked to two factors The first factor relates to the users visual attention for the incremental inter face users direct their visual attention towards the dis play most of the time while in the serial interface they focus on the keys and usually omit checking the dis play Because of t
9. activities The support of activities is explored by proving that specific goals related to the infusion pump can be achieved The activity associated with prescription values of vtbi of 6 mvolume 6 and time infused of 3 mtime 3 can be checked in the model with all three layers Counter examples that will result from failure of the property 39 will be subject to the constraints imposed by the third layer of the model AG device volumeinfused mvolume 39 Reusing models and properties in the analysis of similar interactive devices 15 7 g 3 1 o o a 7 E ia 2 E 1 15 1 7 Te 19 z0 a 2z z z 25 EG fesetElapse resetElapse resetElapse zerohtbi pihtbi pbshwtbi pbshwibi pithi modtimed Ss pime pitime iresetElapse resetElapse reset lapse stat tick tik tick o o o o o o o o a o o o o o o o o o o o o o o o o o 7 z o 2 2 2 z 2 z 2 rm 2 2 2 2 2 2 hod hod tod nodd tod nod hod mise infuse infuse infuse k a jd FASE FALSE FALSE FALSE FALE FALSE FALSE FALE FALSE agar En rye middiso 3 ride p 4 middisnl o o TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE me TRUE TRUE TRUE TRUE TRUE FALE FALE FALSE ready ready ready ready ready ready readh readh ready ready ready ready entering entering entering entering entering ready ready ready ready ready ready ready ready ready
10. at the Minho HCI spec ification repository http hcispecs di uminho pt The model is described in three layers Two layers are common between the two devices The innermost pump layer captures the properties of the pumping device that is controlled by the user interface that is to be analysed The layer is described by a reusable module which is Michael D Harrison et al instantiated in each specification The middle layer is specific to the device being modelled and describes its interface structure The outermost layer the activity model is described as part of the main module to re duce state space overheads This layer describes the constraints on the device that relate to the way it is used It will assume the same activities in each device that is being considered These activities will be derived from an understanding of the work that the clinician is to carry out This outer layer is not dependent on char acteristics of the device though it provides a mapping into the middle layer thereby grounding it in the spe cific details of the device 4 1 The modelling language The models are specified in a logic based on Structured MAL 29 MAL Modal Action Logic is a deontic modal logic that incorporates a notion of action Struc tured MAL adds mechanisms for structuring the specifi cation to the basic MAL notation In our case the notion of interactor 16 27 is used to structure the specifica tion borrowing
11. example in bag mode and in query mode Bag mode allows the user to select from a set of in fusion bag options thereby setting vtbi to a predeter mined value Query mode which is invoked by pressing the query button generates a menu of set up options These options depend on how the device is configured by the manufacturer and include the means of locking Reusing models and properties in the analysis of similar interactive devices 5 Heparin 900IU h n oD Heparin Rate 9mi h Fig 3 The B Braun menu from 3 the infusion rate or disabling the locking of it or setting vtbi and time rather than vtbi and infusion rate There is also the possibility of changing the units of volume and infusion rate The device allows movement between display modes via three function keys key1 key2 and key3 Each function key has a display associated with it indicating its present function 3 3 The B Braun Pump The B Braun pump provides a different mode structure see Figure 3 The different activities of entering vtbi infusion rate and time can be accessed by means of a main menu that provides these activities as options Values are entered for the relevant pump attribute by selecting the appropriate option and using four but tons Two move the cursor left and right and two in crement and decrement the digit associated with the cursor When the number is 9 then up increments the value to 0 and carries but the cursor remains in th
12. first question in the two devices pro duces interesting results For example the modification of vtbi in the Alaris can be achieved in three modes It can be changed manually via the data entry keys when vtbi appears as the top line vtbi can also be en tered along with time rather than with infusion rate a prescription may require that a particular volume be infused over a period of time rather than at a par ticular infusion rate by selecting an appropriate op tions menu entry It is also possible to access a menu of presets bag mode either from normal vtbi entry mode when vtbi appears as the topline or from vtbi entry over time when vtb time appears in the top line The simplest mechanism for entering vtbi assum ing the specification of infusion rate is also accessible when infusing including the option of selecting an in fusion bag using the bag menu but it is not possible to enter vtbi over time These modes are distinguished by values of the attribute entrymode vtmode bagmode when with infusion rate and vttmode and tbagmode when with time It might be expected that either the device clearly distinguishes the four modes through the top line or uses the top line to make it clear that all modes are about entering vtbi In fact neither situation is the case AG entrymode in vtmode bagmode thagmode lt topline dispvtbt 6 is true But this does not include vttmode which is the mode of entry of vtbi
13. model checker NuSMV 11 to check the CTL properties It was necessary to restrict the state space by reducing the ranges of vtbi infusion rate and menu lengths Checking the two layer model is a relatively slow process for example the set of properties described in the paper for the Alaris required approximately four hours of elapsed time of a Lenovo X200 5 1 Mirroring the process in the interface The analysis measures the extent to which the infusion pump process is visible in the device This visibility re lates to basic pump variables infusion rate vtbi time to infuse It is also concerned with whether the pump is infusing or not and whether while infusing it has ex hausted vtbi and is in KVO Keep Vein Open mode The middle layer interface model describes the inter face to these attributes by recording whether they are displayed or not Visibility is modeled using a set of Boolean attributes Hence vtbi is visible in the Alaris pump if middisp dvtbi is true and in the case of the B Braun device if disp dvtbi is true The pump de vice has two modes The first infusion status describes whether the pump is infusing or not The second dis tinguishes between normal infusion and KVO infusion The two modes are signified by two attributes in the device model infusionstatus takes three values namely infuse hold and blank blank is a value that signifies that the pump device is off kvoflag is a boolean that determines w
14. properties They indicate for example that in the case of Property 27 ok always returns the de vice to a top line of holding except when the top line shows options a special mode for changing settings and entering vtbi over time Property 28 confirms that quit always returns to the hold state and property 29 indicates that when top line is volume and key2 is pressed the volume infused is initialized The B Braun has similar properties which are more direct instantia tions of the feedback template AG device infusionstatus hold amp 30 displaymode mainmenu gt AX ok displaymode mainmenu The effect of action is also consistent in the sense that the temporary value being entered is always used to update the attribute relevant to the mode when the key is used AG displaymode disptime amp 31 dispinftime IVAL1 amp device time IVAL1 gt AX ok device time IVAL1 IVAL1 here allows IVY to instantiate and to verify the property with all possible values for device time and disptime The property 31 holds for all values of IVAL1 The multiple uses of function keys in the case of the Alaris adds to the complexity of its interface It is im portant however to see how these two devices behave in relation to the activities that these two design are intended to support This issue is discussed in a lit tle more detail when discussing activities in the next section Dat
15. ready ready reac ready ready ready ready ready ready ready ready ready ready ready ready ererig entering confirmed confirmed confirmed confirmed confirmed confirmed confirmed confirmed ready ready ready ready ready ready ready ready ready o ermerng enenng emerng entering entering o ao o o confirmed confirmed confirmed confirmed confirmed confirmed confirmed confirmed confirmed confirmed confirmed confirmed confirmed confirmed o o o o o o o D o z FASE FAISE FALSE FAISE FALSE FAISE FALSE FAISE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE o o FASE FALSE FALE FALSE FALE FALSE FAI FALSE FALSE FALE FALSE FALSE FASE FAISE FALSE FAISE FALE FALSE TRUE TRUE TRUE TRUE TRUE FALSE FAISE FALSE FAISE FAISE FAISE FALSE FAISE FALSE FAISE FALSE I read options options options vibiime vibiime vibiume wwbiime wibukne vibitme Fig 6 The Alaris activity counter example Alaris activities The trace that specifies a counter example see Figure 6 indicates 1 use of the query mode first to lock the infusion rate to prevent further modification then to choose the option that is used to enter vtbi over time steps 3 9 2 the enter vtbi activity in which double and single chevron keys are used to reach the prescribed value of vtbi steps 10 14 confirmation that vtbi has been entered step 15 4 the enter time activity using the single chevron up button steps 17 1
16. to support the same activity but in which for a variety of reasons quite different design decisions have been made The candidate devices for detailed analysis are the Alaris GP infusion pump 10 see Figure 1 and the B Braun Infusomat Space 3 see Figure 2 In the fol lowing the characteristics of the two pumps are illus trated along with the aims of the analysis 3 1 Common features Most infusion pumps have three basic states infusing holding and off In the infusing state the volume to be infused vtbi is pumped into the patient intravenously according to the infusion rate While in the infusing state the vtbi can be exhausted in which case the pump continues in KVO Keep Vein Open mode and sets off an alarm In holding state values and settings can be changed 3 2 The Alaris Pump When the Alaris pump is in holding state values and settings can be changed using a combination of func tion keys and chevron buttons for the device layout see Figure 5 A subset of the features that can be changed in holding state can also be changed when in fusing Number entry is achieved by means of chevron buttons These buttons are used to increase or decrease entered numbers incrementally Depending on current Fig 2 The BBraun Infusomat Space Pump from 3 mode the chevron buttons can be used to change in fusion rate volume to be infused and time or alter natively allow the user to move between options in a menu for
17. 9 5 confirmation of the time step 20 commencement of infusing step 24 7 infusion until the vtbi is exhausted step 25 on wards w D This sequence can be contrasted with that of the B Braun see Figure 7 1 The main menu item is chosen and the enter vtbi ac tivity is carried out steps 5 12 vtbi is entered via a sequence of up buttons and this requires further exploration 2 The vtbi is confirmed step 13 3 The time choice is selected and the enter time ac tivity commenced steps 16 20 4 Time is confirmed step 21 5 start infusing at step 22 It can be seen that the model checker has generated plausible sequence of actions in both cases This se quence could be further analysed in a more qualitative way using a clinician or human factors specialist to ex plore the implications of these sequences vbume vibiime vibuime vtbidme vibtime vbiume FASE FAISE FAISE FAISE FALSE LSE TRUE TRUE UE holding infusing infusing 6 Discussion and Conclusions This analysis of the two infusion pumps has provided solid evidence of areas of concern where redesign would reduce complexity and increase the reliability of the two designs The properties used in the analysis are largely based on standard patterns either generated by the IVY tool or easily generated from the requirements of the device and situation Analogous properties can be systematically applied to other candidate pumps The procedure is syst
18. Harrison et al While properties 11 and 12 are true of the device prop erty 13 is not The current value of vtbi is not visible in bagmode or thagmode Whether this is a problem de pends on if the current value of vtbi is relevant when choosing a new bag to be infused This issue would raise a discussion about the work context It is likely for ex ample that a bag will be selected only at the start of a new infusion process rather than as an addition to an existing infusion process In the case of the B Braun device pump variables are visible in four situations when the pump is infusing then infusion rate vtbi time and volume infused are visible when the main menu is being shown and infusion rate vtbi and time are the menu options that are visible In this case the three variables are visible in the relevant data entry mode when alarming if the situation before the alarm was one of the above The situations in which vtbi is visible are identified through the following property AG device infusionstatus blank amp 14 displaymode dispalarm gt disp dutbi displaymode mainmenu amp menucursor lt dvol displaymode in disputbi dispinfusing The visibility of the infusion rate is identified through the following analogous property AG displaymede in 15 mainmenu dispinfusing dispalarm gt displaymode disprate amp entrymode dataentry disp drate
19. S 08 volume 5136 of Springer Lecture Notes in Computer Science pages 194 207 Springer Verlag 2008 D J Duke and M D Harrison Abstract interaction ob jects Computer Graphics Forum 12 3 25 36 1993 J Fiadeiro T Maibaum J de Bakker W de Roever and G Rozenberg Describing structuring and imple menting objects In Foundations of Object Oriented Lan guages number 489 in Springer Lecture Notes in Com puter Science pages 274 310 Springer Verlag 1991 US Food and Drug Administration Infusion pump im provement initiative Technical report Center for Devices and Radiological Health April 2010 P N Johnson Laird Mental Models Harvard University Press 1983 BaekGyu Kim Anaheed Ayoub Oleg Sokolsky Insup Lee Paul Jones Yi Zhang and Raoul Jetley Safety assured development of the gpca infusion pump software In Proceedings of the ninth ACM international confer ence on Embedded software EMSOFT 11 pages 155 164 New York NY USA 2011 ACM B Kirwan and L Ainsworth A Guide to Task Analysis Taylor and Francis 1992 R Lane N A Stanton and D Harrison Applying hi erarchical task analysis to medication administration er rors Applied Ergonomics 37 669679 2006 Kim G Larsen Paul Pettersson and Wang Yi UPPAAL in a Nutshell Int Journal on Software Tools for Tech nology Transfer 1 1 2 134 152 Oct 1997 J L Martin B J Norris E Murphy and J A Crowe Medical device development
20. The final publication is available at Springer via http dx doi org 10 1007 s11334 013 0201 3 Noname manuscript No will be inserted by the editor Reusing models and properties in the analysis of similar interactive devices Michael D Harrison Jos Creissac Campos Received date Accepted date Abstract The paper is concerned with the compar ative analysis of interactive devices It compares two devices by checking a battery of template properties that are designed to explore important interface char acteristics The two devices are designed to support similar tasks in a clinical setting but differ in a num ber of respects as a result of judgements based on a range of considerations including software Variations between designs are often relatively subtle and do not always become evident through even relatively thor ough user testing Notwithstanding their subtlety these differences may be important to the safety or usability of the device The illustrated approach uses formal tech niques to provide the analysis This means that similar analysis can be applied systematically Keywords MAL IVY medical devices ment interactive systems procure 1 Introduction and motivation The systematic analysis of properties of interactive be haviour using Modal Action Logic MAL and the IVY tool has been reported in previous papers 7 9 This paper focuses on the modelling and analysis of two de vices de
21. Zhang T R Johnson V L Patel D L Paige and T Kuboseb Using usability heuristics to evaluate pa tient safety of medical devices Journal of Biomedical Informatics 36 2330 2003
22. a entry keys have quite different charac teristics in the two devices The Alaris chevron keys increment or decrement the displayed value either by small steps sup sdown or by big steps fup fdown The BBraun keys either move the cursor left right or increment or decrement the digit indicated by the 14 Michael D Harrison et al cursor up down A detailed analysis of number en try for these devices can be found in 26 The model described has also been translated into an equivalent model in which the actual number domains are used and subjected to theorem proving as will be discussed in a future paper The properties to prove are exam ples of the guarded consistency pattern 7 The idea is to demonstrate that whatever the data entry mode the keys have a similar effect on the relevant pump variable Hence the standard form of the property is that what ever the mode the chevron key will have the relevant effect on the corresponding mode attribute AG entrymode mode amp modeattribute AX chevron effect modeattribute 32 For example in rmode when the infusion rate lock is off the single chevron up button increments the infusion rate by 1 AG rlock amp entrymode rmode amp 33 infusionrate IVAL1 gt AX sup gt infusionrate IVAL1 1 The corresponding property for the B Braun is more complicated because the effect is defined in terms of the different elements of the numeral t
23. ads to the following true property AG fndisp3 fnull amp 23 entrymode in bagmode tbagmode amp topline in attention vtbidone setutbi fndisp3 fquit It can be shown however that if the soft function is quit then it always appears as key3 This can be demonstrated by checking AG fndisp1 fquit fndisp2 fquit 24 fndisp3 fquit gt fndisp3 fquit Furthermore general configurations of function keys can be asserted AG topline volume gt 25 fndisp1 fnull amp fndisp2 fclear amp fndisp3 fquit It can also be shown that in most circumstances the same top line is always associated with the same key configuration Property 26 is a property that fails AG topline dispvtbi gt 26 fndisp1 fok amp fndisp2 fbags amp fndisp3 fquit In bags mode top line displays vtbi but the func tion keys show ok null and back respectively The Alaris and B Braun function keys can be compared more directly using properties similar to the feedback template supported by the IVY tool 7 Several appli cations are relevant here in the case of the Alaris AG fndisp1 fok amp topline options gt AX key1 topline holding 27 AG fndisp3 fquit gt 28 AX key3 topline holding AG topline volume amp infusionstatus hold AX key2 volumeinfused 0 29 Properties 27 29 indicate a sample of these consis tency type
24. alues in the range 1 maxrate The tick action captures the evolution of the process It describes the steps in the process and the alarms that occur when the volume to be infused is exhausted whereupon the de vice enters KVO mode or when the device has been left in a hold state for too long To illustrate the model s specification the normal infusion process is described using the MAL axiom infusionstatus infuse amp infusionrate lt vtbi tick vtbi vtbi infusionrate amp elapsedtime elapsedtime 1 amp volumeinfused volumeinfused infusionrate amp keep kvorate kvoflag infusionrate infusionstatus This axiom describes tick when the pump is infusing infusionstatus infuse and vtbi exceeds the amount that is reduced as a consequence of the value of the infusion rate The axiom has three elements the ac tion that is being described contained in square brack ets the conditions that must be satisfied for the ac tion to have the stated effect left side of the implica tion the result of the action under these conditions utbi vtbi infusionrate specifies that the next state indicated by the prime symbol of vtbi must be equal to its old value minus the infusionrate MAL specifies that unless a state attribute is explicitly constrained in a modal axiom then it can change randomly in the next state The keep function determines the list of state at tributes that cannot change The pum
25. ang Safety requirements for the generic patient controlled analgesia pump disprate l R i moi mbi mbi mbi mbi mbi tbl vol mbi moi 3 B Braun Melsungen AG B Braun Infusomat Space User Manual Technical report B Braun Melsungen AG 34209 Melsungen Germany 2007 4 L A Bligard and A L Osvalder An analytical approach for predicting and identifying use error and usability problem In A Holzinger editor Proceedings of the 3rd Human computer interaction and usability engineering of the Austrian computer society conference on HCI and usability for medicine and health care number 4799 in Springer Lecture Notes in Computer Science pages 427 440 Springer Verlag 2007 5 M L Bolton and E J Bass Formally verifying human automation interaction as part of a system model limita tions and tradeoffs Innovations in System and Software Engineering 6 3 219 231 2010 6 J C Campos and M D Harrison Model checking inter actor specifications Automated Software Engineering 8 275 310 2001 7 J C Campos and M D Harrison Systematic analysis of control panel interfaces using formal tools In N Graham and P Palanque editors Interactive systems Design Specification and Verification DSVIS 08 volume 5136 of Springer Lecture Notes in Computer Science pages 72 85 Springer Verlag 2008 8 J C Campos and M D Harrison Interaction engineering using the IVY tool In G Calvary T C N Graham and P Gray edito
26. aper in that while it focuses on the details of the interactive number entry system while the present paper focuses on the device modes Also relevant is the work of Ruk nas and Curzon 28 who are concerned to model not only the device but also to incorporate assumptions about the activities and goals that are to be carried out based on general cognitive principles They have used their techniques to replicate experimental data relating to an ambulance dispatching system In the paper two detailed models of the interactive behaviour of devices are considered and subjected to systematic analysis using a battery of properties There are no assumptions in this work about cognitive processes Assumptions about infusion activities are made however by using an activity layer see also 15 as is described in Section 4 5 Some relevant research is also concerned with the verification of medical software For instance researchers at FDA and at the University of Pennsylvania have recently used a model driven engineering approach to generate software for a prototype Patient Controlled Analgesic infusion pump 20 Starting from a Simulink Stateflow model they translate the model manually into a specification using timed automata verifying safety requirements with UPPAAL 23 and then synthesising C code with the TIMES tool 1 Examples of safety re quirements are the pump shall issue an alert if paused for more than t minutes each chang
27. are included in the Alaris model 4 5 The activity layer The third layer of the model describes the activities that are assumed to be typical of the clinician s use of the device Whereas the pump layer which is reused be tween devices is specified as a separate interactor the activity layer which has the same shape but different implementation in the two models is in each case part of the interface interactor for the two devices Activ ities are determined through negotiation with domain and human factors experts The process of eliciting and understanding these activity actions and meta state at tributes is a process akin to task modelling 21 where the human factors or domain expert observes the infu sion activity in context The examples here are intended to be indicative only and have not been determined by such a process One of the activities that may have been determined as being important in the infusion process is that another clinician should confirm that the correct value of vtbi has been entered into the device based on the original prescription These meta state attributes do not capture any feature of the device or its inter face rather they indicate a state in the activity as as sumed to be understood by the clinician who is using the device They can be used to constrain the device actions described in the interface layer Hence confirm ing that the vtbi has been entered involves completing the entervtbi activity
28. at indicates the mode see Figure 3 disp is a Boolean array that represents the visibilities of state attributes including those that are specified in the pump interactor There are actions up down right left and ok that allow users to enter data Hence the transition in the B Braun pump that is equiv alent to the Alaris transition that allows the user to begin entering vtbi is as follows displaymode mainmenu amp menucursor dvtbi ok entrymode dataentry amp displaymode disputbi amp dispvalue device vtbi amp entry maadiginder amp disp dvtbi amp disp drate amp disp dtime amp disp detime amp disp dvol amp disp dalarmvol amp effect device resetElapsed amp keep target alarmvolume This axiom specifies that if displaymode shows the main menu and the menu cursor is pointing at the vtbi entry then on pressing ok the device moves to data entry mode as specified by entrymode and the displaymode shows vtbi and the temporary state attribute used to show the number entered is set to the current value of vtbi Only vtbi is shown on the display This B Braun middle layer consists of a specification that involves 16 state attributes 9 actions including 3 augmentations of pump actions and 58 axioms It should be noted that some of the possible set up options that are also provided by the B Braun main menu are omitted from this model but the equivalent features
29. d be defined in Structured MAL as elaspedtime aux tick elapsedtime auz 1 where aux is an auxiliary variable introduced to carry the value of elapsedtime into the next state after tick To avoid these auxiliary variables we extended the def inition of the modal operator of 17 by using priming to state explicitly which references to attributes should be evaluated after the action Hence the axiom above can be written as tick elapsedtime elapsedtime 1 Parentheses will be omitted whenever the scope of the modal operator can be inferred The modal operator makes it possible to prescribe the effect of actions in the state but says nothing about when actions are permitted or required to happen For this permission and obligation operators must be used As in 29 only the assertion of permissions and the denial of obligations are considered per ac guard action ac is permitted only if guard is true cond obl ac if cond is true then action ac becomes obligatory Permissions are asserted therefore by default and obli gations are off by default This makes it easier to add permissions and obligations incrementally when writ ing specifications For example the two permission ax ioms per ac guard and per ac gt guard together yield per ac gt guard1 amp guard2 note that amp is used to denote logical and for logical or and for not This logic is particularly ap
30. e same position and down has the opposite effect see Figure 4 There are fixed function keys clear ok run The availability of these fixed function keys is indicated in the current display 3 4 The aims of the analysis The focus of the analysis presented here is to consider confusions that arise as a result of the mode structures exhibited by these devices Furthermore the analysis ex plores potential confusions relating to information that is being displayed The two devices above are compared ttet v Fig 4 Entering the rate on the B Braun from 3 in terms of software aspects of the design The rela tionship between the device and its environment which is of course extremely important will not be considered explicitly in this paper Hence for example physical as pects of the giving set used to connect the device to the vein of the patient will not be considered nor will any issues associated with electromagnetic interference These other aspects are also important in the design and procurement of these devices but are not the focus here There are a wide range of infusion pumps and sy ringe drivers in use in hospitals with a variety of inter face styles that differ in terms of data entry and the ways in which modes are structured This specific ex ample will trigger discussion of broader issues 4 The model As stated above the specifications of the models dis cussed in this paper can be seen
31. e B Braun has two separate functions that together allow number entry Modifying the size of the increment is achieved using the left or right button The decrement or increment is achieved using the down or up buttons Number entry is only permitted if the device is in dataentry mode Entering vtbi is only allowed for example if the display mode is to display vtbi and the prescribed vtbi is greater than the currently displayed value of vtbi The permis sion also includes similar constraints for up when the display mode is to display time or infusion rate per up entrymode dataentry gt displaymode disputbi amp mvolume gt dispvalue displaymode disptime amp mtime gt dispvalue displaymode disprate amp mrate gt dispvalue The activity layer captures some of the properties of the cognitive models described by 28 It is however sim pler making no assumptions about the cognitive pro cess itself simply concerning itself with observed activ ities This activity layer consists of a specification that involves 4 state attributes 7 actions activities and 21 axioms 5 Verifying the model The aim of the verification process is that similar prop erties indeed patterns expressing user interface charac teristics can be checked of each candidate device These formal properties provide a benchmark against which each candidate design can be explored As a result po tentially unforeseen design conse
32. e in dose settings must be confirmed before it is applied The complete list of the considered safety requirements can be found at 2 Our work complements these analyses being con cerned with interaction properties such as mode clarity and consistency of naming and function Michael D Harrison et al 3 The infusion pumps The candidate devices for analysis are typical of a class of devices that control a process over time The user s activities in relation to the device include setting it up or modifying it and monitoring it Devices of this kind have been the subject of previous work and in partic ular the techniques described in this paper have been applied to a simplification of a flight management sys tem 6 an automobile based air conditioning system 7 and another simpler version of the devices analysed in this paper 8 The analysis described here is consid erably larger than the previous work the two models considered are each ten times the size of the models considered before They provide detailed descriptions of the interactive behaviour of the two devices The aim in this paper is to access relatively subtle properties of more complicated devices It is not possible to include the specifications as appendices to the paper however they are made available at the Minho HCI specification repository The second difference is that the aim is to provide a means of comparison between two real de vices both developed
33. ematic providing a strong basis for comparison Specifically the analysis has indicated issues associ ated with the relation of the display to the underlying pump process and the mode structure of the particular device For example the analysis indicates that there are possible confusions relating to the use of the display of vtbi in the top line in the case of the Alaris ambiguities about whether the pump is infusing or not using the top line of the display as a guide in the case of the Alaris inconsistent use of function keys in the case of the Alaris possible confusions combining left right up and down in the case of the B Braun The analysis says nothing about the significance of these issues The method is to be used as part of a process including the active participation of human factors and domain specialists In the context of use these discrep ancies in the device may not be issues at all An im portant aspect of the method is that it is systematic and that it has the potential to be reused for every candidate infusion pump The inner level of the speci fication can be reused for every candidate pump The outer activity layer can also be partially reused guiding the analyst to create the appropriate constraints on the 16 Michael D Harrison et al z esettnse sts Tesennse esicanse ests sane esthnst mois esehase estan Se ere estar estan e moaren z z z 26
34. es of analyses will be explained in detail in section 5 Masci et at 25 analysed the interactive number en try systems of the B Braun and Alaris pumps with the Symbolic Analysis Laboratory SAL 13 They devel oped the specification by reverse engineering the real devices from user manuals and manual exploration of the real devices They formalised a design principle pre dictability 14 which concerns the ability of a user to accurately predict the consequences of future interac tions from the observable persistent state of the device e g from what is shown on the device displays Their verification approach systematically compares a predic tion model which specifies the expectations of the user and relates it to the specification of the actual number entry system of the devices The prediction model can be thought of as a mental model 19 developed by an idealised expert user that i knows perfectly the func tionalities of the device but ii makes decisions only on the basis of the current persistent state externalised by the device Their analysis is conservative if the ideal user fails to predict the effect of any action then real human users would have similar difficulties they can do no better than the idealised expert user They are able to perform the analysis with SAL on detailed models that consider the full range of numbers handled by the real devices This work complements the anal ysis described in this p
35. ess Their specifications are derived from an understanding of two infusion pumps The aim has been to produce specifica tions that are as accurate a snapshot of the devices as possible However the purpose has not been to demon strate in detail the characteristics of current versions as a way of producing a consumers guide but to demon strate the utility of the proposed approach for exploring subtle design differences in a systematic way Details of the description were derived from a combination of manuals 10 3 simulators as well as some limited access to the physical devices themselves The Alaris simulation is due to Patrick Oladimeji of Swansea Uni versity http cs swan ac uk cspo simulations based on the actual device and the other was provided by B Braun of a version of the Infusomat Space MAL and IVY were used to model the two devices The models are illustrated by providing and explain ing fragments of the MAL specification These frag ments both demonstrate process and reuse indicating the scale of the undertaking that can be achieved us ing the MAL notation and the IVY tool The paper demonstrates the extent of commonalities between the two specifications It also demonstrates the common ap plication of properties of interactive behaviour while at the same time showing that some properties were only relevant to one of the devices A common layer specifies the attributes of the pump device how the material is in
36. fused and at what rate or over what period of time The paper briefly introduces specifications of the two devices It focuses on properties that can be used for the purposes of comparison After an overview of the back ground and related work Section 2 the two infusion pumps are introduced Section 3 Section 4 explains the three layers of the models and Section 5 provides examples of how generic properties were used in the verification of the model Six main classes of properties will be considered mirroring of device processes e g infusing on hold in the interface mode clarity feed back for critical actions consistency of the interface checking ease of recovery support for normative tasks A final section Section 6 provides some discussion of the comparison between the two devices and conclu sions 2 Background and related work Motivation for this analysis has been a concern with the safety particular in relation to human error of medical devices 24 The U S Food and Drug Administration FDA 18 is now encouraging the use of safety argu ments based on formal justifications to provide evidence of the safety of medical devices They have launched the Generic Infusion Pump project to investigate solutions to safety problems in infusion pump software Their aim is to develop a set of safety reference models that can be used to assess safety of infusion pump software Techniques are required to help answer questions
37. fusing status is indicated by a top line that either displays infusing or KVO This property turns out to be false because the device can continue to infuse when clearing volume chang ing vtbi when indicating that the device is locked and when selecting certain options using the query button and when showing the information associated with an option These top lines can appear in both infusing and holding states In the case of the infusion status being hold the property 3 indicates a more refined stage in the development of the property for the Alaris AG device infusionstatus blank amp 3 topline in locked volume options dispinfo disputbi topline in holding setvtbi attention vtbitime 4 device infusionstatus hold The question that equations 2 and 3 raise is whether the multiplicity of exceptions is a good or a bad thing It is at this stage that further input from domain or human factors experts is required Potential ambigui ties may not be an issue because other features of the Alaris interface may make it clear to the user the sta tus of the device Indeed aspects of the design wholly unrelated to this interface may be critical for exam ple the sound of the pump operating The analysis has Reusing models and properties in the analysis of similar interactive devices 11 raised these issues in a systematic way that can lead to the appropriate discussion The B Braun pump
38. hat are significant depending on the position of the cursor In the B Braun model the cursor is associated with attribute entry and dispvalue is the attribute that is manipulated in data entry mode before updating the relevant attributes AG entrymode dataentry amp 34 dispvalue IVAL gt AX down gt entry 8 dispvalue IVAL 1 entry 2 dispvalue IVAL 2 entry 1 dispvalue IVAL 4 entry 0 dispvalue IVAL 8 amp amp amp In practice the property needs adjusting to deal with values that are too large or too small as constrained by the invariant in axiom 1 these cases must exclude the possibility of underflow or overflow In addition to the standard property 34 of the same form as the template 30 a further property is required to ensure that when data entry mode is exited using ok then the relevant pump attribute depending on displaymode is updated appropriately The following property shows how this works with time entry displaymode disptime only when dataentry is true and therefore the property has been simplified a little AG displaymode disptime amp 35 dispinftime IVAL amp device time IVAL gt AX ok device time IVAL 5 5 Checking ease of recovery The final stage of analysis of the two devices concerns the ease with which the two devices can recover from a wrong action There are a variety of properties to be explored in th
39. hether the device is in kvo mode In the case of the Alaris pump the most significant predictor of what the device is doing is the top line see Figure 5 The B Braun see Figures 3 and 4 dis plays mode related information in different places This mode display information is represented in the B Braun model by using the state attribute displaymode Whether infusion status is represented unambiguously can be as sessed by checking display properties relating to the sta tus In the case of Alaris the question leads to a fairly complicated answer The Alaris displays the same top line information while both infusing and holding in a number of circumstances because it is possible to ad just aspects of the process while the device is infusing The B Braun is less complex from this perspective The process of checking standard properties is itself a dis covery process Often standard properties of the device fail because they are only partially true It becomes nec essary to explore counter examples and to add further constraints until a true property of appropriate com plexity is determined AG device infusionstatus blank 2 topline in infusing dispkvo 4 device infusionstatus infuse Property 2 shows a stage in the development of the relevant property for the Alaris Properties must ex clude the possibility of the device being switched off expressed as the infusion status not being blank The property indicates that in
40. his device dependent errors like key bounces due to defective buttons are more likely to be detected when using the incremental interface The second factor relates to syntax errors With the serial interface users may accidentally enter invalid numbers e g 1 2 0 or 1 2 while such a possibility is designed out in incremental interfaces Invalid numbers need to 1 A key bounce occurs when physically pressing a button once causes a repeat of the same key Reusing models and properties in the analysis of similar interactive devices 3 be handled and different manufactures generally imple ment different ad hoc solutions with the net result that devices deliver an unpredictable user experience 30 31 The work described in this paper complements empiri cal studies such as this one It is concerned with subtle differences between apparently similar interfaces as pects that would have been impractical to analyse in any experiment Recent formal modelling work relevant to medical devices has focused on a number of aspects of their programming Bolton and Bass 5 used SAL 13 to analyse a model of the Baxter iPump The pump model is devel oped within a framework that takes into account user goals normative tasks i e sequences of actions that must be performed according to written documents such as user manuals or training material and the op erational environment Their main goal is to explore the possibility of
41. igure 5 and the pump is processing normally vtbi has not been ex hausted i e the pump is not in KVO mode topline in holding infusing amp kvoflag key2 topline disputbi amp oldutbi vtbi amp middisp dutbi amp middisp dvol amp middisp dtime amp middisp dbags amp middisp dkvorate amp middisp dquery amp fndisp1 fok amp fndisp2 fbags amp fndisp3 fquit amp entrymode vimode amp effect device resetElapsed amp keep onlight runlight pauselight rdisabled rlock The axiom asserts that the next top line shows vol ume to be infused disputbi and the value of vtbi is Michael D Harrison et al displayed i e middisp dvtbi is true The soft func tion keys fndisp1 etc in this next step show ok bags and quit respectively The mode specified by the value of entrymode is vtmode which indicates that the device is ready to change the value of vtbi Finally the elapsed time since there was last a key stroke when infusionstatus is hold is set to zero This Alaris middle layer consists of a specification that involves 17 state attributes 11 actions including augmentations of pump actions and 75 axioms 4 4 The B Braun layer The B Braun layer has a different structure than that of the Alaris pump The equivalent state attribute to topline is displaymode which specifies that there is in formation in the display th
42. ine value The properties that check the change of mode are as follows AG entrymode value gt 17 AX function gt entrymode value Checking this set of properties indicates that 1 pressing key marked as cancel leaves the device in infuse mode when the top line shows vtbi done 2 tick never changes the entrymode Otherwise the keys will always change the function The second issue can be explored through a set of properties see 8 that check the attributes that are changed by number entry keys in particular modes AG entrymode IVAL1 amp 18 modeattribute IVAL2 AX action entrymode IVAL1 amp modeattribute IVAL2 IVAL1 here is a meta variable that allows IVY to in stantiate and to verify the property with all possible values for entrymode and IVAL2 to all possible values of the mode attribute Hence the following instance of the set is true AG entrymode vtmode amp device vtbi 3 19 gt AX sup gt entrymode vtmode amp device vtbi 3 In the case of the B Braun the relevant properties are AG displaymode value gt 20 AX function displaymode value and AG entrymode value 21 AX function gt entrymode value Checking these properties has the expected effect Reusing models and properties in the analysis of similar interactive devices 13 5 4 Checking consistency of action As discussed in previous sections the two de
43. is context One that can be used to illustrate the analysis is to demonstrate that the data entry keys always have inverses This property has a standard template 7 AG attribute value gt 36 AX actionl EX action2 amp AX action2 attribute value In the case of sup in the Alaris pump and rmode when the infusion rate is not locked the following property holds for all values of IVAL1 except the limits AG infusionrate IVAL1 amp 37 entrymode rmode amp rlock gt AX sup gt EX sdown amp AX sdown infusionrate IVAL1 The recovery property in the case of B Braun is compli cated because of carry When incrementing the digit in the leftmost position of the numeral the model spec ifies that 1000 goes to 1111 This is the largest al lowable number given the constraints of the domains that have been reduced to permit analysis by model checking When the left most digit is decremented then this value returns to 0111 When numbers are not subject to this overflow condition then down acts as an inverse AG entrymode dataentry amp 38 dispvalue IVAL1 gt AX up gt EX down amp AX down gt entrymode dataentry amp dispvalue IVAL1 Perhaps more relevant is the ability of the devices to allow a sequence of actions to reach a different number from whatever the current value This is a property that can also be proved 5 6 Checking support for
44. is designed differently There are a number of ways in which mode is indicated and these are all captured together in the attribute displaymode These different modes can be indicated for example by the size of the label referring to the data entry display see Figures 4 and 3 for examples It is assumed by the model that this feature whatever it is is salient for the user In the case of infusing the display shows arrows that move dynamically as the pump progresses The simple standard property that began the Alaris investi gation of pump status turns out to be true immediately for the B Braun AG device infusionstatus blank 4 displaymode dispinfusing 4 device infusionstatus infuse There are many more display modes in the case of the B Braun that indicate an infusion status of holding AG device infusionstatus blank 5 displaymode in disprate disputbi disptime mainmenu dispalarm dispalarmvol optionsmenu statusmenu dispblank device infusionstatus hold Property 5 unambiguously defines the holding behaviour of the device 5 2 Checking ambiguity of modes There are a number of properties that explore the am biguity or otherwise of interface modes 1 Does the display unambiguously determine the mode of the device Key attributes here are topline for the Alaris and displaymode for the B Braun 2 Are the mode relevant pump variables visible in the relevant mode Exploring the
45. p interactor in volves 10 attributes 3 actions start pause and tick and 20 axioms 4 3 The Alaris layer The difference between the two infusion pumps is cap tured in the middle interface layer of the specification Both pumps use interface modes to make most effec tive use of the devices limited display spaces The mid dle interface layer describes the behaviour of interface modes It also describes which of the pump variables are displayed the displays associated with the function topline middisp fndisp fndisp2 fndisp3 keyl key2 key3 fup sup sdown fdown run pause query on Fig 5 Alaris actions keys and the top line of the display which partly in dicates the mode of the device The Alaris display is organised into three parts topline describes the con tents of the top line represented by an enumeration of possible top line displays iline holding infusing volume disputbi attention vtbidone dispkvo setutbi locked options dispinfo utbitime dispblank middisp is a Boolean array that indicates whether a state attribute is visible These state attributes are mainly but not entirely attributes specified in the underlying pump Finally fndisp1 fndisp2 and fndisp3 represent the displays that describe the current purpose of the three soft keys The following illustrative axiom de scribes the behaviour of the soft key 2 when the top line of the device shows holding see F
46. packaging an automated reasoning tool in such a way that non experts of formal meth ods such as human factors engineering practitioners could i specify a realistic interactive system with in tuitive modelling constructs and ii verify in a reason able amount of time a variety of basic normative tasks such as turning on off the pump stopping the infusion entering a volume to be infused They performed the verification on a simplified model of the pump as the state space of the full model exceeded the capabilities of the model checker This work shares with that paper the concern that verification tools when properly pack aged can enable non experts of formal methods to per form the verification of realistic systems In particular a modelling architecture that enables model reuse can help to reduce the perceived cost of building a formal specification because representative models can be de fined and easily changed to support multiple analyses The work described in this paper differs from Bolton and Bass because its main goal is to compare similar designs of medical devices systematically For this rea son a detailed model of the interactive behaviour of the devices limiting simplification to the minimum is used The layered approach described in the paper proves ef fective for this as it allows some scope for reuse and it is possible to verify safety and reachability properties on the full specification of device modes Exampl
47. propriate for describ ing a system in which components can be reused The interactor presentation is defined by annotating actions and attributes to show that they are perceiv able The modality of the perceivable attribute action is given using further attributes For example vis as serts that the attribute action is visibly perceivable In addition if attached to an action it can be invoked by the user Additional annotations are introduced for fur ther modalities Attributes and action parameters are typed Types are represented as enumerations of the key values or as subranges of integer types Denar a b c Trange 0 10 Interactors are composed through aggregation For example the pump interactor can be assumed within the main interactor of the specification interactor main aggregates pump via device More details of MAL can be found in 6 8 Reusing models and properties in the analysis of similar interactive devices 7 4 2 The pump layer The inner layer describes the basic infusion process This process is captured in an invariant infusionrate gt 0 infusionrateaux infusionrate infusionrate gt 0 time vtbi infusionrateauz infusionrate 0 time 0 1 This invariant asserts a relationship between vtbi in fusion rate and the time to completion of the process infusionrateaux adds slight complication and is intro duced to ensure that division by zero is avoided It takes v
48. quences can be discov ered that could not be found simply by reading the manual or by experimenting with the device The cir cumstances in which properties fail are assessed with the help of human factors or domain expertise Failure acts as a trigger for the consideration of a human in terface characteristic that would otherwise lie hidden Properties checked of each candidate are of the follow ing types Checking that the process represented in the inner most pump layer is visible through the device inter face mirroring the process in the interface Checking that modes can be determined unambigu ously from the interface mode clarity Checking that actions provide appropriate feedback for example when they change mode or change the values of pump attributes Ensuring consistency of use of the display or of ac tion consistency of the interface Checking ease of recovery from an action Ensuring that activities described in the outer layer are supported supporting activities The specific details of the properties in these categories will differ depending on the device s interface as is de scribed in the middle layer of the model The aim is to instantiate standard templates as far as possible In the case of the devices modelled here the proper ties that were checked of the inner and middle layers were checked first before considering the devices con strained by activity assumptions Prope
49. rs Proceedings of the ACM SIGCHI Sym posium on Engineering Interactive Computing Systems pages 35 44 ACM Press 2009 9 J C Campos and M D Harrison Modelling and analysing the interactive behaviour of an infusion pump Electronic Communications of the EASST 5 2011 Cardinal Health Inc Alaris gp volumetric pump direc tions for use Technical report Cardinal Health 1180 Rolle Switzerland 2006 A Cimatti E Clarke E Giunchiglia F Giunchiglia M Pistore M Roveri R Sebastiani and A Tacchella NuSMV 2 An Open Source Tool for Symbolic Model Checking In K G Larsen and E Brinksma editors Computer Aided Verification CAV 02 volume 2404 of Lecture Notes in Computer Science Springer Verlag 2002 E M Clarke O Grumberg and D A Peled Checking MIT Press 1999 L de Moura SAL Tutorial Technical report SRI Inter national Computer Science Laboratory 333 Ravenswood Avenue Menlo Park CA 94025 2004 10 11 12 Model 13 Reusing models and properties in the analysis of similar interactive devices 17 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 A J Dix Formal Methods for Interactive Systems Aca demic Press 1991 G Doherty J C Campos and M D Harrison Resources for situated actions In N Graham and P Palanque editors Interactive systems Design Specification and Verification DSVI
50. rties are pre sented for analysis using CTL see 12 for an intro duction to model checking CTL provides two kinds of temporal operator operators over paths and oper ators over states Paths represent the possible future behaviours of the system When p is a property ex pressed over paths A p expresses that p holds for all 10 Michael D Harrison et al paths and E p that p holds for at least one path Op erators are also provided over states When q and s are properties over states G q expresses that q holds for all the states of the examined path F q that q holds for some states over the examined path X q ex presses that q holds for the next state of the examined path while qUs means that q holds until s holds in the path CTL allows a subset of the possible formulae that might arise from the combination of these opera tors AG q means that q holds for all the states of all the paths AF q means that q holds for some states in all the paths EF q means that q holds for some states in some paths EG q means that q holds for all states in some paths AX q means that q holds in the next state of all paths EX q means that q holds in the next state of some paths A qUs means that q holds until some other property s holds in all paths E qUs means there exists a path in which q holds until some property s The properties are analysed in the IVY tool by translating the MAL model into SMV and using the symbolic
51. the mechanisms from Structured MAL Interactors are modules that have a state defined by attributes which is partially made available to the user through some presentation medium and a set of actions some available to users some internal that act on that state MAL axioms will be used to define the behaviour of interactors In addition to the usual propositional operators and actions the logic provides a modal operator ac expr is the value of expr after the occurrence of action ac the modal op erator is used to define the the effect of actions a special reference event expr is the value of expr in the initial state s the reference event is used to define the initial state s a deontic operator per per ac meaning action ac is permitted to happen next the permission oper ator is used to control when actions might happen a deontic operator obl obl ac meaning action ac is obliged to happen some time in the future Note that obl is not used in these specifications One difference between the logic used here and Struc tured MAL is in the treatment of the modal operator In Structured MAL the modal operator is applied to whole propositions There is no way to relate old and new values of attributes directly Old and new values are often related in practice by the introduction of aux iliary variables For example an action tick which in crements the value of attribute elapsedtime woul
52. veloped by different manufacturers to support the same tasks The two devices manage limited dis plays and keys in different ways The paper demon Jos Creissac Campos Departamento de Informatica Universidade do Minho and HASLab INESC TEC Michael D Harrison Paolo Masci School of Electronic Engineering and Computer Science Queen Mary University of London E mail michael harrison eecs qmul ac uk Paolo Masci strates a technique for comparing these user interfaces based on systematic analysis The technique relies on the use of standard property templates These devices are analysed by reusing components of the specifica tion that share common properties and by systemat ically checking similar properties The purpose of the analysis is to demonstrate the use of a formal analysis technique as a means of comparison of the interfaces of two actual devices particular mechanisms for the analysis based on the common use of components of the specification The approach will be demonstrated by producing anal yses of two intravenous infusion pumps the Alaris GP 10 and the B Braun Infusomat Space 3 Although specific devices are being explored the purpose is to demonstrate the design and the judgements that can be made rather than to rate the two designs The contribution of this paper is to demonstrate the use of the IVY method and tools in producing de tailed specifications of the interactive behaviour of off
53. vices sup port function keys that change modes In the case of Alaris the function keys are soft keys they are labeled fndisp1 fndisp2 fndisp3 in the model The B Braun keys are not soft keys but often how the key is to be interpreted is indicated in the display see for exam ple the infusion data entry mode described in Figure 3 Here OK is labeled as confirm The main function of the B Braun display in relation to function keys is to indicate their availability Two types of consistency are explored here The differences between the devices means that a number of properties are only relevant to one of the devices Hence in the case of the Alaris the obvious questions are whether the same soft function is always associated with the same key and whether the same soft keys are always associated with a particular piece of information on the top line To illustrate how the model can be analysed with respect to these ques tions consider key3 A first question would be whether quit is always associated with key3 whenever it is used AG fndisp3 fnull gt fndisp fquit 22 This property turns out to be false There are a num ber of situations where key3 is used for other purposes In bags mode function key3 shows back rather than quit When the top line shows attention or vtbi done or set vtbi then key is marked as ok and used to exit the dialogue box Exploring all these cases le
54. when entering vtbi over time AG entrymode vttmode 7 4 topline vtbitime is false because the time entry mode ttmode also oc curs when topline vtbitime the distinction between the modes is indicated by the position of an arrow The B Braun does not exhibit such ambiguities The B Braun model includes for example a data entry mode which is true when the display mode indicates entry of infusion rate time and infusion rate AG displaymode in disputbi disprate disptime 4 entrymode dataentry 8 Similar properties are true of scalemode and alarmmode AG displaymode dispalarmvol 9 4 entrymode scalemode AG displaymode dispalarm 10 4 entrymode alarmmode The property 10 is false because there are other sit uations that will generate alarm mode The second fea ture of the two devices that is important in considering modes is whether the pump variables that are being modified are visible in the relevant mode For example it should be expected that the infusion rate is visible when in a mode in which infusion rate is being entered In the case of the Alaris the infusion rate can be entered either in infusemode or rmode AG entrymode in rmode infusemode 11 middisp drate This property of the model is true and similar proper ties relate to other modes for example AG entrymode vtmode middisp dvtbi 12 AG entrymode in bagmode thagmode 13 middisp dvtbi 12 Michael D
Download Pdf Manuals
Related Search