Model-driven development of high-assurance active medical devices

• 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