Skip to main content
SpringerLink
Log in

Model-driven development of high-assurance active medical devices

  • Published:
Software Quality Journal Aims and scope Submit manuscript

Abstract

Advanced medical devices exploit the advantages of embedded software whose development is subject to compliance with stringent requirements of standardization and certification regimes due to the critical nature of such systems. This paper presents initial results and lessons learned from an ongoing project focusing on the development of a formal model of a subsystem of a software-controlled safety-critical active medical device (AMD) responsible for renal replacement therapy. The use of formal approaches for the development of AMDs is highly recommended by standards and regulations, and motivates the recent advancement of the state of the art of related methods and tools including Event-B and Rodin applied in this paper. It is expected that the presented model development approach and the specification of a high-confidence medical system will contribute to the still sparse experience base available at the disposal of the scientific and practitioner community of formal methods and software engineering.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16
Fig. 17

Similar content being viewed by others

Notes

  1. Hemodiafiltration (HDF) is a process in which a high rate of ultrafiltration is used for dialysis.

References

  • Abrial, J. R. (1996). The B book. Cambridge: Cambridge University Press.

    Book  MATH  Google Scholar 

  • Abrial, J. R. (2010). Modeling in Event-B: System and software engineering. Cambridge: Cambridge University Press.

    Book  MATH  Google Scholar 

  • Abrial, J. R., Butler, M., Hallerstede, S., Hoang, T., Mehta, F., & Voisin, L. (2010). Rodin: An open toolset for modelling and reasoning in Event-B. International Journal on Software Tools for Technology Transfer, 12(6), 447–466.

    Article  Google Scholar 

  • Abrial, J. R., & Hallerstede, S. (2007). Refinement, decomposition, and instantiation of discrete models: Application to Event-B. Fundamenta Informaticae, 77(1–2), 1–28.

    MathSciNet  MATH  Google Scholar 

  • Ad hoc Working Group on Risk Assessment and Risk Management. (2006). Risk assessment and risk management methods: Information packages for Small and Medium sized Enterprises (SMEs). Technical report, ENISA.

  • Arney, D., Jetley, R., Jones, P., Lee, I., & Sokolsky, O. (2007). Formal methods based development of a PCA infusion pump reference model: Generic infusion pump (GIP) project. In Joint Workshop on high confidence medical devices, software, and systems and medical device plug-and-play interoperability, 2007. HCMDSS-MDPnP (pp. 23–33).

  • Badeau, F., & Amelot, A. (2005). Using B as a high level programming language in an industrial project: Roissy VAL. In Formal specification and development in Z and B. Volume 3455 of LNCS (pp. 334–354). Berlina: Springer.

  • Bear, S. (1991). An overview of HP-SL. In S. Prehn & W. Toetenel (Eds.), VDM’91 Formal software development methods. Vol. 551 of Lecture Notes in Computer Science (pp. 571–587). Berlin: Springer.

  • Behm, P., Benoit, P., & Meynadier, J. M. (1999). METEOR: A successful application of B in a large project. In FM. Vol. 1708 of LNCS (pp. 369–387). Berlin: Springer.

  • Bjørner, D. (2010). Role of domain engineering in software development—Why current requirements engineering is flawed! In A. Pnueli, I. Virbitskaite, & A. Voronkov (Eds.), Perspectives of systems informatics. Vol. 5947 of Lecture Notes in Computer Science (pp. 2–34). Berlin: Springer.

  • Boehm, B., & Papaccio, P. (1988). Understanding and controlling software costs. IEEE Transactions on Software Engineering, 14(10), 1462–1477.

    Article  Google Scholar 

  • Bowen, J., & Reeves, S. (2013). Modelling safety properties of interactive medical systems. In Proceedings of the 5th ACM SIGCHI symposium on engineering interactive computing systems. EICS’13 (pp. 91–100). New York: ACM.

  • Bowen, J., & Stavridou, V. (1993). Safety-critical systems, formal methods and standards. Software Engineering Journal, 8(4), 189–209.

    Article  Google Scholar 

  • Broadfoot, G. H. (2005). ASD case notes: Costs and benefits of applying formal methods to industrial control software. In J. Fitzgerald, I. Hayes, & A. Tarlecki (Eds.), FM 2005: Formal methods. Vol. 3582 of Lecture Notes in Computer Science (pp. 548–551). Berlin: Springer.

  • Butler, M. (2009). Decomposition structures for Event-B. In Proceedings of the 7th international conference on integrated formal methods. IFM’09 (pp. 20–38). Berlin: Springer.

  • Campos, J. C., & Harrison, M. D. (2008). Systematic analysis of control panel interfaces using formal tools. In T.C. N. Graham and P. Palanque (Eds.), Interactive systems. Design, specification, and verification, Vol. 5136 of Lecture Notes in Computer Science (pp. 72–85). Berlin: Springer.

  • Campos, J. C., & Harrison, M. D. (2011). Modelling and analysing the interactive behaviour of an infusion pump. In Proceedings of 4th International ECEASST.

  • Cansell, D., Mery, D., & Rehm, J. (2007). Time constraint patterns for Event-B development. In J. Julliand & O. Kouchnarenko (Eds.), 7th International conference of B users. Vol. 4355 of LNCS (pp. 140–154). Berlin: Springer.

  • Clarke, E. M., & Wing, J. M. (1996). Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4), 626–643.

    Article  Google Scholar 

  • Dijkstra, E. W. (1972). The humble programmer. Communications of the ACM, 15(10), 859–866.

    Article  Google Scholar 

  • EU. (June 1993). Council Directive 93/42/EEC. Official Journal of the European Union.

  • EU. (September 2007). Directive 2007/47/EC of the European Parliament and of the Council. Official Journal of the European Union.

  • Food and Drug Administration (FDA). (2002). General principles of software validation; Final guidance for industry and FDA Staff.

  • IEC 60601-1:2005. (2005). Medical electrical equipment—Part 1: General requirements for basic safety and essential performance.

  • IEC 61508-3 Ed 2.0. (2010). Functional safety of electrical/electronic/programmable electronic safety-related systems—Part 3: Software requirements.

  • IEC 62304:2006. (2006). Medical device software—Software life cycle processes.

  • Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A., Varpaaniemi, K., Ilic, D., et al. (2013). Developing mode-rich satellite software by refinement in Event-B. Science of Computer Programming, 78(7), 884–905.

    Article  Google Scholar 

  • ISO 13485:2003. (2003). Medical devices—Quality management systems—Requirements for regulatory purposes.

  • Jacky, J. (1990). Formal specification for a clinical cyclotron control system. SIGSOFT Software Engineering Notes, 15(4), 45–54.

    Article  Google Scholar 

  • Jiang, Z., Pajic, M., Connolly, A., Dixit, S., & Mangharam, R. (2010). A platform for implantable medical device validation: Demo abstract. In Wireless Health 2010. WH ’10 (pp. 208–209). New York: ACM.

  • Jones, C. B. (1990). Systematic software development using VDM (2nd ed.). Upper Saddle River, NJ: Prentice-Hall Inc.

    MATH  Google Scholar 

  • Kossak, F., Mashkoor, A., Geist, V., & Illibauer, C. (2014). Improving the understandability of formal specifications: An experience report. In C. Salinesi & I. Weerd (Eds.), Requirements engineering: Foundation for software quality. Vol. 8396 of Lecture Notes in Computer Science (pp. 184–199). Berlin: Springer.

  • Leuschel, M., & Butler, M. (2003). ProB: A model checker for B. In K. Araki, S. Gnesi, & D. Mandrioli (Eds.), FME 2003: Formal methods LNCS 2805 (pp. 855–874). Berlin: Springer.

    Chapter  Google Scholar 

  • Macedo, H., Larsen, P., & Fitzgerald, J. (2008). Incremental development of a distributed real-time model of a cardiac pacing system using VDM. In J. Cuellar, T. Maibaum, & K. Sere (Eds.), FM 2008: Formal methods. Vol. 5014 of Lecture Notes in computer science (pp. 181–197). Berlin: Springer.

  • Mashkoor, A. (2015). The hemodialysis machine case study. Technical report SCCH-TR-1542. Austria: Software Competence Center Hagenberg GmbH.

  • Mashkoor, A., & Jacquot, J. P. (2015). Observation-level-driven formal modeling. In 2015 IEEE 16th International Symposium on High-assurance systems engineering (HASE) (pp. 158–165).

  • Mashkoor, A., & Jacquot, J. P. (Sept 2010). Domain Engineering with Event-B: Some lessons we learned. In Requirements engineering conference (RE), 2010 18th IEEE international (pp. 252–261).

  • Mashkoor, A., Biro, M., Dolgos, M., & Timar, P. (2015). Refinement-based development of software-controlled safety-critical active medical devices. In Software Quality. Software and Systems Quality in Distributed and Mobile Environments, Vol. 200 of Lecture Notes in Business Information Processing (pp. 120–132). Berlin: Springer.

  • Mashkoor, A., Jacquot, J. P. (2011). Guidelines for Formal Domain Modeling in Event-B. In 2011 IEEE 13th international symposium on high-assurance systems engineering (HASE) (pp. 138–145).

  • Méry, D., & Singh, N. K. (2013). Formal specification of medical systems by proof-based refinement. ACM Transactions on Embedded Computing Systems, 12(1), 15:1–15:25.

    Article  Google Scholar 

  • Osaiweran, A., Schuts, M., Hooman, J., & Wesselius, J. (2013). Incorporating formal techniques into industrial practice: An experience report. Electronic Notes Theoretical Computer Science, 295, 49–63.

    Article  Google Scholar 

  • Plagge, D., & Leuschel, M. (2007). Validating Z specifications using the ProB animator and model checker. In J. Davies & J. Gibbons (Eds.), Integrated formal methods. Vol. 4591 of Lecture Notes in Computer Science (pp. 480–500). Berlin: Springer.

  • Runeson, P., & Höst, M. (2009). Guidelines for conducting and reporting case study research in software engineering. Empirical Software Engineering, 14(2), 131–164.

    Article  Google Scholar 

  • Spivey, J. M. (1988). Understanding Z: A specification language and its formal semantics. Cambridge: Cambridge University Press.

    MATH  Google Scholar 

  • Su, W., & Abrial, J. R. (2014). Aircraft landing gear system: Approaches with Event-B to the modeling of an industrial system. In F. Boniol, V. Wiels, Y. Ait Ameur & K. D. Schewe (Eds.), ABZ 2014: The landing gear case study. Vol. 433 of Communications in computer and information science (pp. 19–35). Berlin: Springer.

  • Sun, J., Liu, Y., & Dong, J. (2008). Model checking CSP revisited: Introducing a process analysis toolkit. In T. Margaria & B. Steffen (Eds.), Leveraging applications of formal methods, verification and validation. Vol. 17 of communications in computer and information science (pp. 307–322). Berlin: Springer.

    Google Scholar 

  • Tuan, L. A., Zheng, M. C., & Tho, Q. T. (2010). Modeling and verification of safety critical systems: A case study on pacemaker. In: 2010 Fourth international conference on secure software integration and reliability improvement (SSIRI) (pp. 23–32).

  • Woodcock, J., Larsen, P. G., Bicarregui, J., & Fitzgerald, J. (2009). Formal methods: Practice and experience. ACM Computing Surveys, 41(4), 19:1–19:36.

    Article  Google Scholar 

Download references

Acknowledgments

The research reported in this article has been supported by the Austrian Ministry for Transport, Innovation and Technology, the Federal Ministry of Science, Research and Economy, and the Province of Upper Austria in the frame of the COMET center SCCH

Author information

Authors and Affiliations

  1. Software Competence Center Hagenberg GmbH, Hagenberg, Austira

    Atif Mashkoor

Authors
  1. Atif Mashkoor
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Atif Mashkoor.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Mashkoor, A. Model-driven development of high-assurance active medical devices. Software Qual J 24, 571–596 (2016). https://doi.org/10.1007/s11219-015-9288-0

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11219-015-9288-0

Keywords

Search

Navigation