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.

Presenters:
Chris Hobbs, Senior Developer, Safe Systems, QNX Software Systems
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.