{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:31:52Z","timestamp":1725568312403},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642165603"},{"type":"electronic","value":"9783642165610"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16561-0_31","type":"book-chapter","created":{"date-parts":[[2010,11,2]],"date-time":"2010-11-02T09:50:50Z","timestamp":1288691450000},"page":"312-326","source":"Crossref","is-referenced-by-count":16,"title":["Trustable Formal Specification for Software Certification"],"prefix":"10.1007","author":[{"given":"Dominique","family":"M\u00e9ry","sequence":"first","affiliation":[]},{"given":"Neeraj Kumar","family":"Singh","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"31_CR1","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1080\/105294100277723","volume":"7","author":"K.L. Keatley","year":"1999","unstructured":"Keatley, K.L.: A review of the fda draft guidance document for software validation: guidance for industry. Qual. Assur.\u00a07(1), 49\u201355 (1999)","journal-title":"Qual. Assur."},{"key":"31_CR2","unstructured":"A Research and Development Needs Report by NITRD: High-Confidence Medical Devices: Cyber-Physical Systems for 21st Century Health Care, http:\/\/www.nitrd.gov\/About\/MedDevice-FINAL1-web.pdf"},{"issue":"4","key":"31_CR3","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1049\/sej.1993.0025","volume":"8","author":"J. Bowen","year":"1993","unstructured":"Bowen, J., Stavridou, V.: Safety-critical systems, formal methods and standards. Software Engineering Journal\u00a08(4), 189\u2013209 (1993)","journal-title":"Software Engineering Journal"},{"issue":"4","key":"31_CR4","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/s10009-003-0137-2","volume":"5","author":"R.P. Jetley","year":"2004","unstructured":"Jetley, R.P., Carlos, C., Iyer, S.P.: A case study on applying formal methods to medical devices: computer-aided resuscitation algorithm. STTT\u00a05(4), 320\u2013330 (2004)","journal-title":"STTT"},{"issue":"4","key":"31_CR5","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/MC.2006.113","volume":"39","author":"R. Jetley","year":"2006","unstructured":"Jetley, R., Purushothaman Iyer, S., Jones, P.: A formal methods approach to medical device review. Computer\u00a039(4), 61\u201367 (2006)","journal-title":"Computer"},{"key":"31_CR6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J.R. Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"31_CR7","first-page":"196","volume":"94","author":"J.H. Magee","year":"2003","unstructured":"Magee, J.H.: Validation of medical modeling & simulation training devices and systems. Stud. Health Technol. Inform.\u00a094, 196\u2013198 (2003)","journal-title":"Stud. Health Technol. Inform."},{"key":"31_CR8","unstructured":"Common Criteria, http:\/\/www.commoncriteria.org\/"},{"key":"31_CR9","doi-asserted-by":"crossref","unstructured":"M\u00e9ry, D., Singh, N.K.: Real-time animation for formal specification. In: Complex Systems Design & Management (CSDM), Paris (2010)","DOI":"10.1007\/978-3-642-15654-0_3"},{"issue":"1","key":"31_CR10","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"T. Hoare","year":"2003","unstructured":"Hoare, T.: The verifying compiler: A grand challenge for computing research. J. ACM\u00a050(1), 63\u201369 (2003)","journal-title":"J. ACM"},{"issue":"1","key":"31_CR11","first-page":"28","volume":"110","author":"B.S. Goldman","year":"1974","unstructured":"Goldman, B.S., Noble, E.J., Heller, J.G., Covvey, D.: The pacemaker challenge. CMAJ\u00a0110(1), 28\u201331 (1974)","journal-title":"CMAJ"},{"issue":"4","key":"31_CR12","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2009.09.001","volume":"238","author":"C.L. Heitmeyer","year":"2009","unstructured":"Heitmeyer, C.L.: On the role of formal methods in software certification: An experience report. Electr. Notes Theor. Comput. Sci.\u00a0238(4), 3\u20139 (2009)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1","key":"31_CR13","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1109\/TSE.2007.70772","volume":"34","author":"C.L. Heitmeyer","year":"2008","unstructured":"Heitmeyer, C.L., Archer, M., Leonard, E.I., McLean, J.: Applying formal methods to a certifiably secure software system. IEEE Trans. Software Eng.\u00a034(1), 82\u201398 (2008)","journal-title":"IEEE Trans. Software Eng."},{"key":"31_CR14","unstructured":"Rushby, J.: Formal methods and their role in the certification of critical systems. Technical report, Safety and Reliability of Software Based Systems (Twelfth Annual CSR Workshop) (1995)"},{"key":"31_CR15","doi-asserted-by":"crossref","unstructured":"Jackson, M.: The problem frames approach to software engineering. In: APSEC, p. 14 (2007)","DOI":"10.1109\/ASPEC.2007.11"},{"key":"31_CR16","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999) ISBN 978-0262032704."},{"key":"31_CR17","unstructured":"Project RODIN: Rigorous open development environment for complex systems: RODIN Toolset and ProB. (2004), http:\/\/rodin-b-sharp.sourceforge.net\/"},{"issue":"2","key":"31_CR18","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol.\u00a011(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"31_CR19","unstructured":"Boston Scientific: Pacemaker system specification, Technical report, Boston Scientific (2007), http:\/\/www.cas.mcmaster.ca\/sqrl\/SQRLDocuments\/PACEMAKER.pdf"},{"key":"31_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-540-68237-0_14","volume-title":"FM 2008: Formal Methods","author":"H.D. Macedo","year":"2008","unstructured":"Macedo, H.D., Larsen, P.G., Fitzgerald, J.S.: Incremental development of a distributed real-time model of a cardiac pacing system using vdm. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 181\u2013197. Springer, Heidelberg (2008)"},{"key":"31_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/11955757_13","volume-title":"B 2007: Formal Specification and Development in B","author":"D. Cansell","year":"2006","unstructured":"Cansell, D., M\u00e9ry, D., Rehm, J.: Time constraint patterns for event b development. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol.\u00a04355, pp. 140\u2013154. Springer, Heidelberg (2006)"},{"key":"31_CR22","unstructured":"M\u00e9ry, D., Singh, N.K.: Functional behavior of a cardiac pacing system. International Journal of Discrete Event Control Systems 1(2) (in Press, 2010)"},{"key":"31_CR23","unstructured":"M\u00e9ry, D., Singh, N.K.: Technical Report on Formal Development of Two-Electrode Cardiac Pacing System (2010), http:\/\/hal.archives-ouvertes.fr\/inria-00465061\/en\/"},{"key":"31_CR24","volume-title":"Bioelectromagnetism","author":"J. Malmivuo","year":"1995","unstructured":"Malmivuo, J.: Bioelectromagnetism. Oxford University Press, Oxford (1995) ISBN 0-19-505823-2"},{"key":"31_CR25","doi-asserted-by":"publisher","DOI":"10.1002\/9780470695982","volume-title":"Simplified Interpretations of Pacemaker ECGs","author":"A. Hesselson","year":"2003","unstructured":"Hesselson, A.: Simplified Interpretations of Pacemaker ECGs. Blackwell Publishers, Malden (2003) ISBN 978-1-4051-0372-5"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification, and Validation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16561-0_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,5]],"date-time":"2019-06-05T21:08:01Z","timestamp":1559768881000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16561-0_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642165603","9783642165610"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16561-0_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}