-
Notifications
You must be signed in to change notification settings - Fork 23
Home
PVSio-web is a new graphical tool for prototyping and analysis of user interface software. The tool transforms the animation capabilities of the standard PVS theorem proving system with a sophisticated graphical front-end allowing interactive (human-computer) system 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.
Example realistic simulations created with PVSio-web can be watched in this YouTube video: https://www.youtube.com/watch?v=T0QmUe0bwL8
Live demos of realistic medical devices are executed on a free Heroku cloud server. Links to these live demos can be found at www.pvsioweb.org
[PVSio-web 2.0: Joining PVS to HCI.] (http://www.chi-med.ac.uk/research/downloadandcount.php?PPnum=PP310) Paolo Masci, Patrick Oladimeji, Yi Zhang, Paul Jones, Paul Curzon, Harold Thimbleby. Proceedings of 27th International Conference on Computer Aided Verification (CAV2015). California, USA, 2015
[PVSio-web: a tool for rapid prototyping device user interfaces in PVS.] (http://www.chi-med.ac.uk/researchers/downloadandcount.php?PPnum=PP112) Patrick Oladimeji, Paolo Masci, Paul Curzon and Harold Thimbleby. Proceedings of the 5th International Workshop on Formal Methods for Interactive Systems (FMIS 2013), London, UK, 2013
[The benefits of formalising design guidelines: A case study on the predictability of drug infusion pumps.] (http://www.chi-med.ac.uk/researchers/downloadandcount.php?PPnum=PP135) Paolo Masci, Rimvydas Ruksenas, Patrick Oladimeji, Abigain Cauchi, Andy Gimblett, Karen Li, Paul Curzon, Harold Thimbleby. In Innovations in Systems and Software Engineering, Vol 11(2), Springer-Verlag. London, 2015
[Formal Verification of Medical Device User Interfaces Using PVS] (http://www.chi-med.ac.uk/researchers/bibdetail.php?docID=706) Paolo Masci, Yi Zhang, Paul Jones, Paul Curzon, Harold Thimbleby Proceedings of ETAPS/FASE2014, 17th International Conference on Fundamental Approaches to Software Engineering, Grenoble, France, 2014
[Using PVSio-web to demonstrate software issues in medical user interfaces.] (http://www.chi-med.ac.uk/research/downloadandcount.php?PPnum=PP234) Paolo Masci, Patrick Oladimeji, Paul Curzon and Harold Thimbleby. In 4th International Symposium on Foundations of Healthcare Information Engineering and Systems (FHIES2014). Washington DC, USA, 2014
[Combining PVSio with Stateflow] (http://www.chi-med.ac.uk/research/downloadandcount.php?PPnum=PP204) Paolo Masci, Yi Zhang, Paul Jones, Patrick Oladimeji, Enrico D'Urso, Cinzia Bernardeschi, Paul Curzon, Harold Thimbleby Proceedings of 6th NASA Formal Methods Symposium (NFM2014), NASA Johnson Space Center, Houston, TX, 2014
[Model-based development of the Generic PCA infusion pump user interface prototype in PVS.] (http://www.chi-med.ac.uk/research/downloadandcount.php?PPnum=PP120) Paolo Masci, Anaheed Ayoub, Paul Curzon, Insup Lee, Oleg Sokolsky, Harold Thimbleby. Proceedings of Safecomp2013, 32nd International Conference on Computer Safety, Reliability and Security, LAAS-CNRS, Toulouse, France, 2013
[Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example.] (http://www.chi-med.ac.uk/research/downloadandcount.php?PPnum=PP114) Paolo Masci, Anaheed Ayoub, Paul Curzon, Michael Harrison, Insup Lee, Harold Thimbleby. In EICS2013, 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, London, UK, 2013
[On formalising interactive number entry on infusion pumps.] (http://www.chi-med.ac.uk/research/downloadandcount.php?PPnum=PP021) Paolo Masci, Rimvydas Ruksenas, Patrick Oladimeji, Abigail Cauchi, Andy Gimblett, Karen Li, Paul Curzon, Harold Thimbleby. In FMIS2011, the 4th Intl. Workshop on Formal Methods for Interactive Systems. Limerick, Ireland, 2011