{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:09:10Z","timestamp":1748750950981,"version":"3.41.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319251400"},{"type":"electronic","value":"9783319251417"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25141-7_10","type":"book-chapter","created":{"date-parts":[[2015,10,31]],"date-time":"2015-10-31T08:51:25Z","timestamp":1446281485000},"page":"132-146","source":"Crossref","is-referenced-by-count":7,"title":["Formally Analyzing Continuous Aspects of\u00a0Cyber-Physical Systems Modeled by Homogeneous Linear Differential Equations"],"prefix":"10.1007","author":[{"given":"Muhammad Usman","family":"Sanwal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,1]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Abraham-Mumm, E., Steffen, M., Hannemann, U.: Verification of hybrid systems: formalization and proof rules in PVS. In: ICECCS, pp. 48\u201357 (2001)","DOI":"10.1109\/ICECCS.2001.930163"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Akella, R., McMillin, B.M.: Model-checking BNDC properties in cyber-physical systems. In: Computer Software and Applications Conference, pp. 660\u2013663 (2009)","DOI":"10.1109\/COMPSAC.2009.101"},{"issue":"1","key":"10_CR3","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/s10703-009-0079-8","volume":"35","author":"A Platzer","year":"2009","unstructured":"Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. Formal Methods Syst. Des. 35(1), 98\u2013120 (2009)","journal-title":"Formal Methods Syst. Des."},{"key":"10_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"10_CR5","volume-title":"Formal Methods: State of the Art and New Directions","author":"PP Boca","year":"2009","unstructured":"Boca, P.P., Bowen, J.P., Siddiqi, J.I.: Formal Methods: State of the Art and New Directions. Springer, Heidelberg (2009)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-14052-5_12","volume-title":"Interactive Theorem Proving","author":"S Boldo","year":"2010","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00e2tre, J.-C., Mayero, M., Melquiond, G., Weis, P.: Formal proof of a wave equation resolution scheme: the method error. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 147\u2013162. Springer, Heidelberg (2010)"},{"key":"10_CR7","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/2000367.2000368","volume":"2","author":"L Bu","year":"2011","unstructured":"Bu, L., Wang, Q., Chen, X., Wang, L., Zhang, T., Zhao, J., Li, X.: Towards online hybrid systems model checking of cyber-physical systems\u2019 time-bounded short-run behavior. SIGBED 2, 7\u201310 (2011)","journal-title":"SIGBED"},{"issue":"1","key":"10_CR8","first-page":"1","volume":"2","author":"RW Butler","year":"2009","unstructured":"Butler, R.W.: Formalization of the integral calculus in the PVS theorem prover. J. Formalized Reasoning 2(1), 1\u201326 (2009)","journal-title":"J. Formalized Reasoning"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-24372-1_1","volume-title":"Automated Technology for Verification and Analysis","author":"EM Clarke","year":"2011","unstructured":"Clarke, E.M., Zuliani, P.: Statistical model checking for cyber-physical systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 1\u201312. Springer, Heidelberg (2011)"},{"key":"10_CR10","unstructured":"Cruz-Filipe, L.: Constructive real analysis: a type-theoretical formalization and applications. Ph.D. thesis, University of Nijmegen, April 2004"},{"key":"10_CR11","doi-asserted-by":"crossref","DOI":"10.1525\/9780520323094","volume-title":"Mathematics for Biomedical Applications","author":"SA Glantz","year":"1979","unstructured":"Glantz, S.A.: Mathematics for Biomedical Applications. University of California Press, Berkeley (1979)"},{"key":"10_CR12","first-page":"376","volume":"236","author":"SA Glantz","year":"1979","unstructured":"Glantz, S.A., Tyberg, J.V.: Determination of frequency response from step response: application to fluid-filled catheters. Am. J. Physiol. 236, 376\u2013378 (1979)","journal-title":"Am. J. Physiol."},{"key":"10_CR13","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-1-4612-3658-0_10","volume-title":"Current Trends in Hardware Verification and Automated Theorem Proving","author":"MJC Gordon","year":"1989","unstructured":"Gordon, M.J.C.: Mechanizing programming logics in higher-order logic. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) Current Trends in Hardware Verification and Automated Theorem Proving, pp. 387\u2013439. Springer, Heidelberg (1989)"},{"key":"10_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-1591-5","volume-title":"Theorem Proving with the Real Numbers","author":"J Harrison","year":"1998","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers. Springer, Heidelberg (1998)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11541868_8","volume-title":"Theorem Proving in Higher Order Logics","author":"JV Harrison","year":"2005","unstructured":"Harrison, J.V.: A HOL theory of euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 114\u2013129. Springer, Heidelberg (2005)"},{"key":"10_CR16","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511576430","volume-title":"Handbook of Practical Logic and Automated Reasoning","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge (2009)"},{"issue":"4","key":"10_CR17","first-page":"1","volume":"41","author":"CAR Hoare","year":"2009","unstructured":"Hoare, C.A.R., Misra, J., Leavens, G.T., Shankar, N.: The verifed software initiative: a manifesto. ACM Comput. Surv. 41(4), 1\u20138 (2009)","journal-title":"ACM Comput. Surv."},{"key":"10_CR18","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1021\/i100024a600","volume":"25","author":"JO Hougen","year":"1986","unstructured":"Hougen, J.O., Hougen, S.T., Hougen, T.J.: Dynamics of fluid-filled catheter systems by pulse testing. Ind. Eng. Chem. Fundam. 25, 462\u2013470 (1986)","journal-title":"Ind. Eng. Chem. Fundam."},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-32347-8_26","volume-title":"Interactive Theorem Proving","author":"F Immler","year":"2012","unstructured":"Immler, F., H\u00f6lzl, J.: Numerical analysis of ordinary differential equations in Isabelle\/HOL. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 377\u2013392. Springer, Heidelberg (2012)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Liu, J., Zhang, L.: QoS modeling for cyber-physical systems using aspect-oriented approach. In: 2011 Second International Conference on Networking and Distributed Computing (ICNDC), pp. 154\u2013158 (2011)","DOI":"10.1109\/ICNDC.2011.38"},{"key":"10_CR21","unstructured":"Zhang, L., Hu, J., Yu, W.: Generating Test Cases for Cyber Physical Systems from Formal Specification, pp. 97\u2013103. Springerl, Heidelberg (2011)"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-642-31137-6_32","volume-title":"Computational Science and Its Applications \u2013 ICCSA 2012","author":"A Mashkoor","year":"2012","unstructured":"Mashkoor, A., Hasan, O.: Formal probabilistic analysis of cyber-physical transportation systems. In: Murgante, B., Gervasi, O., Misra, S., Nedjah, N., Rocha, A.M.A.C., Taniar, D., Apduhan, B.O. (eds.) ICCSA 2012, Part III. LNCS, vol. 7335, pp. 419\u2013434. Springer, Heidelberg (2012)"},{"issue":"1","key":"10_CR23","first-page":"7","volume":"2","author":"K Oduola","year":"2011","unstructured":"Oduola, K., Sofimieari, I., Nwambo, P.: A method for solving higher order homogeneous ordinary differential equations with non-constant coefficients. J. Emerg. Trends Eng. Appl. Sci. 2(1), 7\u201310 (2011)","journal-title":"J. Emerg. Trends Eng. Appl. Sci."},{"issue":"2","key":"10_CR24","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A Platzer","year":"2008","unstructured":"Platzer, A.: Differential dynamic logics for hybrid systems. J. Autom. Reasoning 41(2), 143\u2013189 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171\u2013178. Springer, Heidelberg (2008)"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Rajkumar, R., Lee, I., Sha, L., Stankovic, J.J.: Cyber-physical systems: the next computing revolution. In: 2010 47th ACM\/IEEE Design Automation Conference (DAC), pp. 731\u2013736 (2010)","DOI":"10.1145\/1837274.1837461"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-642-39637-3_29","volume-title":"Computational Science and Its Applications \u2013 ICCSA 2013","author":"MU Sanwal","year":"2013","unstructured":"Sanwal, M.U., Hasan, O.: Formal verification of cyber-physical systems: coping with continuous elements. In: Murgante, B., Misra, S., Carlini, M., Torre, C.M., Nguyen, H.-Q., Taniar, D., Apduhan, B.O., Gervasi, O. (eds.) ICCSA 2013, Part I. LNCS, vol. 7971, pp. 358\u2013371. Springer, Heidelberg (2013)"},{"key":"10_CR28","unstructured":"Sanwal, M.U.: Formal Reasoning about Homogeneous Linear Differential Equations (2013). http:\/\/save.seecs.nust.edu.pk\/students\/usman\/lde.html"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008)"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Thacker, R.A., Jones, K.R., Myers, C.J., Zheng, H.: Automatic abstraction for verification of cyber-physical systems. In: Proceedings of the 1st ACM\/IEEE International Conference on Cyber-Physical Systems, pp. 12\u201321. ACM (2010)","DOI":"10.1145\/1795194.1795197"},{"key":"10_CR31","first-page":"665","volume":"33","author":"H Zhang","year":"2006","unstructured":"Zhang, H., Liu, J.H., Holden, A.V.: Computing the age-related dysfunction of cardiac pacemaker. Comput. Cardiol. 33, 665\u2013668 (2006)","journal-title":"Comput. Cardiol."},{"issue":"4","key":"10_CR32","first-page":"823","volume":"7","author":"L Zhang","year":"2012","unstructured":"Zhang, L.: Aspect oriented formal techniques for cyber physical systems. J. Softw. 7(4), 823\u2013834 (2012)","journal-title":"J. Softw."},{"key":"10_CR33","volume-title":"Advanced Engineering Mathematics","author":"DG Zill","year":"2009","unstructured":"Zill, D.G., Wright, W.S., Cullen, M.R.: Advanced Engineering Mathematics, 4th edn. Jones and Bartlett Learning, London (2009)","edition":"4"}],"container-title":["Lecture Notes in Computer Science","Cyber Physical Systems. Design, Modeling, and Evaluation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25141-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T07:45:52Z","timestamp":1748677552000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25141-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319251400","9783319251417"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25141-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}