Fork me on GitHub

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.

Run PVSio-web from our Web Server Download PVSio-web

Publications


Tool papers

  1. ``PVSio-web 2.0: Joining PVS to HCI.'' P. Masci, P. Oladimeji, Y. Zhang, P. Jones, P. Curzon, H. Thimbleby. Proceedings of 27th International Conference on Computer Aided Verification (CAV2015). California, USA, 2015. [PDF]
  2. ``PVSio-web: a tool for rapid prototyping device user interfaces in PVS.''Patrick Oladimeji, Paolo Masci, Paul Curzon and Harold ThimblebyProceedings of the 5th International Workshop on Formal Methods for Interactive Systems (FMIS 2013). London, UK, 2013 [PDF]

Applications

  1. ``The benefits of formalising design guidelines: A case study on the predictability of drug infusion pumps.'' P. Masci, R. Rukšėnas, P. Oladimeji, A. Cauchi, A. Gimblett, Y. Li, P. Curzon, H. Thimbleby. In Innovations in Systems and Software Engineering, Vol 11(2), Springer-Verlag. London, 2015 [PDF]
  2. ``Formal Verification of Medical Device User Interfaces Using PVS.'' P. Masci, Y. Zhang, P. Jones, P. Curzon, H. Thimbleby. In ETAPS/FASE2014, 17th International Conference on Fundamental Approaches to Software Engineering, Grenoble, France, 2014 [PDF]
  3. ``Tool demo: Using PVSio-web to demonstrate software issues in medical user interfaces.'' P. Masci, P. Oladimeji, P. Curzon and H. Thimbleby. In 4th International Symposium on Foundations of Healthcare Information Engineering and Systems (FHIES2014). Washington DC, USA, 2014 [PDF]
  4. ``Combining PVSio with Stateflow.'' P. Masci, Y. Zhang, P. Jones, P. Oladimeji, E. D’Urso, C. Bernardeschi, P. Curzon and H. Thimbleby. In 6th NASA Formal Methods Symposium (NFM2014). Houston, TX, 2014 [PDF]
  5. ``Model-based development of the Generic PCA infusion pump user interface prototype in PVS.'' P. Masci, A. Ayoub, P. Curzon, I. Lee, O. Sokolsky, H. Thimbleby. In Safecomp2013, 32nd International Conference on Computer Safety, Reliability and Security. Toulouse, France 2013 [PDF]
  6. ``Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example.'' P. Masci, A. Ayoub, P. Curzon, M.D. Harrison, I. Lee, H. Thimbleby. In EICS2013, 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, London, UK, 2013 [PDF]
  7. ``On formalising interactive number entry on infusion pumps.'' P. Masci, R. Rukšėnas, P. Oladimeji, A. Cauchi, A. Gimblett, Y. Li, P. Curzon, H. Thimbleby. In FMIS2011, the 4th Intl. Workshop on Formal Methods for Interactive Systems. Limerick, Ireland, 2011 [PDF]