Verification of Medical Devices operation
Software based systems within medical devices are coming under increasing scrutiny as ever more reliance is placed upon them. The focus is not just on devices used within hospitals such as scanners and infusion pumps, but also systems that can be embedded within the body. Various regulatory bodies are becoming increasingly concerned regarding the suitability of evidence for software safety in these types of devices with recent guidance published in the UK by Medicines and Healthcare Products Regulatory Agency (MHRA). The Therac-25 issues investigated by Nancy Leveson is a salutary tale of how the lack of understanding of the user domain, combined with a poor understanding of software development and integration issues can lead to catastrophic events for patients.
These systems need to be shown to be very robust from both a regulatory perspective as well as from a user experience perspective; nurses and doctors, as well as patients, do not wish harm to be caused through the use of medical devices. The typical approach to the development of software based systems has a cost profile heavily weighted towards the end of the project; this represents considerable project risk.
For systems and software in medical devices, the key is to demonstrate that the systems do what has been required, with no side effects. They have to be resilient to user interaction and may have to interact with other systems both within a hospital and, increasingly, within the community maybe over the internet. In some cases, these devices are in-vitro, which makes software updates somewhat challenging from an assurance perspective, let alone a physical one.
The production of evidence should drive the selection of the best development life cycle, processes and tools. The production of verification evidence through either review, analysis or test to provide assurance of resilience should be a by-product of the use of such techniques and be responsive to inevitable change as understanding increases though the development process.
The use of formal methods can be used to provide analysis for both architectures and software. To date, it has been assumed that experts are required to write formal specifications by hand and then to prove the necessary properties using appropriate qualified tools as support. This is not necessarily a quick or repeatable process and where in other industries formal techniques have been used, they have become company specific knowledge, not available to the wider community. Therefore in order for formal techniques to be adopted more widely across industry, they need to be automated in order to achieve the required flexibility, repeatability, have a low training overhead, as well as providing evidence of resilience.
D-RisQ has taken an approach which enables the power of formal methods to be exploited without any specialist training. By using commonly available tools such as Stateflow®, it is now possible for current engineers to develop software systems architectures in a rigorous manner, whilst gaining as a by-product, the required evidence to confidently support system release.
Modelworks® proves that requirements have been correctly captured in a design expressed in Stateflow®, or will show the manner in which compliance has failed. The design can be of a System of Systems, a single system or a software program. It allows a designer to check that the design does what is required. More importantly, it allows a proof that undesired properties will never happen, a check that is typically attempted at the end of a development life-cycle. It is also possible to show behaviour under failure conditions. Modelworks® can be used to show the behaviour of highly distributed Systems-of Systems, including the behaviour of human interaction where necessary.
CLawZ® automatically proves that automatically produced code implements a design expressed in Simulink®. By using the ADI Ada auto-coder or the TargetLink® C auto-coder aligned to the Simulink control system subset, CLawZ® produces evidence that the code correctly implements the design, or shows where the coder has made a mistake. This relieves the need to undertake unit testing thus gaining considerable time benefits.