Title: Rapid Prototyping and Formal Analysis of Interactive Systems in PVSio-Web
Speaker: Paolo Masci, Post-Doc Researcher, HASLab of the INESC-TEC Research Center (Portugal) and Visiting Researcher, Food and Drug Administration
Date: Thursday, May 3, 2018
Location: NIA, Room 137
Time: 10:00am- 11:00am
Abstract:
PVSio-web [1] is a toolkit for model-based design and analysis of safety-critical systems. The toolkit integrates formal methods technologies (PVSio) and web technologies (HTML5 & JavaScript) to facilitate rapid development of interactive prototypes based on formal models that closely resemble the look & feel of a real system. These prototypes enable a constructive dialog between researchers using the PVS system and domain experts that are not familiar with formal methods technologies, facilitating the validation of PVS models and the demonstration of formal analysis results. PVSio-web has been applied successfully to demonstrate latent software anomalies in commercial devices [2-6], as well as to create training material for device users [7], and to explore design requirements for new systems [8]. In this talk, I will present the main features of the PVSio-web toolkit, which includes an IDE for specifying executable PVS models using a graphical notation based on statechart diagrams, a library for rapid prototyping interactive systems, and an environment for generating PVS theorems and proof tactics for the analysis of general requirements of interactive devices. Concrete examples based on real systems are presented to demonstrate the features of the toolkit and its utility to researchers using the PVS system.
Biography:
Paolo Masci is a post-doctoral researcher at the High Assurance Laboratory (HASLab) of the INESC-TEC Research Center (Portugal), and a visiting researcher at the Center for Devices and Radiological Health of the US Food and Drug Administration (CDRH/FDA). In recent years, he has been a visiting researcher at SRI, NASA Langley, and University of Pennsylvania. He has 15 years’ experience on using verification technologies and developing verification tools. Over the last 10 years, he has extensively used PVS to model and analyze usability and safety aspects of commercial medical system. The results of his work are currently used by regulatory authorities (to improve pre-market review decisions), by hospitals (for training clinicians and to improve their procurement decisions), by manufacturers (to explore design solutions for new devices), and in universities (to support teaching of formal methods). In 2014, together with the CHI+MED team (www.chi-med.ac.uk), he has been awarded a GE Healthcare Award for Outstanding Impact in Health and Wellbeing. Since 2015, he is enrolled as external software expert for the MHRA, the UK medical device regulator. Since 2017, he is contributing to the new interoperability standard AAMI/UL-2800 for the definition of use-related safety requirements for next-generation medical systems.