{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T04:11:09Z","timestamp":1750824669327,"version":"3.41.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319631936"},{"type":"electronic","value":"9783319631943"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63194-3_7","type":"book-chapter","created":{"date-parts":[[2017,7,26]],"date-time":"2017-07-26T15:58:43Z","timestamp":1501084723000},"page":"96-112","source":"Crossref","is-referenced-by-count":7,"title":["From Requirements to Code: Model Based Development of a Medical Cyber Physical System"],"prefix":"10.1007","author":[{"given":"Anitha","family":"Murugesan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mats P. E.","family":"Heimdahl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sanjai","family":"Rayadurgam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Komp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lian","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Baek-Gyu","family":"Kim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oleg","family":"Sokolsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Insup","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,27]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"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\u2013236. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-30080-9_7"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-28891-3_13","volume-title":"NASA Formal Methods","author":"D Cofer","year":"2012","unstructured":"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\u2013140. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28891-3_13"},{"key":"7_CR3","unstructured":"FDA. White Paper: Infusion Pump Improvement Initiative, April 2010"},{"issue":"3","key":"7_CR4","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1109\/52.896248","volume":"17","author":"CA Gunter","year":"2000","unstructured":"Gunter, C.A., Gunter, E.L., Jackson, M., Zave, P.: A reference model for requirements and specifications. IEEE Software 17(3), 37\u201343 (2000)","journal-title":"IEEE Software"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Hammond, J., Rawlings, R., Hall, A.: Will it work? [requirements engineering]. In: Fifth IEEE International Symposium on Requirements Engineering, Proceedings, pp. 102\u2013109 (2001)","DOI":"10.1109\/ISRE.2001.948549"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1109\/TwinPeaks.2013.6614716"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1007\/978-3-540-24617-6_4"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1109\/DASC.2003.1245813"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"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\u2013164, October 2011","DOI":"10.1145\/2038642.2038667"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Knight, J.C.: Safety critical systems: challenges and directions. In: Proceedings of the 24th International Conference on Software Engineering, pp. 547\u2013550. IEEE (2002)","DOI":"10.1145\/581339.581406"},{"key":"7_CR11","unstructured":"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\u2013146 (1997)"},{"key":"7_CR12","unstructured":"MathWorks Inc. Products. http:\/\/www.mathworks.com\/products"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Circular compositional reasoning about liveness. Technical report 1999\u201302, Cadence Berkeley Labs, Berkeley, CA 94704 (1999)","DOI":"10.1007\/3-540-48153-2_30"},{"issue":"4","key":"7_CR14","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/s10009-004-0173-6","volume":"8","author":"SP Miller","year":"2006","unstructured":"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\u2013319 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"7_CR15","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/1646353.1646372","volume":"53","author":"SP Miller","year":"2010","unstructured":"Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58\u201364 (2010)","journal-title":"Commun. ACM"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1109\/MiSE.2013.6595290"},{"key":"7_CR17","unstructured":"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"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1109\/ICCPS.2014.6843718"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1145\/2527269.2527272"},{"key":"7_CR20","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1109\/2.910904","volume":"34","author":"B Nuseibeh","year":"2001","unstructured":"Nuseibeh, B.: Weaving together requirements and architectures. Computer 34, 115\u2013117 (2001)","journal-title":"Computer"},{"key":"7_CR21","first-page":"1","volume":"PP","author":"M Pajic","year":"2010","unstructured":"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\u201312 (2010). In early online access","journal-title":"IEEE Trans. Ind. Inform."},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"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\u2019l Symposium on Software Testing and Analysis (ISSTA) (2008, submitted). http:\/\/crisys.cs.umn.edu\/ISSTA08.pdf","DOI":"10.1145\/1368088.1368111"},{"key":"7_CR23","unstructured":"SAE. http:\/\/www.aadl.info\/aadl\/downloads\/papers\/aadllanguagesummary.pdf"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Sha, L., Gopalakrishnan, S., Liu, X., Wang, Q.: Cyber-physical systems: a new frontier. In: Machine Learning in Cyber Trust, pp. 3\u201313. Springer, New York (2009)","DOI":"10.1007\/978-0-387-88735-7_1"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/978-3-642-28872-2_28"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/2593770.2593776"},{"issue":"2","key":"7_CR27","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1109\/MS.2012.173","volume":"30","author":"MW Whalen","year":"2013","unstructured":"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\u201360 (2013)","journal-title":"IEEE Software"}],"container-title":["Lecture Notes in Computer Science","Software Engineering in Health Care"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63194-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T18:10:23Z","timestamp":1750788623000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63194-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319631936","9783319631943"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63194-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}