{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:40:42Z","timestamp":1725493242690},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540766483"},{"type":"electronic","value":"9783540766506"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-76650-6_7","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T03:12:49Z","timestamp":1193368369000},"page":"96-115","source":"Crossref","is-referenced-by-count":3,"title":["Machine-Assisted Proof Support for Validation Beyond Simulink"],"prefix":"10.1007","author":[{"given":"Chunqing","family":"Chen","sequence":"first","affiliation":[]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Butler, R.W.: Formalization of the integral calculus in the pvs theorem prover. Technical report, NASA Langley Research Center, Hampton, Virginia (October 2004)"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Cerone, A.: Axiomatisation of an interval calculus for theorem proving. Electr. Notes Theor. Comput. Sci.\u00a042 (2001)","DOI":"10.1016\/S1571-0661(04)80879-X"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","first-page":"167","volume-title":"Computer Aided Verification","author":"G. Chakravorty","year":"2006","unstructured":"Chakravorty, G., Pandya, P.K.: Digitizing interval duration logic. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 167\u2013179. Springer, Heidelberg (2006)"},{"key":"7_CR4","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C.-L. Chang","year":"1997","unstructured":"Chang, C.-L., Lee, R.C., Lee, R.C.-T.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, Inc., London (1997)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1007\/11901433_5","volume-title":"ICFEM 2006","author":"C. Chen","year":"2006","unstructured":"Chen, C., Dong, J.S.: Applying Timed Interval Calculus to Simulink Diagrams. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 74\u201393. Springer, Heidelberg (2006)"},{"issue":"5","key":"7_CR6","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. on Prog. Lang. and Sys.s\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. on Prog. Lang. and Sys.s"},{"key":"7_CR7","series-title":"Lecture Notes in Artificial Intelligence","first-page":"95","volume-title":"AI 2006","author":"J.E. Dawson","year":"2006","unstructured":"Dawson, J.E., Gor\u00e9, R.: Machine-checking the timed interval calculus. In: Sattar, A., Kang, B.-H. (eds.) AI 2006. LNCS (LNAI), vol.\u00a04304, pp. 95\u2013106. Springer, Heidelberg (2006)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/BFb0105402","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Dutertre","year":"1996","unstructured":"Dutertre, B.: Elements of mathematical analysis in PVS. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 141\u2013156. Springer, Heidelberg (1996)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Fidge, C.J., Hayes, I.J., Mahony, B.P.: Defining differentiation and integration in Z. In: ICFEM 1998, pp. 64\u201373 (1998)","DOI":"10.1109\/ICFEM.1998.730571"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/BFb0054291","volume-title":"Mathematics of Program Construction","author":"C.J. Fidge","year":"1998","unstructured":"Fidge, C.J., Hayes, I.J., Martin, A.P., Wabenhorst, A.: A Set-Theoretic Model for Real-Time Specification and Reasoning. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol.\u00a01422, pp. 188\u2013206. Springer, Heidelberg (1998)"},{"key":"7_CR11","volume-title":"Introduction to HOL: A theorem proving environment for higher order logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","first-page":"73","volume-title":"TPHOLs 1998","author":"A.M. Gravell","year":"1998","unstructured":"Gravell, A.M., Pratten, C.H.: Embedding a formal notation: Experiences of automating the embedding of z in the higher order logics of pvs and hol. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 73\u201384. Springer, Heidelberg (1998)"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Gupta, S., Krogh, B.H., Rutenbar, R.A.: Towards formal verification of analog designs. In: ICCAD 2004, pp. 210\u2013217 (2004)","DOI":"10.1109\/ICCAD.2004.1382573"},{"key":"7_CR14","unstructured":"Heilmann, S.T.: Proof Support for Duration Calculus. PhD thesis, Department of Information Technology, Technical University of Denmark (1999)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11813040_1","volume-title":"FM 2006","author":"T.A. Henzinger","year":"2006","unstructured":"Henzinger, T.A., Sifakis, J.: The embedded systems design challenge. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 1\u201315. Springer, Heidelberg (2006)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","first-page":"137","volume-title":"Software Security - Theories and Systems","author":"M. Jersak","year":"2004","unstructured":"Jersak, M., Cai, Y., Ziegenbein, D., Ernst, R.: A transformational approach to constraint relaxation of a time-driven simulation model. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol.\u00a03233, pp. 137\u2013142. Springer, Heidelberg (2004)"},{"issue":"9","key":"7_CR17","doi-asserted-by":"publisher","first-page":"817","DOI":"10.1109\/32.159841","volume":"18","author":"B.P. Mahony","year":"1992","unstructured":"Mahony, B.P., Hayes, I.J.: A case-study in timed refinement: A mine pump. IEEE Transactions on Software Engineering\u00a018(9), 817\u2013826 (1992)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR18","unstructured":"The MathWorks. Simulink - Simulation and Model-based Design - Using Simulink Version 6 (2004)"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1007\/11901433_33","volume-title":"Formal Methods and Software Engineering","author":"B. Meenakshi","year":"2006","unstructured":"Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for translating simulink models into input language of a model checker. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 606\u2013620. Springer, Heidelberg (2006)"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Moszkowski, B.C.: A complete axiomatization of interval temporal logic with infinite time. In: LICS 2000, pp. 241\u2013252 (2000)","DOI":"10.1109\/LICS.2000.855773"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Mu\u00f1oz, C., Carre\u00f1o, V., Dowek, G.: Formal analysis of the operational concept for the Small Aircraft Transportation System. In: REFT 2006, pp. 306\u2013325 (2006)","DOI":"10.1007\/11916246_16"},{"issue":"3","key":"7_CR22","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/s10009-002-0084-3","volume":"4","author":"C. Mu\u00f1oz","year":"2003","unstructured":"Mu\u00f1oz, C., Carre\u00f1o, V., Dowek, G., Butler, R.W.: Formal verification of conflict detection algorithms. I. Jour. on Soft. Tools for Tech. Trans.\u00a04(3), 371\u2013380 (2003)","journal-title":"I. Jour. on Soft. Tools for Tech. Trans."},{"key":"7_CR23","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification system. In: Kapur, D. (ed.) CADE-11. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1007\/3-540-60609-2_11","volume-title":"SOFSEM 1995","author":"H. Rischel","year":"1995","unstructured":"Rischel, H., Cu\u00e9llar, J., M\u00f8k, S., Ravn, A.P., Wildgruber, I.: Development of safety-critical real-time systems. In: Bartosek, M., Staudek, J., Wiedermann, J. (eds.) SOFSEM 1995. LNCS, vol.\u00a01012, pp. 206\u2013235. Springer, Heidelberg (1995)"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"660","DOI":"10.1007\/3-540-58468-4_189","volume-title":"FTRTFT 1994","author":"J.U. Skakkeb\u00e6k","year":"1994","unstructured":"Skakkeb\u00e6k, J.U., Shankar, N.: Towards a duration calculus proof assistant in pvs. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994. LNCS, vol.\u00a0863, pp. 660\u2013679. Springer, Heidelberg (1994)"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1007\/3-540-63533-5_30","volume-title":"FME 1997","author":"D.W.J. Stringer-Calvert","year":"1997","unstructured":"Stringer-Calvert, D.W.J., Stepney, S., Wand, I.: Using pvs to prove a z refinement: A case study. In: Jones, C.B. (ed.) FME 1997. LNCS, vol.\u00a01313, pp. 573\u2013588. Springer, Heidelberg (1997)"},{"issue":"1","key":"7_CR28","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1109\/JPROC.2002.805818","volume":"91","author":"A. Tiwari","year":"2003","unstructured":"Tiwari, A., Shankar, N., Rushby, J.M.: Invisible Formal Methods for Embedded Control Systems. Proceedings of the IEEE\u00a091(1), 29\u201339 (2003)","journal-title":"Proceedings of the IEEE"},{"issue":"4","key":"7_CR29","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1145\/1113830.1113834","volume":"4","author":"S. Tripakis","year":"2005","unstructured":"Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time simulink to lustre. Trans. on Embedded Computing Sys.\u00a04(4), 779\u2013818 (2005)","journal-title":"Trans. on Embedded Computing Sys."},{"key":"7_CR30","volume-title":"Using Z: Specification, Refinement and Proof","author":"J. Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z: Specification, Refinement and Proof. Prentice Hall International, Englewood Cliffs (1996)"},{"key":"7_CR31","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"C.C. Zhou","year":"1991","unstructured":"Zhou, C.C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters\u00a040, 269\u2013276 (1991)","journal-title":"Information Processing Letters"},{"key":"7_CR32","volume-title":"A classical mind: essays in honour of C. A. R. Hoare","author":"C.C. Zhou","year":"1994","unstructured":"Zhou, C.C., Li, X.S.: A mean value calculus of durations. In: A classical mind: essays in honour of C. A. R. Hoare, Prentice-Hall International, Englewood Cliffs (1994)"},{"key":"7_CR33","first-page":"36","volume-title":"Hybrid Systems","author":"C.C. Zhou","year":"1993","unstructured":"Zhou, C.C., Ravn, A.P., Hansen, M.R.: An extended duration calculus for hybrid real-time systems. In: Hybrid Systems, pp. 36\u201359. Springer, Heidelberg (1993)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-76650-6_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:57:18Z","timestamp":1619506638000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-76650-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540766483","9783540766506"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-76650-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}