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

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
This seminar is best suited for software engineers in the
medical devices and safety-critical embedded market.

Hobbs, Senior Developer, Safe Systems, QNX Software Systems

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

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.