{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T00:06:36Z","timestamp":1778198796849,"version":"3.51.4"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,10,7]],"date-time":"2014-10-07T00:00:00Z","timestamp":1412640000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002855","name":"Ministry of Science and Technology of the People's Republic of China","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002855","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Shanghai Knowledge Service Platform Project"},{"DOI":"10.13039\/501100004106","name":"East China Normal University","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004106","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Shanghai Minhang Talent Project"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2014,10,14]]},"abstract":"<jats:p>The cardiac pacemaker system, proposed as a problem topic in the Verification Grand Challenge, offers a range of difficulties to address for formal specification, development, and verification technologies. We focus on the sensing problem, the question of whether the heart has produced a spontaneous heartbeat or not. This question is plagued by uncertainties arising from the often unpredictable environment that a real pacemaker finds itself in. We develop a time domain tracking approach to this problem, as a complement to the usual frequency domain approach most frequently used. We develop our case study in the continuous ASM (Abstract State Machine) formalism, which is briefly summarised, through a series of refinement and retrenchment steps, each adding new levels of complexity to the model.<\/jats:p>","DOI":"10.1145\/2610375","type":"journal-article","created":{"date-parts":[[2014,10,14]],"date-time":"2014-10-14T12:29:11Z","timestamp":1413289751000},"page":"1-40","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["A Continuous ASM Modelling Approach to Pacemaker Sensing"],"prefix":"10.1145","volume":"24","author":[{"given":"Richard","family":"Banach","sequence":"first","affiliation":[{"name":"University of Manchester, Manchester, U.K."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, P.R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wen","family":"Su","sequence":"additional","affiliation":[{"name":"Shanghai University, Shanghai, P.R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaofeng","family":"Wu","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, P.R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,10,7]]},"reference":[{"key":"e_1_2_1_1_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Workshop on Theory of Hybrid Systems","author":"Alur R.","unstructured":"R. Alur , C. Courcoubetis , T. Henzinger , and P.-H. Ho . 1993. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems . In Proceedings of the Workshop on Theory of Hybrid Systems . Lecture Notes in Computer Science , vol. 736 , Springer , 209--229. R. Alur, C. Courcoubetis, T. Henzinger, and P.-H. Ho. 1993. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Proceedings of the Workshop on Theory of Hybrid Systems. Lecture Notes in Computer Science, vol. 736, Springer, 209--229."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1540-8159.1989.tb02696.x"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"R. Banach and C. Jeske. 2014. Retrenchment and refinement interworking: The tower theorems. Math. Struc. Comp. Sci To appear. http:\/\/www.cs.man.ac.uk\/&sim;banach\/some.pubs\/Retrench.Tower.pdf.  R. Banach and C. Jeske. 2014. Retrenchment and refinement interworking: The tower theorems. Math. Struc. Comp. Sci To appear. http:\/\/www.cs.man.ac.uk\/&sim;banach\/some.pubs\/Retrench.Tower.pdf.","DOI":"10.1017\/S0960129514000061"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.11.001"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.04.002"},{"key":"e_1_2_1_7_1","unstructured":"R. Banach H. Zhu W. Su and X. Wu. 2014. Moded and continuous ASM. Submitted.  R. Banach H. Zhu W. Su and X. Wu. 2014. Moded and continuous ASM. Submitted."},{"key":"e_1_2_1_8_1","volume-title":"Step: An Illustrated Guide","author":"Barold S.","year":"2010","unstructured":"S. Barold , R. Stroobandt , and A. Sinnaeve . 2010 . Cardiac Pacemakers and Resynchronization Step by Step: An Illustrated Guide . Wiley-Blackwell . S. Barold, R. Stroobandt, and A. Sinnaeve. 2010. Cardiac Pacemakers and Resynchronization Step by Step: An Illustrated Guide. Wiley-Blackwell."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12652-011-0062-2"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0012-7"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"E. B\u00f6rger and R. F. St\u00e4rk. 2003. Abstract State Machines. A Method for High Level System Design and Analysis. Springer.   E. B\u00f6rger and R. F. St\u00e4rk. 2003. Abstract State Machines. A Method for High Level System Design and Analysis. Springer.","DOI":"10.1007\/978-3-642-18216-7"},{"key":"e_1_2_1_12_1","unstructured":"Boston Scientific. 2007. PACEMAKER system specification. http:\/\/www.cas.mcmaster.ca\/sqrl\/_SQRL Documents\/PACEMAKER.pdf.  Boston Scientific. 2007. PACEMAKER system specification. http:\/\/www.cas.mcmaster.ca\/sqrl\/_SQRL Documents\/PACEMAKER.pdf."},{"key":"#cr-split#-e_1_2_1_13_1.1","doi-asserted-by":"crossref","unstructured":"L. Britnell R. Gorbachev R. Jalil etal 2012. Field-effect tunneling transistor based on vertical graphene heterostructures. Science. DOI: 10.1126\/science.1218461. 10.1126\/science.1218461","DOI":"10.1126\/science.1218461"},{"key":"#cr-split#-e_1_2_1_13_1.2","doi-asserted-by":"crossref","unstructured":"L. Britnell R. Gorbachev R. Jalil et al. 2012. Field-effect tunneling transistor based on vertical graphene heterostructures. Science. DOI: 10.1126\/science.1218461.","DOI":"10.1126\/science.1218461"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1561\/1000000001"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"E.\n      Clarke\n     and \n      P.\n      Zuliani\n  . \n  2011\n  . Statistical model checking for cyber-physical systems. In Proceedings of ATVA-11 Lecture Notes in Computer Science T. Bultan and P.-A. Hsiung (Eds.) vol. \n  6996 Springer 1--12.   E. Clarke and P. Zuliani. 2011. Statistical model checking for cyber-physical systems. In Proceedings of ATVA-11 Lecture Notes in Computer Science T. Bultan and P.-A. Hsiung (Eds.) vol. 6996 Springer 1--12.","DOI":"10.1007\/978-3-642-24372-1_1"},{"key":"e_1_2_1_16_1","volume-title":"Report: Cyber-Physical Systems","author":"CPS.","year":"2008","unstructured":"CPS. 2008 . Report: Cyber-Physical Systems . http:\/\/iccps2012.cse.wustl.edu\/_doc\/CPS_Summit_Report.pdf. CPS. 2008. Report: Cyber-Physical Systems. http:\/\/iccps2012.cse.wustl.edu\/_doc\/CPS_Summit_Report.pdf."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00602-9_10"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1161\/01.CIR.56.5.750"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11603009_13"},{"key":"e_1_2_1_20_1","unstructured":"K. Ellenbogen B. Wilkoff G. Kay and C-P. Lau. 2006. Clinical Cardiac Pacing Defibrillation and Resynchronization Therapy. Saunders.  K. Ellenbogen B. Wilkoff G. Kay and C-P. Lau. 2006. Clinical Cardiac Pacing Defibrillation and Resynchronization Therapy. Saunders."},{"key":"e_1_2_1_21_1","unstructured":"K. Ellenbogen and M. Wood. 2008. Cardiac Pacing and ICDs. Wiley-Blackwell. 5th ed.  K. Ellenbogen and M. Wood. 2008. Cardiac Pacing and ICDs. Wiley-Blackwell. 5th ed."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0002-8703(77)80078-1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1038\/nmat1849"},{"key":"e_1_2_1_24_1","volume-title":"Catastrophe Theory for Scientists and Engineers","author":"Gilmore R.","unstructured":"R. Gilmore . 1981. Catastrophe Theory for Scientists and Engineers . Dover . R. Gilmore. 1981. Catastrophe Theory for Scientists and Engineers. Dover."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-007-0029-9"},{"key":"e_1_2_1_26_1","first-page":"28","article-title":"The pacemaker challenge","volume":"10","author":"Goldman B.","year":"1974","unstructured":"B. Goldman , E. Noble , J. Heller , and D. Covvey . 1974 . The pacemaker challenge . Can. Med. Ass. J. 10 , 28 -- 31 . B. Goldman, E. Noble, J. Heller, and D. Covvey. 1974. The pacemaker challenge. Can. Med. Ass. J. 10, 28--31.","journal-title":"Can. Med. Ass. J."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_44"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987100.1987114"},{"key":"e_1_2_1_29_1","volume-title":"A Classical Mind, Essays in Honour of C","author":"He J.","unstructured":"J. He . 1994. From CSP to hybrid systems . In A Classical Mind, Essays in Honour of C .A.R. Hoare, Roscoe (Ed.), Prentice-Hall , 171--189. J. He. 1994. From CSP to hybrid systems. In A Classical Mind, Essays in Honour of C.A.R. Hoare, Roscoe (Ed.), Prentice-Hall, 171--189."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788803"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.145"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1540-8159.1979.tb05171.x"},{"key":"e_1_2_1_33_1","unstructured":"KIV. Karlsruhe Interactive Verifier. http:\/\/www.informatik.uni-augsburg.de\/lehrstuehle\/swt\/se\/kiv\/.  KIV. Karlsruhe Interactive Verifier. http:\/\/www.informatik.uni-augsburg.de\/lehrstuehle\/swt\/se\/kiv\/."},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"F. Kusumoto and N. Goldschlager. 2007. Cardiac Pacing for the Clinician. Springer.  F. Kusumoto and N. Goldschlager. 2007. Cardiac Pacing for the Clinician. Springer.","DOI":"10.1007\/978-0-387-72763-9"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the NSF Workshop on Cyber-Physical Systems: Research Motivation, Techniques and Roadmap.","author":"Lee E.","year":"2006","unstructured":"E. Lee . 2006 . Cyber-physical systems\u2014Are computing foundations adequate . In Proceedings of the NSF Workshop on Cyber-Physical Systems: Research Motivation, Techniques and Roadmap. E. Lee. 2006. Cyber-physical systems\u2014Are computing foundations adequate. In Proceedings of the NSF Workshop on Cyber-Physical Systems: Research Motivation, Techniques and Roadmap."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2008.25"},{"key":"e_1_2_1_37_1","unstructured":"E. Lee and S. Sesha. 2013. Introduction to Embedded Systems - A Cyber-Physical Systems Approach. Lulu.com.  E. Lee and S. Sesha. 2013. Introduction to Embedded Systems - A Cyber-Physical Systems Approach. Lulu.com."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_14"},{"key":"e_1_2_1_39_1","volume-title":"Tech. Rep. INRIA-00419973:2. LORIA, Universit\u00e9 Henri Poincar\u00e9 - Nancy I","author":"M\u00e9ry D.","year":"2009","unstructured":"D. M\u00e9ry and N. Singh . 2009 . Pacemaker's functional behaviors in event-B. Tech. Rep. INRIA-00419973:2. LORIA, Universit\u00e9 Henri Poincar\u00e9 - Nancy I . http:\/\/hal.inria.fr\/inria-00419973\/PDF\/Pacemaker.pdf. D. M\u00e9ry and N. Singh. 2009. Pacemaker's functional behaviors in event-B. Tech. Rep. INRIA-00419973:2. LORIA, Universit\u00e9 Henri Poincar\u00e9 - Nancy I. http:\/\/hal.inria.fr\/inria-00419973\/PDF\/Pacemaker.pdf."},{"key":"e_1_2_1_40_1","volume-title":"Tech. Rep. INRIA-00465061:2. LORIA, Universit\u00e9 Henri Poincar\u00e9 - Nancy I","author":"M\u00e9ry D.","year":"2010","unstructured":"D. M\u00e9ry and N. Singh . 2010 . Technical report on formal development of two-electrode cardiac pacing system. Tech. Rep. INRIA-00465061:2. LORIA, Universit\u00e9 Henri Poincar\u00e9 - Nancy I . http:\/\/hal.inria.fr\/inria-00465061\/PDF\/Report_2electrode.pdf. D. M\u00e9ry and N. Singh. 2010. Technical report on formal development of two-electrode cardiac pacing system. Tech. Rep. INRIA-00465061:2. LORIA, Universit\u00e9 Henri Poincar\u00e9 - Nancy I. http:\/\/hal.inria.fr\/inria-00465061\/PDF\/Report_2electrode.pdf."},{"key":"e_1_2_1_41_1","volume-title":"Tech. Rep. LORIA, Universit\u00e9 Henri Poincar\u00e9 - Nancy I","author":"M\u00e9ry D.","year":"2011","unstructured":"D. M\u00e9ry and N. Singh . 2011 . Functional behavior of a cardiac pacing system. Tech. Rep. LORIA, Universit\u00e9 Henri Poincar\u00e9 - Nancy I . http:\/\/www.loria.fr\/&sim;singhnne\/Home_files\/downloads\/ijdecs2010.pdf, Int. J. Disc. Event Control Syst. D. M\u00e9ry and N. Singh. 2011. Functional behavior of a cardiac pacing system. Tech. Rep. LORIA, Universit\u00e9 Henri Poincar\u00e9 - Nancy I. http:\/\/www.loria.fr\/&sim;singhnne\/Home_files\/downloads\/ijdecs2010.pdf, Int. J. Disc. Event Control Syst."},{"key":"e_1_2_1_42_1","unstructured":"National Science and Technology Council. 2011. Trustworthy cyberspace: Strategic plan for the federal cybersecurity research and development program. http:\/\/www.whitehouse.gov\/sites\/default\/files\/microsites\/ostp\/fed_cybersecurity_rd_strategic_plan_2011.pdf.  National Science and Technology Council. 2011. Trustworthy cyberspace: Strategic plan for the federal cybersecurity research and development program. http:\/\/www.whitehouse.gov\/sites\/default\/files\/microsites\/ostp\/fed_cybersecurity_rd_strategic_plan_2011.pdf."},{"key":"e_1_2_1_43_1","volume-title":"Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics","author":"Platzer A.","unstructured":"A. Platzer . 2010. Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics . Springer . A. Platzer. 2010. Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/2044973.2044989"},{"key":"e_1_2_1_45_1","unstructured":"RET. Retrenchment Homepage. http:\/\/www.cs.man.ac.uk\/retrenchment.  RET. Retrenchment Homepage. http:\/\/www.cs.man.ac.uk\/retrenchment."},{"key":"e_1_2_1_46_1","volume-title":"An Introduction to Catastrophe Theory","author":"Saunders P.","unstructured":"P. Saunders . 1980. An Introduction to Catastrophe Theory . Cambridge University Press . P. Saunders. 1980. An Introduction to Catastrophe Theory. Cambridge University Press."},{"key":"e_1_2_1_47_1","first-page":"952","article-title":"Verification of ASM refinements using generalized forward simulation","volume":"7","author":"Schellhorn G.","year":"2001","unstructured":"G. Schellhorn . 2001 . Verification of ASM refinements using generalized forward simulation . J. Univ. Comput. Sci. 7 , 952 -- 979 . G. Schellhorn. 2001. Verification of ASM refinements using generalized forward simulation. J. Univ. Comput. Sci. 7, 952--979.","journal-title":"J. Univ. Comput. Sci."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.11.013"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.eupc.2004.12.004"},{"key":"e_1_2_1_50_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of HSCC-02","author":"Stauner T.","unstructured":"T. Stauner . 2002. Discrete-time refinement of hybrid automata . In Proceedings of HSCC-02 . Lecture Notes in Computer Science , vol. 2289 , Springer , 144--161. T. Stauner. 2002. Discrete-time refinement of hybrid automata. In Proceedings of HSCC-02. Lecture Notes in Computer Science, vol. 2289, Springer, 144--161."},{"key":"e_1_2_1_51_1","volume-title":"Proc. UIC-10","volume":"6406","author":"Stehr M.","unstructured":"M. Stehr , M. Kim , and C. Talcott . 2010. Toward distributed declarative control of networked cyber-physical systems . In Proc. UIC-10 . Lecture Notes in Computer Science , vol. 6406 . Z. Yu, R. Liscano, G. Chen, D. Zhang, and X. Zhou (Eds.), Springer, 397--413. M. Stehr, M. Kim, and C. Talcott. 2010. Toward distributed declarative control of networked cyber-physical systems. In Proc. UIC-10. Lecture Notes in Computer Science, vol. 6406. Z. Yu, R. Liscano, G. Chen, D. Zhang, and X. Zhou (Eds.), Springer, 397--413."},{"key":"e_1_2_1_52_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of FM-11","author":"Sztipanovits J.","unstructured":"J. Sztipanovits . 2011. Model integration and cyber physical systems: A semantics perspective . In Proceedings of FM-11 . Lecture Notes in Computer Science , vol. 6664 , M. Butler and W. Schulte (Eds.). Springer , p. 1, http:\/\/sites.lero.ie\/download.aspx&quest;f=Sztipanovits-Keynote.pdf. Invited talk, FM 2011, Limerick, Ireland. J. Sztipanovits. 2011. Model integration and cyber physical systems: A semantics perspective. In Proceedings of FM-11. Lecture Notes in Computer Science, vol. 6664, M. Butler and W. Schulte (Eds.). Springer, p. 1, http:\/\/sites.lero.ie\/download.aspx&quest;f=Sztipanovits-Keynote.pdf. Invited talk, FM 2011, Limerick, Ireland."},{"key":"e_1_2_1_53_1","volume-title":"Verification and Control of Hybrid Systems: A Symbolic Approach","author":"Tabuada P.","unstructured":"P. Tabuada . 2009. Verification and Control of Hybrid Systems: A Symbolic Approach . Springer . P. Tabuada. 2009. Verification and Control of Hybrid Systems: A Symbolic Approach. Springer."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13174-010-0004-9"},{"key":"e_1_2_1_55_1","volume-title":"Open dynamical systems: Their aims and their origins. Ruberti Lecture","author":"Willems J.","year":"2007","unstructured":"J. Willems . 2007. Open dynamical systems: Their aims and their origins. Ruberti Lecture , Rome . http:\/\/homes. esat.kuleuven.be\/&sim;jwillems\/Lectures\/ 2007 \/Rubertilecture.pdf. J. Willems. 2007. Open dynamical systems: Their aims and their origins. Ruberti Lecture, Rome. http:\/\/homes. esat.kuleuven.be\/&sim;jwillems\/Lectures\/2007\/Rubertilecture.pdf."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1085\/jgp.16.3.423"},{"key":"e_1_2_1_57_1","volume-title":"Ann Arbor: University of Michigan Press. (Reprinted in: Lepeschkin and Johnston (eds.), Selected Papers of Frank N. Wilson.","author":"Wilson F.","year":"1933","unstructured":"F. Wilson , A. Macleod , and P. Barker . 1933 b. The Distribution of the Currents of Action and of Injury Displayed by Heart Muscle and Other Excitable Tissues. University of Michigan Studies . Scientific Series, vol. 10 , Ann Arbor: University of Michigan Press. (Reprinted in: Lepeschkin and Johnston (eds.), Selected Papers of Frank N. Wilson. Ann Arbor, J.W. Edwards (1954).) F. Wilson, A. Macleod, and P. Barker. 1933b. The Distribution of the Currents of Action and of Injury Displayed by Heart Muscle and Other Excitable Tissues. University of Michigan Studies. Scientific Series, vol. 10, Ann Arbor: University of Michigan Press. (Reprinted in: Lepeschkin and Johnston (eds.), Selected Papers of Frank N. Wilson. Ann Arbor, J.W. Edwards (1954).)"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.340"},{"key":"e_1_2_1_59_1","first-page":"661","article-title":"The verification grand challenge","volume":"13","author":"Woodcock J.","year":"2007","unstructured":"J. Woodcock and R. Banach . 2007 . The verification grand challenge . JUCS 13 , 661 -- 668 . J. Woodcock and R. Banach. 2007. The verification grand challenge. JUCS 13, 661--668.","journal-title":"JUCS"},{"key":"e_1_2_1_60_1","volume-title":"Proceedings of ICHIT-11","volume":"206","author":"Zhang L.","unstructured":"L. Zhang and J. He . 2011. A formal framework for aspect-oriented specification of cyber physical systems . In Proceedings of ICHIT-11 . Communications in Computer and Information Science , vol. 206 , G. Lee, D. Howard, and V. Slezak (Eds.), Springer, 391--398. L. Zhang and J. He. 2011. A formal framework for aspect-oriented specification of cyber physical systems. In Proceedings of ICHIT-11. Communications in Computer and Information Science, vol. 206, G. Lee, D. Howard, and V. Slezak (Eds.), Springer, 391--398."},{"key":"e_1_2_1_61_1","volume-title":"Proceedings ICAR-11","volume":"122","author":"Z\u00fchlke L.","unstructured":"L. Z\u00fchlke and L. Ollinger . 2012. Agile automaton sysytems based on cyber-physical systems and service oriented architectures . In Proceedings ICAR-11 . Lecture Notes in Electrical Engineering , vol. 122 , G. Lee (Ed.), Springer, 567--574. L. Z\u00fchlke and L. Ollinger. 2012. Agile automaton sysytems based on cyber-physical systems and service oriented architectures. In Proceedings ICAR-11. Lecture Notes in Electrical Engineering, vol. 122, G. Lee (Ed.), Springer, 567--574."}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2610375","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2610375","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:55:53Z","timestamp":1750229753000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2610375"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10,7]]},"references-count":62,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,10,14]]}},"alternative-id":["10.1145\/2610375"],"URL":"https:\/\/doi.org\/10.1145\/2610375","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,10,7]]},"assertion":[{"value":"2013-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}