@conference { fmis2013-pvsioweb,
	title = {PVSio-web: a tool for rapid prototyping device user interfaces in PVS},
	booktitle = {FMIS2013, 5th International Workshop on Formal Methods for Interactive Systems, London, UK, June 24, 2013},
	volume = {69},
	year = {2013},
	publisher = {ECEASST},
	organization = {ECEASST},
	abstract = {<p>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.</p>
},
	attachments = {https://haslab.uminho.pt/sites/default/files/masci/files/fmis2013.pdf},
	author = {Patrick Oladimeji and Paolo Masci and Paul Curzon and Harold Thimbleby}
}