Integrating User Design and Formal Models within PVSio-Web
This work addresses the gap for designers and developers in creating verifiable interactive systems, though it is incremental in integrating existing prototyping and modeling concepts.
The paper tackled the separation between user experience design tools and formal modeling systems by developing a tool that generates state machine diagrams and formal models from interactive prototypes, enabling designers to create formal models without specialized expertise.
Creating formal models of interactive systems has wide reaching benefits, not only for verifying low-level correctness, but also as a tool for ensuring user interfaces behave logically and consistently. Despite this, tools for designing user experiences and tools for creating and working with formal models are typically distinctly separate systems. This work aims to bridge this divide by allowing the generation of state machine diagrams and formal models via a simple, interactive prototyping tool that mirrors the basic functionality of many modern digital prototyping applications.