Paolo Masci

Citation:

Oladimeji P, Masci P, Curzon P, Thimbleby H.  2013.  PVSio-web: a tool for rapid prototyping device user interfaces in PVS. FMIS2013, 5th International Workshop on Formal Methods for Interactive Systems, London, UK, June 24, 2013. 69 copy at www.tinyurl.com/y2yxuktn

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.

Citation Key: