PVSio-web is a graphical environment for facilitating the design and evaluation of interactive (human-computer) systems. Using PVSio-web, one can generate and evaluate realistic
interactive prototypes from formal models. PVSio-web has been successfully used for analyzing commercial, safety-critical medical devices. It has been used to create training material for device developers and device users. It has also been used for medical device design, by both formal methods experts and non-technical end users.
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]