PVSio-web: a tool for rapid prototyping device user interfaces in PVS

Authors

Patrick Oladimeji
Paolo MasciQueen Mary University London
Paul CurzonQueen Mary University London
Harold ThimblebySwansea University

DOI:

https://doi.org/10.14279/tuj.eceasst.69.963

Abstract

We present PVSio-web which extends the simulation component of the PVS proof system with functionalities for rapid prototyping device user interfaces. The tool presents itself as a classic image-editing environment with functionalities such as area selection and hyperlink creation, thus reducing the barriers that prevent non-experts in formal methods from using PVS. Designers load a picture of the layout of the device user interface under development, specify interactive areas over the layout, and link them to a PVS specification. They can then explore the behaviour of the formal user interface specification through point-and-click interactions. The architecture of the tool is general, and can be used as the basis for extending other verification tools. A demonstration of the capabilities of PVSio-web is presented through an example based on a commercial medical device user interface. Our ultimate aim is to promote and facilitate the use of formal verification tools when developing device user interfaces.

Downloads

Published

2014-10-25

How to Cite

[1]

P. Oladimeji, P. Masci, P. Curzon, and H. Thimbleby, “PVSio-web: a tool for rapid prototyping device user interfaces in PVS”,ECEASST, vol. 69, Oct. 2014.