{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:51:42Z","timestamp":1750308702776,"version":"3.41.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2013,1]]},"abstract":"<jats:p>Formal methods have emerged as an alternative approach to ensuring quality and correctness of highly critical systems, overcoming limitations of traditional validation techniques such as simulation and testing. We propose a refinement-based methodology for complex medical systems design, which possesses all the required key features. A refinement-based combined approach of formal verification, model validation using a model-checker and refinement chart is proposed in this methodology for designing a high-confidence medical device. Furthermore, we show the effectiveness of this methodology for the design of a cardiac pacemaker system.<\/jats:p>","DOI":"10.1145\/2406336.2406351","type":"journal-article","created":{"date-parts":[[2013,1,29]],"date-time":"2013-01-29T16:20:55Z","timestamp":1359476455000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"title":["Formal Specification of Medical Systems by Proof-Based Refinement"],"prefix":"10.1145","volume":"12","author":[{"given":"Dominique","family":"M\u00e9ry","sequence":"first","affiliation":[{"name":"Universit\u00e9 Henri Poincar\u00e9 Nancy 1"}]},{"given":"Neeraj Kumar","family":"Singh","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Henri Poincar\u00e9 Nancy 1"}]}],"member":"320","published-online":{"date-parts":[[2013,1]]},"reference":[{"volume-title":"Modeling in Event-B: System and Software Engineering","author":"Abrial J.-R.","key":"e_1_2_1_1_1","unstructured":"Abrial , J.-R. 2010. Modeling in Event-B: System and Software Engineering . Cambridge University Press . Abrial, J.-R. 2010. Modeling in Event-B: System and Software Engineering. Cambridge University Press."},{"key":"e_1_2_1_2_1","volume-title":"Eds","author":"Abrial J.-R.","year":"1996","unstructured":"Abrial , J.-R. , B\u00f6rger , E. , and Langmaack , H . Eds . 1996 . Formal Methods for Industrial Applications, Specifying and Programming the Steam Boiler Control. Lecture Notes in Computer Science Series, vol. 1165 , Springer . Abrial, J.-R., B\u00f6rger, E., and Langmaack, H. Eds. 1996. Formal Methods for Industrial Applications, Specifying and Programming the Steam Boiler Control. Lecture Notes in Computer Science Series, vol. 1165, Springer."},{"volume-title":"Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems","author":"Alur R.","key":"e_1_2_1_3_1","unstructured":"Alur , R. 2007. Verification and integration of real-time control software . In Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems , S. Ramesh and P. Sampath Eds., Springer , 47--49. Alur, R. 2007. Verification and integration of real-time control software. In Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems, S. Ramesh and P. Sampath Eds., Springer, 47--49."},{"key":"e_1_2_1_4_1","volume-title":"-P","author":"Baier C.","year":"2008","unstructured":"Baier , C. and Katoen , J . -P . 2008 . Principles of Model Checking. MIT Press . Baier, C. and Katoen, J.-P. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Barold S. S. Stroobandt R. X. and Sinnaeve A. F. 2004. Cardiac Pacemakers Step by Step. Futura Publishing.  Barold S. S. Stroobandt R. X. and Sinnaeve A. F. 2004. Cardiac Pacemakers Step by Step . Futura Publishing.","DOI":"10.1002\/9780470750728"},{"key":"e_1_2_1_6_1","unstructured":"Bj\u00f8rner D. 2006. Software Engineering: Vol 1 Abstraction and Modelling - Vol 2 Specification of Systems and Languages - Vol 3 Domains Requirements and Software Design. Texts in Theoretical Computer Science. An EATCS Series.  Bj\u00f8rner D. 2006. Software Engineering: Vol 1 Abstraction and Modelling - Vol 2 Specification of Systems and Languages - Vol 3 Domains Requirements and Software Design . Texts in Theoretical Computer Science. An EATCS Series."},{"key":"e_1_2_1_7_1","volume-title":"Eds","author":"Bj\u00f8rner D.","year":"2007","unstructured":"Bj\u00f8rner , D. and Henson , M. C . Eds . 2007 . Logics of Specification Languages. EATCS Textbook in Computer Science. Springer . Bj\u00f8rner, D. and Henson, M. C. Eds. 2007. Logics of Specification Languages. EATCS Textbook in Computer Science. Springer."},{"key":"e_1_2_1_8_1","unstructured":"Boston Scientific. 2007. Pacemaker system specification. Tech. rep.  Boston Scientific. 2007. Pacemaker system specification. Tech. rep."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1049\/sej.1993.0025"},{"volume-title":"An introduction to requirements capture using PVS: Specification of a simple autopilot. NASA Tech. Memo. 110255","author":"Butler R. W.","key":"e_1_2_1_10_1","unstructured":"Butler , R. W. 1996. An introduction to requirements capture using PVS: Specification of a simple autopilot. NASA Tech. Memo. 110255 , NASA Langley Research Center , Hampton, VA . Butler, R. W. 1996. An introduction to requirements capture using PVS: Specification of a simple autopilot. NASA Tech. Memo. 110255, NASA Langley Research Center, Hampton, VA."},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Cansell D. and M\u00e9ry D. 2007. The Event-B Modeling Method: Concepts and Case Studies. In Logics of Specification Languages D. Bj\u00f8rner and M. C. Henson Eds. Springer 33--140.  Cansell D. and M\u00e9ry D. 2007. The Event-B Modeling Method: Concepts and Case Studies. In Logics of Specification Languages D. Bj\u00f8rner and M. C. Henson Eds. Springer 33--140.","DOI":"10.1007\/978-3-540-74107-7_3"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/348019.348093"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1177\/003759703039952"},{"key":"e_1_2_1_14_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. 1999. Model Checking. MIT Press.   Clarke E. M. Grumberg O. and Peled D. 1999. Model Checking . MIT Press."},{"key":"e_1_2_1_15_1","unstructured":"ClearSy. Atelier B. http:\/\/www.clearsy.com.  ClearSy. Atelier B. http:\/\/www.clearsy.com."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_31"},{"key":"e_1_2_1_17_1","unstructured":"EB2ALL. 2011. Automatic code generation from Event-B to many Programming Languages. http:\/\/eb2all.loria.fr\/.  EB2ALL. 2011. Automatic code generation from Event-B to many Programming Languages. http:\/\/eb2all.loria.fr\/."},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Ellenbogen K. A. and Wood M. A. 2005. Cardiac Pacing and ICDs 4th Ed. Blackwell.  Ellenbogen K. A. and Wood M. A. 2005. Cardiac Pacing and ICDs 4th Ed. Blackwell.","DOI":"10.1002\/9780470750674"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1161\/CIRCUALTIONAHA.108.189741"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 2nd International Workshop on Responsive Computer Systems. Springer, 287--300","author":"Fohler G.","year":"1992","unstructured":"Fohler , G. 1992 . Realizing changes of operational modes with a pre run-time scheduled hard real-time system . In Proceedings of the 2nd International Workshop on Responsive Computer Systems. Springer, 287--300 . Fohler, G. 1992. Realizing changes of operational modes with a pre run-time scheduled hard real-time system. In Proceedings of the 2nd International Workshop on Responsive Computer Systems. Springer, 287--300."},{"key":"e_1_2_1_21_1","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software design Patterns","author":"Gamma E.","year":"1994","unstructured":"Gamma , E. , Helm , R. , Johnson , R. , Vlissides , R. , and Gamma , P . 1994 . Design Patterns: Elements of Reusable Object-Oriented Software design Patterns . Addison-Wesley Professional Computing . Gamma, E., Helm, R., Johnson, R., Vlissides, R., and Gamma, P. 1994. Design Patterns: Elements of Reusable Object-Oriented Software design Patterns. Addison-Wesley Professional Computing."},{"key":"e_1_2_1_22_1","first-page":"28","article-title":"The pacemaker challenge","volume":"110","author":"Goldman B. S.","year":"1974","unstructured":"Goldman , B. S. , Noble , E. J. , Heller , J. G. , and Covvey , D. 1974 . The pacemaker challenge . Can. Med. Assoc. J. 110 , 1, 28 -- 31 . Goldman, B. S., Noble, E. J., Heller, J. G., and Covvey, D. 1974. The pacemaker challenge. Can. Med. Assoc. J. 110, 1, 28--31.","journal-title":"Can. Med. Assoc. J."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_44"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"volume-title":"Proceedings of the 10th International Conference on Model Checking Software. Springer, 235--239","author":"Henzinger T. A.","key":"e_1_2_1_25_1","unstructured":"Henzinger , T. A. , Jhala , R. , Majumdar , R. , and Sutre , G . 2003. Software verification with BLAST. In Software verification with BLAST . In Proceedings of the 10th International Conference on Model Checking Software. Springer, 235--239 . Henzinger, T. A., Jhala, R., Majumdar, R., and Sutre, G. 2003. Software verification with BLAST. In Software verification with BLAST. In Proceedings of the 10th International Conference on Model Checking Software. Springer, 235--239."},{"volume-title":"Simplified Interpretations of Pacemaker ECGs","author":"Hesselson A.","key":"e_1_2_1_26_1","unstructured":"Hesselson , A. 2003. Simplified Interpretations of Pacemaker ECGs . Blackwell Publishers . Hesselson, A. 2003. Simplified Interpretations of Pacemaker ECGs. Blackwell Publishers."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592439"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/602382.602403"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.368134"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.113"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-003-0137-2"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1080\/105294100277723"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1173706.1173740"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.127"},{"volume-title":"Cardiac Pacemakers and Defibrillators","author":"Love C. J.","key":"e_1_2_1_36_1","unstructured":"Love , C. J. 2006. Cardiac Pacemakers and Defibrillators . Landes Bioscience Publishers . Love, C. J. 2006. Cardiac Pacemakers and Defibrillators. Landes Bioscience Publishers."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_14"},{"key":"e_1_2_1_38_1","first-page":"196","article-title":"Validation of medical modeling & simulation training devices and systems","volume":"94","author":"Magee J. H.","year":"2003","unstructured":"Magee , J. H. 2003 . Validation of medical modeling & simulation training devices and systems . Stud. Health Technol Inf. 94 , 196 -- 198 . Magee, J. H. 2003. Validation of medical modeling & simulation training devices and systems. Stud. Health Technol Inf. 94, 196--8.","journal-title":"Stud. Health Technol Inf."},{"key":"e_1_2_1_39_1","unstructured":"Malmivuo J. 1995. Bioelectromagnetism. Oxford University Press. ISBN 0-19-505823-2.  Malmivuo J. 1995. Bioelectromagnetism . Oxford University Press. ISBN 0-19-505823-2."},{"key":"e_1_2_1_40_1","unstructured":"M\u00e9ry D. and Singh N. K. 2009. Pacemaker\u2019s functional behaviors in Event-B. Res. rep. http:\/\/hal.inria.fr\/inria-00419973\/en\/.  M\u00e9ry D. and Singh N. K. 2009. Pacemaker\u2019s functional behaviors in Event-B. Res. rep. http:\/\/hal.inria.fr\/inria-00419973\/en\/."},{"volume-title":"Proceedings of the International Conference on Software Engineering and Formal Methods.","author":"M\u00e9ry D.","key":"e_1_2_1_41_1","unstructured":"M\u00e9ry , D. and Singh , N. K . 2010a. EB2C: A tool for Event-B to C conversion support . In Proceedings of the International Conference on Software Engineering and Formal Methods. M\u00e9ry, D. and Singh, N. K. 2010a. EB2C: A tool for Event-B to C conversion support. In Proceedings of the International Conference on Software Engineering and Formal Methods."},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"M\u00e9ry D. and Singh N. K. 2010b. Real-time animation for formal specification. In Complex Systems Design & Management M. Aiguier F. Bretaudeau and D. Krob Eds. Springer 49--60.  M\u00e9ry D. and Singh N. K. 2010b. Real-time animation for formal specification. In Complex Systems Design & Management M. Aiguier F. Bretaudeau and D. Krob Eds. Springer 49--60.","DOI":"10.1007\/978-3-642-15654-0_3"},{"key":"e_1_2_1_43_1","unstructured":"M\u00e9ry D. and Singh N. K. 2010. Formal development of two-electrode cardiac pacing system. Technical Rep. http:\/\/hal.archives-ouvertes.fr\/inria-00465061\/en\/.  M\u00e9ry D. and Singh N. K. 2010. Formal development of two-electrode cardiac pacing system. Technical Rep. http:\/\/hal.archives-ouvertes.fr\/inria-00465061\/en\/."},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"M\u00e9ry D.\n     and \n      Singh N. K\n  . \n  2010\n  . Trustable formal specification for software certification. In Proceedings of the 4th International Symposium on Leveraging Applications T. Margaria and B. Steffen Eds. Lecture Notes in Computer Science Series vol. \n  6416\n  . \n  Springer 312--326.   M\u00e9ry D. and Singh N. K. 2010. Trustable formal specification for software certification. In Proceedings of the 4th International Symposium on Leveraging Applications T. Margaria and B. Steffen Eds. Lecture Notes in Computer Science Series vol. 6416. Springer 312--326.","DOI":"10.1007\/978-3-642-16561-0_31"},{"key":"e_1_2_1_45_1","first-page":"129","article-title":"Functional behavior of a cardiac pacing system","volume":"1","author":"M\u00e9ry D.","year":"2011","unstructured":"M\u00e9ry , D. and Singh , N. K. 2011 . Functional behavior of a cardiac pacing system . International J. Discrete Event Control Syst. 1 , 2, 129 -- 149 . M\u00e9ry, D. and Singh, N. K. 2011. Functional behavior of a cardiac pacing system. International J. Discrete Event Control Syst. 1, 2, 129--149.","journal-title":"International J. Discrete Event Control Syst."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/298595.298856"},{"volume-title":"High-Confidence Medical Devices: Cyber-Physical Systems for 21st Century Health Care","author":"NITRD.","key":"e_1_2_1_47_1","unstructured":"NITRD. High-Confidence Medical Devices: Cyber-Physical Systems for 21st Century Health Care . http:\/\/www.nitrd.gov\/About\/MedDevice-FINAL1-web.pdf. NITRD. High-Confidence Medical Devices: Cyber-Physical Systems for 21st Century Health Care. http:\/\/www.nitrd.gov\/About\/MedDevice-FINAL1-web.pdf."},{"key":"e_1_2_1_48_1","unstructured":"ProB. The ProB animator and model checker for the B method. http:\/\/www.stups.uni-duesseldorf.de\/ProB\/overview.php\/.  ProB. The ProB animator and model checker for the B method. http:\/\/www.stups.uni-duesseldorf.de\/ProB\/overview.php\/."},{"key":"e_1_2_1_49_1","unstructured":"Project RODIN. 2004. Rigorous open development environment for complex systems. http:\/\/rodin-bsharp.sourceforge.net\/.2004--2007.  Project RODIN. 2004. Rigorous open development environment for complex systems. http:\/\/rodin-bsharp.sourceforge.net\/.2004--2007."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:TIME.0000016129.97430.c6"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-009-0130-5"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69149-5_20"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/647705.734655"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.340"},{"key":"e_1_2_1_55_1","first-page":"661","article-title":"The verification grand challenge","volume":"13","author":"Woodcock J.","year":"2007","unstructured":"Woodcock , J. and Banach , R. 2007 . The verification grand challenge . J. Univ. Comput. Sci. 13 , 5, 661 -- 668 . Woodcock, J. and Banach, R. 2007. The verification grand challenge. J. Univ. Comput. Sci. 13, 5, 661--668.","journal-title":"J. Univ. Comput. Sci."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2406336.2406351","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2406336.2406351","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:13:55Z","timestamp":1750277635000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2406336.2406351"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1]]},"references-count":55,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,1]]}},"alternative-id":["10.1145\/2406336.2406351"],"URL":"https:\/\/doi.org\/10.1145\/2406336.2406351","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2013,1]]},"assertion":[{"value":"2010-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}