User interface prototyping within PVSio-Web

Interactive software and devices are becoming increasingly common in safety-critical environments, such as hospitals and manufacturing. To verify that such devices behave correctly and safely formal models can be used to describe their behaviour in a way that allows mathematical proof of their robustness.

PVSio Web is a web-based application for creating and evaluating such formal models, focused around allowing graphical interactive prototypes to be generated from existing formal models.

Recognizing the similarity between the formal models being created and the expressiveness of modern prototyping tools (such as InVision and Marvel), I worked under the supervision of Professor Steve Reeves to bridge these two areas, within PVSio-Web. The result was a tool that allows images of interfaces to be annotated with “hotspots” to create simple multi-screen interactive prototypes, while also generating valid formal models.

The technical work for this involved integrating with and extending the Backbone-based PVsio-Web codebase, using D3 to generate charts and refactoring the application’s styling to follow a more modern, SASS-based approach.

I received the John Turner Prize from the University of Waikato’s Computer Science Department for achieving the highest mark for the honours report written on the work. The work was also presented as a paper in 2018 at the 4th Workshop on Formal Integrated Development Environment in Oxford.