Home

Paolo Masci edited this page Apr 29, 2016 · 13 revisions
Clone this wiki locally

About PVSio-web

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

Live demos of realistic medical devices are executed on a free Amazon EC2 cloud server. Links to these live demos can be found at www.pvsioweb.org

Publications

Tool papers

PVSio-web 2.0: Joining PVS to HCI. 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. 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

Applications

The benefits of formalising design guidelines: A case study on the predictability of drug infusion pumps. 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 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. 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 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. 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. 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. 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