Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Software Quality Journal
Erschienen in: Software Quality Journal 3/2016

01.09.2016

Model-driven development of high-assurance active medical devices

verfasst von: Atif Mashkoor

Erschienen in: Software Quality Journal | Ausgabe 3/2016

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.
Vorheriger Artikel Understanding the gap between software process practices and actual practice in very small companies
Nächster Artikel Special issue on quality in model-driven engineering

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
Hemodiafiltration (HDF) is a process in which a high rate of ultrafiltration is used for dialysis.
 
Literatur
Abrial, J. R. (2010). Modeling in Event-B: System and software engineering. Cambridge: Cambridge University Press.CrossRefMATH
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.CrossRef
Abrial, J. R., & Hallerstede, S. (2007). Refinement, decomposition, and instantiation of discrete models: Application to Event-B. Fundamenta Informaticae, 77(1–2), 1–28.MathSciNetMATH
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.CrossRef
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.CrossRef
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.CrossRef
Dijkstra, E. W. (1972). The humble programmer. Communications of the ACM, 15(10), 859–866.CrossRef
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.CrossRef
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.CrossRef
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
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.CrossRef
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.CrossRef
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.CrossRef
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.CrossRef
Spivey, J. M. (1988). Understanding Z: A specification language and its formal semantics. Cambridge: Cambridge University Press.MATH
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.
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.CrossRef
Metadaten
Titel
Model-driven development of high-assurance active medical devices
verfasst von
Atif Mashkoor
Publikationsdatum
01.09.2016
Verlag
Springer US
Erschienen in
Software Quality Journal / Ausgabe 3/2016
Print ISSN: 0963-9314
Elektronische ISSN: 1573-1367
DOI
https://doi.org/10.1007/s11219-015-9288-0

Weitere Artikel der Ausgabe 3/2016

Software Quality Journal 3/2016 Zur Ausgabe

OriginalPaper

A research framework for building SPI proposals in small organizations: the COMPETISOFT experience

OriginalPaper

Assessing and improving quality of QVTo model transformations

OriginalPaper

Understanding the gap between software process practices and actual practice in very small companies

EditorialNotes

Special issue on software and service improvement in the scope of SMEs

OriginalPaper

Measuring the complexity of domain-specific languages developed using MDD

OriginalPaper

Timing consistency checking for UML/MARTE behavioral models