PVSio-web is a graphical environment that transforms the animation capabilities of the standard PVS theorem proving system with a sophisticated graphical front-end allowing interactive (human-computer) systems modelling and prototyping. Using PVSio-web, one can generate and evaluate realistic interactive prototypes from formal models. PVSio-web has been successfully used over the last two years for analysing commercial medical devices, and has been used to create training material for device developers and device users. For safety-critical medical device design, PVSio-web has been used with formal methods experts and with non-technical end users, including doctors and nurses.
Design issues in medical user interfaces.
Paolo Masci, Queen Mary University of London, has used PVSio-web to create this video for hospitals, device manufacturers, and regulators to raise awareness about general user interface software issues.
``PVSio-web 2.0: Joining PVS to HCI.'' Proceedings of 27th International Conference on Computer Aided Verification (CAV2015). California, USA, 2015. [PDF]
``PVSio-web: a tool for rapid prototyping device user interfaces in PVS.''Proceedings of the 5th International Workshop on Formal Methods for Interactive Systems (FMIS 2013). London, UK, 2013 [PDF]
``The benefits of formalising design guidelines: A case study on the predictability of drug infusion pumps.'' In Innovations in Systems and Software Engineering, Vol 11(2), Springer-Verlag. London, 2015 [PDF]
``Formal Verification of Medical Device User Interfaces Using PVS.'' In ETAPS/FASE2014, 17th International Conference on Fundamental Approaches to Software Engineering, Grenoble, France, 2014 [PDF]
``Tool demo: Using PVSio-web to demonstrate software issues in medical user interfaces.'' In 4th International Symposium on Foundations of Healthcare Information Engineering and Systems (FHIES2014). Washington DC, USA, 2014 [PDF]
``Combining PVSio with Stateflow.'' In 6th NASA Formal Methods Symposium (NFM2014). Houston, TX, 2014 [PDF]
``Model-based development of the Generic PCA infusion pump user interface prototype in PVS.'' In Safecomp2013, 32nd International Conference on Computer Safety, Reliability and Security. Toulouse, France 2013 [PDF]
``Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example.''
In EICS2013, 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, London, UK, 2013 [PDF]
``On formalising interactive number entry on infusion pumps.''
In FMIS2011, the 4th Intl. Workshop on Formal Methods for Interactive Systems. Limerick, Ireland, 2011 [PDF]