Location: CLT701 Date/Time: 9th September 2014, 14:00 - 16:00
Speaker(s): Dr. Paolo Masci.
Brief Description:In this talk, we illustrate our work carried out in collaboration with the FDA for the analysis of user interface software using formal methods technologies. A concrete example is presented that involved the analysis of user software source code from a marketed device. The source code is formally analysed within the Prototype Verification System (PVS), a state-of-the-art formal methods technology developed at SRI International. First, the source code of the device is transformed into an executable PVS model. Then, the PVS model is verified against relevant safety and usability requirements using the PVS theorem prover. During the analysis, realistic prototypes of the device are automatically generated using the PVSio-web prototyping environment with the aim to assess the relevance of identified design issues/flaws.