{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T12:40:09Z","timestamp":1746362409295,"version":"3.40.4"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319107011"},{"type":"electronic","value":"9783319107028"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10702-8_1","type":"book-chapter","created":{"date-parts":[[2014,9,1]],"date-time":"2014-09-01T12:19:16Z","timestamp":1409573956000},"page":"1-15","source":"Crossref","is-referenced-by-count":6,"title":["Formal Verification of Steady-State Errors in Unity-Feedback Control Systems"],"prefix":"10.1007","author":[{"given":"Muhammad","family":"Ahmad","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"1_CR1","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/s00165-010-0170-3","volume":"23","author":"P. Clayton","year":"2011","unstructured":"Clayton, P., Cavalcanti, A., O\u2019Halloran, C.: From Control Law Diagrams to Ada via Circus. Formal Aspects of Computing\u00a023(4), 465\u2013512 (2011)","journal-title":"Formal Aspects of Computing"},{"doi-asserted-by":"crossref","unstructured":"Ahmad, M.: Formal Verification of Steady State Errors in Unity-Feedback Control Systems (2014), http:\/\/save.seecs.nust.edu.pk\/students\/ahmad\/sseufcs.html","key":"1_CR2","DOI":"10.1007\/978-3-319-10702-8_1"},{"doi-asserted-by":"crossref","unstructured":"Alur, R.: Formal Verification of Hybrid Systems. In: Embedded Software, pp. 273\u2013278 (2011)","key":"1_CR3","DOI":"10.1145\/2038642.2038685"},{"doi-asserted-by":"crossref","unstructured":"Arthan, R., Caseley, P., O\u2019Halloran, C., Smith, A.: ClawZ: Control Laws in Z. In: Formal Engineering Methods, pp. 169\u2013176 (2000)","key":"1_CR4","DOI":"10.1109\/ICFEM.2000.873817"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-24756-2_2","volume-title":"Integrated Formal Methods","author":"R.J. Boulton","year":"2004","unstructured":"Boulton, R.J., Gottliebsen, H., Hardy, R., Kelsey, T., Martin, U.: Design Verification for Control Engineering. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 21\u201335. Springer, Heidelberg (2004)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/3-540-36580-X_11","volume-title":"Hybrid Systems: Computation and Control","author":"R.J. Boulton","year":"2003","unstructured":"Boulton, R.J., Hardy, R., Martin, U.: A Hoare Logic for Single-Input Single-Output Continuous-Time Control Systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol.\u00a02623, pp. 113\u2013125. Springer, Heidelberg (2003)"},{"issue":"5","key":"1_CR7","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/s00165-009-0108-9","volume":"21","author":"J.S. Dong","year":"2009","unstructured":"Dong, J.S., Chen, C., Sun, J.: A Formal framework for Modeling and Validating Simulink diagrams. Formal Aspects of Computing\u00a021(5), 451\u2013483 (2009)","journal-title":"Formal Aspects of Computing"},{"issue":"1","key":"1_CR8","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1109\/41.345854","volume":"42","author":"D. Czarkowski","year":"1995","unstructured":"Czarkowski, D., Pujara, L.R., Kazimierczuk, M.K.: Robust Stability of State-Feedback Control of PWM DC-DC push-pull Converter. IEEE Transaction on Industrial Electronics\u00a042(1), 108\u2013111 (1995)","journal-title":"IEEE Transaction on Industrial Electronics"},{"key":"1_CR9","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":"J. Harrison","year":"2005","unstructured":"Harrison, J.: A HOL Theory of Euclidean Space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 114\u2013129. Springer, Heidelberg (2005)"},{"key":"1_CR10","first-page":"151","volume":"10","author":"J. Harrison","year":"2007","unstructured":"Harrison, J.: Formalizing Basic Complex Analysis. Studies in Logic, Grammar and Rhetoric\u00a010, 151\u2013165 (2007)","journal-title":"Studies in Logic, Grammar and Rhetoric"},{"issue":"2","key":"1_CR11","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-012-9250-9","volume":"50","author":"J. Harrison","year":"2013","unstructured":"Harrison, J.: The HOL Light Theory of Euclidean Space. Journal of Automated Reasoning\u00a050(2), 173\u2013190 (2013)","journal-title":"Journal of Automated Reasoning"},{"doi-asserted-by":"crossref","unstructured":"Hasan, O., Ahmad, M.: Formal analysis of steady state errors in feedback control systems using HOL-light. In: Proceedings of the Conference on Design, Automation and Test in Europe, DATE 2013, pp. 1423\u20131426 (2013)","key":"1_CR12","DOI":"10.7873\/DATE.2013.290"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-28891-3_15","volume-title":"NASA Formal Methods","author":"H. Herencia-Zapana","year":"2012","unstructured":"Herencia-Zapana, H., Jobredeaux, R., Owre, S., Garoche, P.-L., Feron, E., Perez, G., Ascariz, P.: PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C\/ACSL. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol.\u00a07226, pp. 147\u2013161. Springer, Heidelberg (2012)"},{"issue":"4","key":"1_CR14","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/s11768-012-0064-4","volume":"10","author":"Y. Hote","year":"2012","unstructured":"Hote, Y.: A New Approach to Time Domain Analysis of Perturbed PWM push-pull DC-DC Converter. Journal of Control Theory and Applications\u00a010(4), 465\u2013469 (2012)","journal-title":"Journal of Control Theory and Applications"},{"issue":"11","key":"1_CR15","doi-asserted-by":"publisher","first-page":"1368","DOI":"10.1080\/00207170600725552","volume":"79","author":"M.D. Lutovac","year":"2006","unstructured":"Lutovac, M.D., To\u0161ic, D.V.: Symbolic Analysis and Design of Control Systems using Mathematica. International Journal of Control\u00a079(11), 1368\u20131381 (2006)","journal-title":"International Journal of Control"},{"unstructured":"Mahony, B.: The DOVE approach to the Design of Complex Dynamic Processes. In: Workshop on Formalising Continuous Mathematics, pp. 167\u2013187. NASA Conference Publication (2002)","key":"1_CR16"},{"unstructured":"MathWorks Simulink (2012), http:\/\/www.mathworks.com\/products\/simulink","key":"1_CR17"},{"unstructured":"Nise, N.S.: Control System Engineering. Wiley and Sons (2003)","key":"1_CR18"},{"unstructured":"Ogata, K.: Modern Control Engineering. Prentice-Hall (1997)","key":"1_CR19"},{"unstructured":"Pike, L.: Pervasive Formal Verification in Control System. In: Formal Methods in Computer-Aided Design. Panel Discussion (2011)","key":"1_CR20"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"744","DOI":"10.1007\/978-3-642-45221-5_50","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S.H. Taqdees","year":"2013","unstructured":"Taqdees, S.H., Hasan, O.: Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19. LNCS, vol.\u00a08312, pp. 744\u2013758. Springer, Heidelberg (2013)"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/3-540-45873-5_36","volume-title":"Hybrid Systems: Computation and Control","author":"A. Tiwari","year":"2002","unstructured":"Tiwari, A., Khanna, G.: Series of Abstractions for Hybrid Automata. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol.\u00a02289, pp. 465\u2013478. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10702-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T12:22:01Z","timestamp":1746361321000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10702-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319107011","9783319107028"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10702-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}