One part of demonstrating that a device is accept- ably safe, often required by regulatory standards, is to show that it satisfies a set of requirements known to mitigate hazards. This paper is concerned with how to demonstrate that a user interface software design is compliant with use related requirements. A methodology is presented based on the use of formal methods technologies. The aim is to provide guidance to developers on how to address three key verification challenges: how to validate a model, and show that it is a faithful representation of the device; how to formalize requirements given in natural language, and what are the benefits brought in by the formalization process; how to prove requirements of a model using readily available formal verification tools. A model of a commercial device is used throughout the paper to demonstrate the methodology. A representative set of requirements will be considered. They are based on FDA draft documentation for programmable medical devices, and on best practice in user interface design illustrated in relevant international standards. The presented methodology aims to demonstrate how to achieve the FDA’s agenda of using formal methods that can support the approval process for real medical devices.

Michael D. Harrison, Paolo Masci, José Creissac Campos, Paul Curzon. Verification of user interface software in PVS: the example of FDA requirements and programmable medical devices. (submitted).