Lessons learned: using formal methods to develop medical device software

Overview
For many years, formal methods have promised great things for the development of safety-critical software, such as that used in medical devices. If we can ”prove” our design to be correct, we will be able, not only to reduce implementation and test times, but also to use the proof as compelling evidence during the device approval process. Unfortunately, except for a few well-publicised exceptions, formal methods have failed to meet expectations when applied to the development of commercial products.

As a result of a major initiative funded by the European Union, practical tools are now emerging that allow formal construction of software. Thanks to this formal construction we now build the proof that our design is correct as we build the product.

This webinar describes the experiences QNX has had in applying Rodin, the European formal design tool, to the design of software for a simple medical device.

We will discuss:

• what worked
• what didn't work
• how much work was required to use the tool
• what skills are needed to create a formal specification
• what surprises we uncovered

Finally, we will briefly discuss how the evidence provided by the tool can be used to support a safety case, and how it can help in the approval process.

Estimated length: 1 hour, including Q&A

Who should attend: This seminar is best suited for software engineers in the medical devices and safety-critical embedded market.

Speaker biographies:

Chris Hobbs is a kernel developer at QNX, specializing in "sufficiently-available" software: software created with the minimum development effort to meet the availability and reliability needs of the customer; and in producing safe software (in conformance with IEC61508 SIL3). In addition to his software development work, Chris is a flight instructor, a singer with a particular interest in Schubert's Lieder, and the author of several books, including Flying Beyond: the Canadian Commercial Pilot Textbook (2011) and The Largest Number Smaller than Five (2007). His blog, Software Musings, focuses "primarily on software and analytical philosophy".

Chris Hobbs earned a B.Sc., Honours in Pure Mathematics and Mathematical Philosophy at the University of London's Queen Mary and Westfield College.

Yi Zheng - Product Manager QNX Neutrino RTOS Safe Kernel, QNX Software Systems

Yi Zheng is the product manager responsible for the QNX Neutrino RTOS Safe Kernel (certified to IEC 61508 SIL3), the QNX Neutrino RTOS Secure Kernel (certified to Common Criteria EAL 4+), and for the upcoming QNX Neutrino RTOS Certified Plus (certified to IEC 61508 SIL3 and EAL 4+). She also manages the QNX Neutrino RTOS and the QNX Momentics Tool Suite. Prior to joining QNX Software Systems, she worked at Entrust Technologies, Autodesk, and Nortel Networks, designing a wide range of software applications. She holds a Bachelor's in Computer Science and a Master's in Business Administration, and is a certified management accountant.

About QNX Software Systems
QNX Software Systems Limited, a subsidiary of Research In Motion Limited (RIM) (NASDAQ:RIMM; TSX:RIM), is a leading vendor of operating systems, development tools, and professional services for connected embedded systems. Global leaders such as Audi, Cisco, General Electric, Lockheed Martin, and Siemens depend on QNX® technology for vehicle infotainment systems, network routers, medical devices, industrial controllers, security and defense systems, and other mission-critical applications. Founded in 1980, QNX Software Systems Limited is headquartered in Ottawa, Canada; its products are distributed in over 100 countries worldwide. Visit www.qnx.com.

Register now for this web seminar: Lessons learned: using formal methods to develop medical device software