Abstract
PVSio-web is a graphical environment for facilitating the design and evaluation of interactive (human-computer) systems. Using PVSio-web, one can generate and evaluate realistic interactive prototypes from formal models. PVSio-web has been successfully used over the last two years for analyzing commercial, safety-critical medical devices. It has been used to create training material for device developers and device users. It has also been used for medical device design, by both formal methods experts and non-technical end users.
This paper presents the latest release of PVSio-web 2.0, which will be part of the next PVS distribution. The new tool architecture is discussed, and the rationale behind its design choices are presented.
PVSio-web Tool: http://www.pvsioweb.org
US Government (outside the US) 2015. The rights of this work are transferred to the extent transferrable according to title 17 U.S.C. 105.
You have full access to this open access chapter, Download conference paper PDF
Similar content being viewed by others
Keywords
1 Introduction
Inadequate user interface design is repeatedly reported as a root cause of many incidents in healthcare [1, 2], avionics [3], and other safety-critical domains [4]. Design and analysis of user interfaces often requires a multidisciplinary team of human factors specialists, engineers, and end users to validate requirements, specifications, and implementation details. Rigorous formal methods tools can enable early identification of potential design issues. State-of-the-art verification tools like PVS [5], however, generally have minimal front-ends that create barriers when formal methods experts need to work in a multidisciplinary team and engage with non-experts of formal methods technologies — e.g., to validate hypotheses included in the formal models, or to discuss formal analysis results.
The tool presented in this paper, PVSio-web, significantly reduces these barriers. PVSio-web is a web-based environment for modeling and prototyping interactive (human-computer) systems in PVS, and is particularly suitable for: validating hypotheses included in formal models and formal properties before starting the verification process; demonstrating formal analysis results to engineers and domain specialists in a way that is easy to comprehend; and enabling lightweight formal analysis of user interfaces based on user-centred design methods, such as user testing and expert walkthroughs of prototypes. PVSio-web can be freely downloaded with the latest version of PVS [6] or from our repository [7].
Related Work. SCR [8] is a toolset for the analysis of system requirements and specifications. Using SCR, one can formally specify the behavior of a system, use visual front-ends for demonstrating the system behavior based on the specifications, and use a group of formal methods tools (including PVS) for the analysis of system properties. In contrast to our tool, SCR lacks specialized functionalities needed for the analysis of user interfaces, such as rapid generation of user interface prototypes, deployment of prototypes on mobile devices, and logging of user interactions. Simulink [9] is a de-facto standard environment for model-based design and analysis of dynamic systems. It provides a graphical model editor based on Statecharts, and functions for rapid generation of realistic prototypes. Unlike our tool, Simulink offers very limited functions for prototyping user interface designs. More importantly, its architecture is not open, preventing it from being used with PVS or other formal analysis tools. In [10], an approach to develop realistic device prototypes using graph models and interactive pictures is presented, but the approach is not supported by a development environment, and the prototypes are manually crafted. PetShop [11], IVY [12] and similar verification tools for formal analysis of user interfaces lack functions for rapid generation of realistic prototypes. Other verification tools like Bandera [13] and PVSioChecker [14] are not specialized for user interface analysis, and features such as rapid prototyping are out of their intended functionalities.
2 PVSio-web: System Overview and Applications
PVSio-web provides a formal methods based, sophisticated graphical front-end for modeling and prototyping interactive (human-computer) systems. It transforms the animation capabilities of PVS, and enables the user to rapidly generate realistic prototypes in two steps: first, a picture of the user interface is loaded into the tool; second, programmable areas are created over the picture and linked to the formal model specifying the human-system interaction. Programmable areas for input widgets (e.g., buttons) over the user interface picture define how user actions are translated into PVS expressions that can be animated within PVSio [15], the native animation environment of PVS. Programmable areas for output widgets (e.g., displays), on the other hand, define how results returned by PVSio are rendered into visual elements of the prototype, so the visual appearance of the prototype can closely resemble the appearance of the real system in the corresponding state.
Figure 1(a) is a screenshot of PVSio-web generating a prototype, where framed boxes are programmable overlay areas: thus, our tool embeds a script in the area over button “0” that translates click actions over the button into a PVS expression click_0(st), and evaluates this expression in PVSio. The function click_0 is defined in the PVS model of the system, st being the current model state. Our tool automatically keeps track of model states during interaction with the prototype, and seamlessly replaces st with the current model state. The overlay over the display region renders the value of PVS expressions returned by PVSio (here, as numbers).
Applications. PVSio-web has been applied successfully in the analysis of commercial medical devices. Using PVSio-web, we have:
-
demonstrated previously undetected design issues in medical devices [16, 17],
-
created training material [22] for device developers and users.
For example, the prototype shown in Fig. 1(a) is one of many that have been used to analyze real medical devices, here a drug infusion pump. Our analysis focused on the data entry defining how the infusion pump responds when the user enters configuration parameters, such as therapy data or patient data. The PVS model of the infusion pump’s user interface was obtained by translating the source-code implementation of its user interface software into a PVS theory. Using PVSio-web, we generated a realistic prototype based on the formal model, and used it to perform quick exploratory analyses of the model to understand how to best formalize human factors principles as PVS theorems. An example human factors principle is consistency, asserting that the same user actions should produce the same results in logically equivalent situations. We formalized this principle as a PVS theorem that checks whether the data entry interaction of the device consistently registered button clicks in all states. This theorem allowed us to discover previously undetected issues with the decimal point (full details of the analysis are in [16]). The same prototype was also used to demonstrate the identified design issues to regulators and real device users (nurses, doctors, medical device trainers), resulting in the recognition of the safety implications of these issues. This and other prototypes generated using PVSio-web are currently used in training material for hospitals [23], device manufacturers, and regulators to raise awareness about general user interface software issues [22].
3 The PVSio-web Architecture
The architecture of the latest release of PVSio-web is shown in Fig. 2. It follows the Model-View-Controller design pattern [24], creating a clear separation between modules responsible for the behavior of the prototype and those for its visual appearance. In particular, the behavior of a prototype is entirely specified using PVS executable models animated within PVSio. PVSio is used as is, without any modification that might compromise its correctness or sound integration with PVS.
PVSio-web provides multiple facets; that is, it combines different development environments specifically designed for different target users. One facet, Simulator View, is designed for domain specialists and end users: it includes only elements and functionalities for exploring the behavior of prototypes generated with PVSio-web. The other facets are designed for developers and formal methods specialists. They provide tools for creating the visual appearance of the prototype (Prototype Builder), and for editing the PVS model. Advanced PVS users can use the Model Editor for editing and type-checking PVS models; developers who are novice PVS users can use a visual model editor (Emucharts Editor) for developing formal models using a graphical notation based on Statecharts [25]. The facets work well together, allowing people with different background and expertise to work together with the same underlying formal models.
\(\blacktriangleright \) The Simulator View handles the execution of prototypes developed within PVSio-web, and logs user interactions with the prototype. This module renders the visual elements of the prototype, and implements functions for detecting and logging user actions over input widgets. It also translates user actions performed on the input widgets into PVS expressions; triggers the evaluation of PVS expressions in PVSio; and renders PVS expressions returned by PVSio into visual elements of the prototype. Translation of user actions into PVS expressions, and rendering of PVS expressions into visual elements are performed in real time using template scripts created with Prototype Builder. Example prototypes executed within Simulator View are illustrated in [17, 22].
\(\blacktriangleright \) The Prototype Builder automates the generation of a prototype, providing a graphical environment with functions for defining the visual aspect of the prototype (typically, a picture) and for creating programmable overlay areas that enable interaction with the prototype. Overlay areas corresponding to input widgets define which user actions are recognized (e.g., press, release, click) and how these actions are translated into PVS expressions. The translation is performed using templates that map user actions to PVS functions on the basis of naming conventions. An example template is , which translates clicks performed by the user over a button into a PVS function that takes one parameter , representing the current model state. Areas corresponding to output widgets use string filters to extract the actual value of the widget from PVS expressions returned by PVSio.
\(\blacktriangleright \) The EmuCharts Editor implements a visual editor and code generators for creating executable formal models. With this module, developers can: define states by drawing labelled boxes; define transitions by drawing labelled arrows; define variables representing relevant characteristics of the system; and generate executable models from the visual diagram. Model generators employ constructs from languages supported by popular analysis tools and programming languages: state labels are translated into enumerated type constants; state variables are translated into fields of a record type defining the system state; state transitions are translated into transition functions over system states. Language constructs for checking well-formedness of the model are automatically embedded in the generated models. For example, the PVS model generator introduces subtyping [26] relations so that consistency and coverage of conditions can be checked with the PVS type-checker (e.g., see the PVS model snippet in Fig. 1(c)).
\(\blacktriangleright \) The Model Editor is a text editor for editing formal models, providing the typical functionalities of modern IDEs (syntax highlighting, autocomplete, search, etc.) as well as a file browser to perform operations on the file system.
\(\blacktriangleright \) The PVSio Wrapper spawns PVSio processes needed for model animation, and hides the native read-eval-print loop of PVSio behind an API implementing a standard observer pattern [27], with functions for sending commands to PVSio, and for receiving call-backs when PVSio returns a result. This module implements mechanisms to disable inappropriate configurations of our tool, e.g., it disallows spawning multiple concurrent instances of PVSio for demonstrating concurrent systems (the demonstration of such systems must be based on a PVS model that explicitly defines the concurrent behavior).
\(\blacktriangleright \) The Co-Simulator creates a communication infrastructure that enables exchange of simulation events and data between PVS models animated within PVSio and models animated within other simulation environments. This module is particularly useful for the development and evaluation of complex systems. In particular, a development team can employ different modeling and analysis tools for different parts of a complex system, while using the Co-Simulator to verify system properties in a coordinated simulation environment. Example prototypes using this module to perform co-simulation of PVS models and Simulink models are described in [28, 29].
4 Implementation
The core modules of PVSio-web are entirely implemented in JavaScript, which eases the deployment of PVSio-web to mobile devices (tablets, smartphones, etc.) allowing demonstrations to be given conveniently to domain experts. A client-server architecture is used, in which the server builds on NodeJS [30] and the client relies on the JavaScript engine of web browsers. Jison [31] is employed to automatically generate language parsers from production rules. Model generators use Handlebars [32] for generating formal specifications from model templates. PVSio-web 2.0 includes model generators for PVS, MAL [12], PIM [33], and VDM-SL [34]. PVSio-web text editors build on CodeMirror [35]. PVSio-web visual editors build on D3.js [36].
PVSio-web was first released in early 2013 [37]. The tool has been continuously extended with new features, and re-engineered to improve modularity and the overall code quality. JSLint [38] and Jasmine [39] are routinely used to ensure that our implementation is compliant with established coding standards and that the code is well-formed. The latest version of PVSio-web consists of 18,000 lines of JavaScript code.
5 Conclusions and Future Directions
PVSio-web shows it is possible and productive to make realistic user interfaces, with all the benefits of web access (mobility, platform independence), connected closely to formal methods tools. PVSio-web makes professional formal methods accessible to end users and others, as is required in best practice for user interface design. We believe that our tool has the potential to improve the development of safe and dependable device user interfaces, as it facilitates using formal methods practices in an area of product design that has typically not made use of this technology. The tool is gaining popularity: it was downloaded over 1,600 times in 2014 [40]; research groups are exploring applications of the tool to the analysis of commercial products in other application domains (e.g., Honeywell is using it to analyze flight decks [41]). PVSio-web has been successfully used in tutorials [42, 43] to explain the structure of PVS models, and the meaning of PVS theorems to researchers and students that were not familiar with formal methods. Other universities [44–47] are also using our tool as a basis for projects and student theses. Current and future development directions include improved support for advanced formal verification techniques. For example, we are developing a new visual front-end, Proof Explorer [48], to ease the demonstration of formal proofs, the generation of test cases from verification results, and the development of proof strategies specialized for the analysis of user interface software (example strategies are informally described in [21]). We are additionally developing model generators and co-simulators to link our tool with other popular formal methods tools, including SAL [49], KeYmaera [50], and Uppaal [51]. We are also regularly adding new case studies in medical and other domains, e.g., for avionics and aerospace.
References
Simone, L.: Software-related recalls: an analysis of records. Biomed. Instrum. Technol. 47(6), 514–522 (2013)
US Food and Drug Administration (FDA), Manufacturer and User Facility Device Experience Database (MAUDE). http://www.fda.gov/MedicalDevices/DeviceRegulationandGuidance/PostmarketRequirements/ReportingAdverseEvents/ucm127891.htm
Gelman, G., Feigh, K., Rushby, J.: Example of a complementary use of model checking and human-performance simulation. IEEE Trans. Hum. Mach. Syst. 44(5), 576–590 (2014)
Millett, L., Thomas, M., Jackson, D., et al.: Software for Dependable Systems: Sufficient Evidence?. National Academies Press, Washington, DC (2007)
Owre, S., Rushby, J., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)
PVS Specification and Verification System – GitHub repository. https://github.com/samowre/PVS
PVSio-web - Interactive human-computer systems modelling and prototyping tool. http://www.pvsioweb.org
Heitmeyer, C., Kirby, J., Labaw, B., Bharadwaj, R.: SCR: a toolset for specifying and analyzing software requirements. In: Vardi, M.Y., Hu, A.J. (eds.) CAV 1998. LNCS, vol. 1427, pp. 526–531. Springer, Heidelberg (1998)
Mathworks Simulink. http://www.mathworks.com/products/simulink
Thimbleby, H., Gow, J.: Applying graph theory to interaction design. In: Gulliksen, J., Harning, M.B., van der Veer, G.C., Wesson, J. (eds.) EIS 2007. LNCS, vol. 4940, pp. 501–519. Springer, Heidelberg (2008)
Palanque, P., Ladry, J.-F., Navarre, D., Barboni, E.: High-Fidelity Prototyping of Interactive Systems Can Be Formal Too. In: Jacko, J.A. (ed.) HCI International 2009, Part I. LNCS, vol. 5610, pp. 667–676. Springer, Heidelberg (2009)
Campos, J., Harrison, M.: Interaction engineering using the IVY tool. In: Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS09), pp. 35–44. ACM (2009)
Hatcliff, J., Dwyer, M.B., Păsăreanu, C.S.: Foundations of the Bandera abstraction tools. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 172–203. Springer, Heidelberg (2002)
Dutle, A.M., Muñoz, C.A., Narkawicz, A.J., Butler, R.W.: Software validation via model animation. In: Blanchette, J.C., Kosmatov, N. (eds.) TAP 2015. LNCS, vol. 9154, pp. 92–108. Springer, Heidelberg (2015)
Muñoz, C.: Rapid prototyping in PVS, Technical report NIA Report No. 2003–03, NASA/CR-2003-212418. National Institute of Aerospace (2003)
Masci, P., Zhang, Y., Jones, P., Curzon, P., Thimbleby, H.: Formal verification of medical device user interfaces using PVS. In: Gnesi, S., Rensink, A. (eds.) FASE 2014 (ETAPS). LNCS, vol. 8411, pp. 200–214. Springer, Heidelberg (2014)
Masci, P., Oladimeji, P., Curzon, P., Thimbleby, H.: Tool demo: Using PVSio-web to demonstrate software issues in medical user interfaces. In: 4th International Symposium on Foundations of Healthcare Information Engineering and Systems (FHIES 2014) (2014)
Masci, P., Ayoub, A., Curzon, P., Harrison, M., Lee, I., Thimbleby, H.: Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. In: EICS2013, 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems. ACM Digital Library (2013)
Masci, P., Ayoub, A., Curzon, P., Lee, I., Sokolsky, O., Thimbleby, H.: Model-based development of the generic PCA infusion pump user interface prototype in PVS. In: Bitsch, F., Guiochet, J., Kaâniche, M. (eds.) SAFECOMP. LNCS, vol. 8153, pp. 228–240. Springer, Heidelberg (2013)
Masci, P., Rukšėnas, R., Oladimeji, P., Cauchi, P., Gimblett, A., Li, Y., Curzon, P., Thimbleby, H.: The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps. Innovations Syst. Softw. Eng. 11(2), 73–93 (2013)
Harrison, M., Masci, P., Campos, J., Curzon, P.: Demonstrating that medical devices satisfy user related safety requirements. In: 4th International Symposium on Foundations of Healthcare Information Engineering and Systems (FHIES 2014) (2014)
Masci, P.: Design issues in medical user interfaces. https://www.youtube.com/watch?v=T0QmUe0bwL8
Masci, P.: Data entry issues in medical devices. Seminar given within the Washington Adventist Hospital’s Continuing Medical Education (CME) Program (2014)
Krasner, G., Pope, S.: A description of the model-view-controller user interface paradigm in the Smalltalk-80 system. J. Object Oriented Program. 1(3), 26–49 (1988)
Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8, 231–274 (1987)
Shankar, N., Owre, S.: Principles and pragmatics of Subtyping in PVS. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 37–52. Springer, Heidelberg (2000)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-oriented Software. Pearson Education, Upper Saddle River (1994)
Masci, P., Zhang, Y., Jones, P., Oladimeji, P., D’Urso, E., Bernardeschi, C., Curzon, P., Thimbleby, H.: Combining PVSio with Stateflow. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 209–214. Springer, Heidelberg (2014)
Bernardeschi, C., Domenici, A., Masci, P.: Integrated simulation of implantable cardiac pacemaker software and heart models. In: 2nd International Conference on Cardiovascular Technologies (CARDIOTECHNIX 2014). ScitePress Digital Library (2014). http://www.scitepress.org
Node.js. http://nodejs.org
Jison - JavaScript Parser Generator. http://jison.org
Handlebars Semantic Templates. http://handlebarsjs.com
Bowen, J., Reeves, S.: Modelling safety properties of interactive medical systems. In: Proceedings of the 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS 2013, pp. 91–100. ACM (2013)
Masci, P., Couto, L., Larsen, P., Curzon, P.: Integrating the PVSio-web modelling and prototyping environment with Overture. In: 13th Overture Workshop, Satellite Event of FM 2015 (2015)
CodeMirror text editor for web browsers. http://codemirror.net
D3.js JavaScript library for dynamic creation and control of graphical elements. http://d3js.org
Oladimeji, P., Masci, P., Curzon, P., Thimbleby, H.: PVSio-web: a tool for rapid prototyping device user interfaces in PVS. In: 5th International Workshop on Formal Methods for Interactive Systems (FMIS 2013) (2013). http://www.pvsioweb.org
JSLint - JavaScript Code Quality Tool. http://www.jslint.com
Jasmine - JavaScript Testing Tool. http://jasmine.github.io
Download statistics for package pvsio-web. http://npm-stat.com/charts.html?package=pvsio-web
Hall, B., Bhatt, D.: Formal Specification and Verification of Human Interactive Interfaces Incorporating Voice Control. Project Proposal, Honeywell (2013)
Medical devices and HCI. Full day tutorial at NordiCHI (2014). http://cs.swan.ac.uk/~cspo/2014/nordichi/
Masci, P.: Design and analysis of software for interactive medical devices. Ph.D. module at University of Pisa (2014). http://phd.dii.unipi.it/formazione/item/85-dr-paolo-masci
Robb, N.: Exploring Aspects of Automated Test Generation on Models. Waikato University, New Zealand, Honour Project (2015)
Pascoe, I.: Usability study of a system that models interactive systems. Waikato University, New Zealand, Honour Project (2015)
D’Urso, E.: Emulink: a graphical modelling environment for PVS, Master’s thesis. University of Pisa, Italy (2014)
Faria, C.: Web-base user interface prototyping and simulation, Master’s thesis. University of Minho, Portugal (2014)
Proof Explorer. https://github.com/thehogfather/ProofExplorer
de Moura, L., Owre, S., Rueß, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 496–500. Springer, Heidelberg (2004)
Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171–178. Springer, Heidelberg (2008)
Behrmann, G., David, A., Larsen, K., Hakansson, J., Petterson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: Third International Conference on Quantitative Evaluation of Systems. QEST 2006, pp. 125–126. IEEE (2006)
Acknowledgements
This work is part of CHI+MED (EPSRC grant [EP/G059063/1]). The authors would like to thank SRI International, in particular John Rushby, Sam Owre and Natarajan Shankar for supporting the development of our tool.
Disclaimer. The mention of commercial products, their sources, or their use in connection with material reported herein is not to be construed as either an actual or implied endorsement of such products by the U.S. Department of Health and Human Services.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland (outside the US)
About this paper
Cite this paper
Masci, P., Oladimeji, P., Zhang, Y., Jones, P., Curzon, P., Thimbleby, H. (2015). PVSio-web 2.0: Joining PVS to HCI. In: Kroening, D., Păsăreanu, C. (eds) Computer Aided Verification. CAV 2015. Lecture Notes in Computer Science(), vol 9206. Springer, Cham. https://doi.org/10.1007/978-3-319-21690-4_30
Download citation
DOI: https://doi.org/10.1007/978-3-319-21690-4_30
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-21689-8
Online ISBN: 978-3-319-21690-4
eBook Packages: Computer ScienceComputer Science (R0)