Abstract
The advanced use of technology in medical devices has improved the way health care is delivered to patients. Unfortunately, the increased complexity of modern medical devices poses challenges for development, assurance, and regulatory approval. In an effort to improve the safety of advanced medical devices, organizations such as FDA have supported exploration of techniques to aid in the development and regulatory approval of such systems. In an ongoing research project, our aim is to provide effective development techniques and exemplars of system development artifacts that demonstrate state of the art development techniques.
In this paper we present an end-to-end model-based approach to medical device software development along with the artifacts created in the process. While outlining the approach, we also describe our experiences, challenges, and lessons learned in the process of formulating and analyzing the requirements, modeling the system, formally verifying the models, generating code, and executing the generated code in the hardware for generic patient controlled analgesic infusion pump (GPCA). We believe that the development artifacts and techniques presented in this paper could serve as a generic reference to be used by researchers, practitioners, and authorities while developing and evaluating cyber physical medical devices.
This work has been partially supported by NSF grants CNS-0931931 and CNS-1035715.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
In Fig. 4, the connections between components are abstracted for visual clarity.
References
Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30080-9_7
Cofer, D., Gacek, A., Miller, S., Whalen, M.W., LaValley, B., Sha, L.: Compositional verification of architectural models. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 126–140. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28891-3_13
FDA. White Paper: Infusion Pump Improvement Initiative, April 2010
Gunter, C.A., Gunter, E.L., Jackson, M., Zave, P.: A reference model for requirements and specifications. IEEE Software 17(3), 37–43 (2000)
Hammond, J., Rawlings, R., Hall, A.: Will it work? [requirements engineering]. In: Fifth IEEE International Symposium on Requirements Engineering, Proceedings, pp. 102–109 (2001)
Heimdahl, M.P.E., Duan, L., Murugesan, A., Rayadurgam, S.: Modeling and requirements on the physical side of cyber-physical systems. In: Second International Workshop on the Twin Peaks of Requirements and Architecture, May 2013
Heimdahl, M.P.E., Rayadurgam, S., Visser, W., Devaraj, G., Gao, J.: Auto-generating test sequences using model checkers: a case study. In: 3rd International Workshop on Formal Approaches to Testing of Software (FATES 2003) (2003)
Joshi, A., Miller, S.P., Heimdahl, M.P.E.: Mode confusion analysis of a flight guidance system using formal methods. In: Proceedings of 22nd Digital Avionics Systems Conference (DASC 2003), vol. 1, p. 2-D. IEEE (2003)
Kim, B.G., Ayoub, A., Sokolsky, O., Lee, I., Jones, P., Zhang, Y., Jetley, R.: Safety-assured development of the GPCA infusion pump software. In: Proceedings of the International Conference on Embedded Software (EMSOFT), pp. 155–164, October 2011
Knight, J.C.: Safety critical systems: challenges and directions. In: Proceedings of the 24th International Conference on Software Engineering, pp. 547–550. IEEE (2002)
Leveson, N., Pinnel, L.D., Sandys, S.D., Koga, S., Reese, J.D.: Analyzing software specifications for mode confusion potential. In: Proceedings of a Workshop on Human Error and System Development, pp. 132–146 (1997)
MathWorks Inc. Products. http://www.mathworks.com/products
McMillan, K.L.: Circular compositional reasoning about liveness. Technical report 1999–02, Cadence Berkeley Labs, Berkeley, CA 94704 (1999)
Miller, S.P., Tribble, A.C., Whalen, M.W., Heimdahl, M.P.E.: Proving the shalls: early validation of requirements through formal methods. Int. J. Softw. Tools Technol. Transf. 8(4), 303–319 (2006)
Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58–64 (2010)
Murugesan, A., Rayadurgam, S., Heimdahl, M.P.E.: Modes, features, and state-based modeling for clarity and flexibility. In: Fifth International Workshop on Modeling in Software Engineering, May 2013
Murugesan, A., Rayadurgam, S., Heimdahl, M.P.E.: Using models to address challenges in specifying requirements for medical cyber-physical systems. In: Fourth workshop on Medical Cyber-Physical Systems, April 2013
Murugesan, A., Sokolsky, O., Rayadurgam, S., Whalen, M., Heimdahl, M.P.E., Lee, I.: Linking abstract analysis to concrete design: a hierarchical approach to verify medical CPS safety. In: International Conference on Cyber-Physical Systems (ICCPS) 2014, April 2014
Murugesan, A., Whalen, M.W., Rayadurgam, S., Heimdahl, M.P.E.: Compositional verification of a medical device system. In: ACM International Conference on High Integrity Language Technology (HILT). ACM, November 2013
Nuseibeh, B.: Weaving together requirements and architectures. Computer 34, 115–117 (2001)
Pajic, M., Mangharam, R., Sokolsky, O., Arney, D., Goldman, J., Lee, I.: Model-driven safety analysis of closed-loop medical systems. IEEE Trans. Ind. Inform. PP, 1–12 (2010). In early online access
Rajan, A., Whalen, M.W., Staats, M., Deng, W., Heimdahl, M.P.E.: The effect of program and model structure on the fault finding ability of MC/DC test suites. In: Proceedings of Int’l Symposium on Software Testing and Analysis (ISSTA) (2008, submitted). http://crisys.cs.umn.edu/ISSTA08.pdf
SAE. http://www.aadl.info/aadl/downloads/papers/aadllanguagesummary.pdf
Sha, L., Gopalakrishnan, S., Liu, X., Wang, Q.: Cyber-physical systems: a new frontier. In: Machine Learning in Cyber Trust, pp. 3–13. Springer, New York (2009)
Staats, M., Gay, G., Whalen, M.W., Heimdahl, M.P.E.: On the danger of coverage directed test case generation. In: 15th International Conference on Fundamental Approaches to Software Engineering (FASE), April 2012
Whalen, M., Murugesan, A., Rayadurgam, S., Heimdahl, M.: Structuring Simulink models for verification and reuse. In: Proceedings of the 6th International Workshop on Modeling in Software Engineering (2014)
Whalen, M.W., Gacek, A., Cofer, D., Murugesan, A., Heimdahl, M.P.E., Rayadurgam, S.: Your what is my how: iteration and hierarchy in system design. IEEE Software 30(2), 54–60 (2013)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Murugesan, A. et al. (2017). From Requirements to Code: Model Based Development of a Medical Cyber Physical System. In: Huhn, M., Williams, L. (eds) Software Engineering in Health Care. SEHC FHIES 2014 2014. Lecture Notes in Computer Science(), vol 9062. Springer, Cham. https://doi.org/10.1007/978-3-319-63194-3_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-63194-3_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-63193-6
Online ISBN: 978-3-319-63194-3
eBook Packages: Computer ScienceComputer Science (R0)