文章基本信息

标题：PVSio-web: a tool for rapid prototyping device user interfaces in PVS
本地全文：下载
作者：Patrick Oladimeji ; Paolo Masci ; Paul Curzon 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2013
卷号：69
期号：0
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：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.