Towards medical device behavioural validation using Petri nets

Medical devices development and validation are difficult activities due to the critical nature of these products, involving risks to the human lives. Moreover, regulatory agencies are increasing the control over companies because of the still huge number of harms caused for several reasons, having software failures as one of the main causes. Thus it is clear that more formal and sophisticated software development techniques should be investigated. In this paper, we show how Petri nets can play the role of a generic framework for architectural decisions for control systems, allowing besides verification/simulation, an important bridge in the requested traceability by regulatory bodies. We claim that it is possible to satisfy traceability from architectural elements to code, test cases, functional and safety requirements and so on. In order to make clear our point, we conducted a case study from a generic infusion pump specification.