{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:20:54Z","timestamp":1750306854932,"version":"3.41.0"},"reference-count":80,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,2,1]],"date-time":"2014-02-01T00:00:00Z","timestamp":1391212800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003407","name":"Ministero dell'Istruzione, dell'Universit\u00e0 e della Ricerca","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100003407","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2014,2]]},"abstract":"<jats:p>\n            Many\n            <jats:italic>embedded systems<\/jats:italic>\n            are indeed\n            <jats:italic>software-based control systems<\/jats:italic>\n            , that is, control systems whose controller consists of\n            <jats:italic>control software<\/jats:italic>\n            running on a microcontroller device. This motivates investigation on\n            <jats:italic>formal model-based design<\/jats:italic>\n            approaches for automatic synthesis of embedded systems control software. We present an algorithm, along with a tool QKS implementing it, that from a formal model (as a\n            <jats:italic>discrete-time linear hybrid system<\/jats:italic>\n            ) of the controlled system (\n            <jats:italic>plant<\/jats:italic>\n            ),\n            <jats:italic>implementation specifications<\/jats:italic>\n            (that is, number of bits in the\n            <jats:italic>Analog-to-Digital<\/jats:italic>\n            , AD, conversion) and\n            <jats:italic>system-level formal specifications<\/jats:italic>\n            (that is, safety and liveness requirements for the\n            <jats:italic>closed loop system<\/jats:italic>\n            ) returns correct-by-construction control software that has a\n            <jats:italic>Worst-Case Execution Time<\/jats:italic>\n            (WCET) linear in the number of AD bits and meets the given specifications. We show feasibility of our approach by presenting experimental results on using it to synthesize control software for a buck DC-DC converter, a widely used mixed-mode analog circuit, and for the inverted pendulum.\n          <\/jats:p>","DOI":"10.1145\/2559934","type":"journal-article","created":{"date-parts":[[2014,2,18]],"date-time":"2014-02-18T14:08:32Z","timestamp":1392732512000},"page":"1-42","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Model-based synthesis of control software from system-level formal specifications"],"prefix":"10.1145","volume":"23","author":[{"given":"Federico","family":"Mari","sequence":"first","affiliation":[{"name":"Sapienza University of Rome, Italy"}]},{"given":"Igor","family":"Melatti","sequence":"additional","affiliation":[{"name":"Sapienza University of Rome, Italy"}]},{"given":"Ivano","family":"Salvo","sequence":"additional","affiliation":[{"name":"Sapienza University of Rome, Italy"}]},{"given":"Enrico","family":"Tronci","sequence":"additional","affiliation":[{"name":"Sapienza University of Rome, Italy"}]}],"member":"320","published-online":{"date-parts":[[2014,2,20]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_4"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_4"},{"volume-title":"Proceedings of the Conference on Decision and Control (CDC'12)","author":"Alimguzhin V.","key":"e_1_2_1_3_1","unstructured":"V. Alimguzhin , F. Mari , I. Melatti , I. Salvo , and E. Tronci . 2012a. Automatic control software synthesis for quantized discrete time hybrid systems . In Proceedings of the Conference on Decision and Control (CDC'12) . To appear. (A preliminary version can be found at http:\/\/arxiv.org\/abs\/1207.4098.) V. Alimguzhin, F. Mari, I. Melatti, I. Salvo, and E. Tronci. 2012a. Automatic control software synthesis for quantized discrete time hybrid systems. In Proceedings of the Conference on Decision and Control (CDC'12). To appear. (A preliminary version can be found at http:\/\/arxiv.org\/abs\/1207.4098.)"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2380356.2380398"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1132357.1132363"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.871304"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.489079"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30080-9_1"},{"key":"e_1_2_1_10_1","series-title":"Lecture Notes in Computer Science","volume-title":"Hybrid Systems: Computation and Control (HSCC'99)","author":"Asarin E.","year":"1999","unstructured":"E. Asarin and O. Maler . 1999 . As soon as possible: Time optimal control for timed automata. In Proceedings of the International Workshop on Hybrid Systems: Computation and Control (HSCC'99) . Lecture Notes in Computer Science , vol. 1569 , Springer , 19--30. E. Asarin and O. Maler. 1999. As soon as possible: Time optimal control for timed automata. In Proceedings of the International Workshop on Hybrid Systems: Computation and Control (HSCC'99). Lecture Notes in Computer Science, vol. 1569, Springer, 19--30."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/963778.963782"},{"key":"e_1_2_1_12_1","unstructured":"A. Bemporad. 2004. Hybrid toolbox. http:\/\/cse.lab.imtlucca.it\/&sim;bemporad\/hybrid\/toolbox\/.  A. Bemporad. 2004. Hybrid toolbox. http:\/\/cse.lab.imtlucca.it\/&sim;bemporad\/hybrid\/toolbox\/."},{"key":"e_1_2_1_13_1","series-title":"Lecture Notes in Computer Science","volume-title":"Hybrid Systems: Computation and Control (HSCC'04)","author":"Bemporad A.","year":"2004","unstructured":"A. Bemporad and N. Giorgetti . 2004 . A sat-based hybrid solver for optimal control of hybrid systems. In Proceedings of the 7th International Workshop on Hybrid Systems: Computation and Control (HSCC'04) . Lecture Notes in Computer Science , vol. 2993 , Springer , 126--141. A. Bemporad and N. Giorgetti. 2004. A sat-based hybrid solver for optimal control of hybrid systems. In Proceedings of the 7th International Workshop on Hybrid Systems: Computation and Control (HSCC'04). Lecture Notes in Computer Science, vol. 2993, Springer, 126--141."},{"volume-title":"Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC'11)","author":"Benerecetti M.","key":"e_1_2_1_14_1","unstructured":"M. Benerecetti , M. Faella , and S. Minopoli . 2011. Revisiting synthesis of switching controllers for linear hybrid systems . In Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC'11) . 4753--4758. M. Benerecetti, M. Faella, and S. Minopoli. 2011. Revisiting synthesis of switching controllers for linear hybrid systems. In Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC'11). 4753--4758."},{"key":"e_1_2_1_15_1","volume-title":"Modern Control Theory","author":"Brogan W. L.","unstructured":"W. L. Brogan . 1991. Modern Control Theory 3 rd Ed. Prentice-Hall , Upper Saddle River, NJ. W. L. Brogan. 1991. Modern Control Theory 3rd Ed. Prentice-Hall, Upper Saddle River, NJ.","edition":"3"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_9"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"P. Cern\u00fd K. Chatterjee T. A. Henzinger A. Radhakrishna and R. Singh. 2011. Quantitative synthesis for concurrent programs. In Computer Aided Verification G. Gopalakrishnan and S. Qadeer Eds. Springer 243--259.   P. Cern\u00fd K. Chatterjee T. A. Henzinger A. Radhakrishna and R. Singh. 2011. Quantitative synthesis for concurrent programs. In Computer Aided Verification G. Gopalakrishnan and S. Qadeer Eds. Springer 243--259.","DOI":"10.1007\/978-3-642-22110-1_20"},{"volume-title":"Proceedings of the 4th International Conference on Artificial Intelligence Planning Systems (AIPS'98)","author":"Cimatti A.","key":"e_1_2_1_19_1","unstructured":"A. Cimatti , M. Roveri , and P. Traverso . 1998. Strong planning in non-deterministic domains via model checking . In Proceedings of the 4th International Conference on Artificial Intelligence Planning Systems (AIPS'98) . 36--43. A. Cimatti, M. Roveri, and P. Traverso. 1998. Strong planning in non-deterministic domains via model checking. In Proceedings of the 4th International Conference on Artificial Intelligence Planning Systems (AIPS'98). 36--43."},{"volume-title":"Proceedings of the 19th International Conference on Automated Planning and Scheduling (ICAPS'09)","author":"Della Penna G.","key":"e_1_2_1_20_1","unstructured":"G. Della Penna , D. Magazzeni , F. Mercorio , and B. Intrigila . 2009. UPMurphi: A tool for universal planning on pddl&plus; problems . In Proceedings of the 19th International Conference on Automated Planning and Scheduling (ICAPS'09) . 106--113. G. Della Penna, D. Magazzeni, F. Mercorio, and B. Intrigila. 2009. UPMurphi: A tool for universal planning on pddl&plus; problems. In Proceedings of the 19th International Conference on Automated Planning and Scheduling (ICAPS'09). 106--113."},{"key":"e_1_2_1_21_1","volume-title":"Lecture Notes in Electrical Engineering","volume":"15","author":"Della Penna G.","unstructured":"G. Della Penna , D. Magazzeni , A. Tofani , B. Intrigila , I. Melatti , and E. Tronci . 2008. Automated Generation of Optimal Controllers through Model Checking Techniques . Lecture Notes in Electrical Engineering , vol. 15 , Springer. G. Della Penna, D. Magazzeni, A. Tofani, B. Intrigila, I. Melatti, and E. Tronci. 2008. Automated Generation of Optimal Controllers through Model Checking Techniques. Lecture Notes in Electrical Engineering, vol. 15, Springer."},{"volume-title":"Proceedings of the IEEE Power Electronics Specialists Conference (PESC'08)","author":"Dominguez-Garcia A.","key":"e_1_2_1_22_1","unstructured":"A. Dominguez-Garcia and P. Krein . 2008. Integrating reliability into the design of fault-tolerant power electronics systems . In Proceedings of the IEEE Power Electronics Specialists Conference (PESC'08) . 2665--2671. A. Dominguez-Garcia and P. Krein. 2008. Integrating reliability into the design of fault-tolerant power electronics systems. In Proceedings of the IEEE Power Electronics Specialists Conference (PESC'08). 2665--2671."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805829"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0062-x"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2005.858689"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2009.2034922"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0084-y"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"T.\n      Gvero V.\n      Kuncak and \n      R.\n      Piskac\n  . \n  2011\n  . Interactive synthesis of code snippets. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11). G. Gopalakrishnan and S. Qadeer Eds. Lecture Notes in Computer Science vol. \n  6806 Springer 418--423.   T. Gvero V. Kuncak and R. Piskac. 2011. Interactive synthesis of code snippets. In Proceedings of the 23 rd International Conference on Computer Aided Verification (CAV'11). G. Gopalakrishnan and S. Qadeer Eds. Lecture Notes in Computer Science vol. 6806 Springer 418--423.","DOI":"10.1007\/978-3-642-22110-1_33"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050008"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706319"},{"volume-title":"Proceedings of the 24th Colloquium on Automata, Languages, and Programming (ICALP'97)","author":"Henzinger T. A.","key":"e_1_2_1_32_1","unstructured":"T. A. Henzinger and P. W. Kopke . 1997. Discrete-time control for rectangular hybrid automata . In Proceedings of the 24th Colloquium on Automata, Languages, and Programming (ICALP'97) . 582--593. T. A. Henzinger and P. W. Kopke. 1997. Discrete-time control for rectangular hybrid automata. In Proceedings of the 24th Colloquium on Automata, Languages, and Programming (ICALP'97). 582--593."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_1"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1879021.1879062"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038660"},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"S. K. Jha S. Gulwani S. A. Seshia and A. Tiwari. 2010. Synthesizing switching logic for safety and dwell-time requirements. Tech. rep. UCB\/EECS-2010-28 EECS Department University of California Berkeley.  S. K. Jha S. Gulwani S. A. Seshia and A. Tiwari. 2010. Synthesizing switching logic for safety and dwell-time requirements. Tech. rep. UCB\/EECS-2010-28 EECS Department University of California Berkeley.","DOI":"10.1145\/1795194.1795198"},{"volume-title":"Proceedings of the Workshop on Architectural Support for Gigascale Integration (ASGI'07)","author":"Kim W.","key":"e_1_2_1_38_1","unstructured":"W. Kim , M. S. Gupta , G.-Y. Wei , and D. M. Brooks . 2007. Enabling on-chip switching regulators for multi-core processors using current staggering . In Proceedings of the Workshop on Architectural Support for Gigascale Integration (ASGI'07) . W. Kim, M. S. Gupta, G.-Y. Wei, and D. M. Brooks. 2007. Enabling on-chip switching regulators for multi-core processors using current staggering. In Proceedings of the Workshop on Architectural Support for Gigascale Integration (ASGI'07)."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/9.273337"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_38"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2076450.2076472"},{"key":"e_1_2_1_42_1","series-title":"Lecture Notes in Computer Science","volume-title":"Uppaal: Status and developments. In Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97)","author":"Larsen K. G.","year":"1997","unstructured":"K. G. Larsen , P. Pettersson , and W. Yi . 1997 . Uppaal: Status and developments. In Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97) . Lecture Notes in Computer Science , vol. 1254 , Springer , 456--459. K. G. Larsen, P. Pettersson, and W. Yi. 1997. Uppaal: Status and developments. In Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97). Lecture Notes in Computer Science, vol. 1254, Springer, 456--459."},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"O.\n      Maler Z.\n      Manna and \n      A.\n      Pnueli\n  . \n  1992\n  . From timed to hybrid systems. In Proceedings of the REX Workshop on Real-Time: Theory in Practice. J. W. de Bakker C. Huizing W. P. de Roever and G. Rozenberg Eds. Lecture Notes in Computer Science vol. \n  600 Springer 447--484.   O. Maler Z. Manna and A. Pnueli. 1992. From timed to hybrid systems. In Proceedings of the REX Workshop on Real-Time: Theory in Practice. J. W. de Bakker C. Huizing W. P. de Roever and G. Rozenberg Eds. Lecture Notes in Computer Science vol. 600 Springer 447--484.","DOI":"10.1007\/BFb0032003"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770368"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_20"},{"volume-title":"Proceedings of the 6th International Conference on Software Engineering Advances (ICSEA'11)","author":"Mari F.","key":"e_1_2_1_46_1","unstructured":"F. Mari , I. Melatti , I. Salvo , and E. Tronci . 2011a. From boolean relations to control software . In Proceedings of the 6th International Conference on Software Engineering Advances (ICSEA'11) . F. Mari, I. Melatti, I. Salvo, and E. Tronci. 2011a. From boolean relations to control software. In Proceedings of the 6th International Conference on Software Engineering Advances (ICSEA'11)."},{"key":"e_1_2_1_47_1","doi-asserted-by":"crossref","unstructured":"F. Mari I. Melatti I. Salvo and E. Tronci. 2011b. Quantized feedback control software synthesis from system level formal specifications. CoRR abs\/1107.5638v1.  F. Mari I. Melatti I. Salvo and E. Tronci. 2011b. Quantized feedback control software synthesis from system level formal specifications. CoRR abs\/1107.5638v1.","DOI":"10.1145\/2559934"},{"key":"e_1_2_1_48_1","unstructured":"F. Mari I. Melatti I. Salvo and E. Tronci. 2011c. Quantized feedback control software synthesis from system level formal specifications for buck dc\/dc converters. CoRR abs\/1105.5640. http:\/\/arxiv.org\/pdf\/1105.5640.pdf.  F. Mari I. Melatti I. Salvo and E. Tronci. 2011c. Quantized feedback control software synthesis from system level formal specifications for buck dc\/dc converters. CoRR abs\/1105.5640. http:\/\/arxiv.org\/pdf\/1105.5640.pdf."},{"volume-title":"Proceedings of the 2nd International Conference on Advanced Communications and Computation (INFOCOMP'12)","author":"Mari F.","key":"e_1_2_1_49_1","unstructured":"F. Mari , I. Melatti , I. Salvo , and E. Tronci . 2012a. Control software visualization . In Proceedings of the 2nd International Conference on Advanced Communications and Computation (INFOCOMP'12) . ThinkMind, 15--20. F. Mari, I. Melatti, I. Salvo, and E. Tronci. 2012a. Control software visualization. In Proceedings of the 2nd International Conference on Advanced Communications and Computation (INFOCOMP'12). ThinkMind, 15--20."},{"volume-title":"Proceedings of the 7th International Conference on Software Engineering Advances. ThinkMind, 664--671","author":"Mari F.","key":"e_1_2_1_50_1","unstructured":"F. Mari , I. Melatti , I. Salvo , and E. Tronci . 2012b. Linear constraints as a modeling language for discrete time hybrid systems . In Proceedings of the 7th International Conference on Software Engineering Advances. ThinkMind, 664--671 . F. Mari, I. Melatti, I. Salvo, and E. Tronci. 2012b. Linear constraints as a modeling language for discrete time hybrid systems. In Proceedings of the 7th International Conference on Software Engineering Advances. ThinkMind, 664--671."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32943-2_19"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_49"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysconle.2011.02.002"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_51"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10107-003-0433-3"},{"key":"e_1_2_1_56_1","volume-title":"Synthia: Verification and synthesis for timed automata","author":"Peter H.-J.","year":"2011","unstructured":"H.-J. Peter , R. Ehlers , and R. Mattm\u00fcller . 2011 . Synthia: Verification and synthesis for timed automata . In Computer Aided Verification. G. Gopalakrishnan and S. Qadeer, Eds., Springer , 649--655. H.-J. Peter, R. Ehlers, and R. Mattm\u00fcller. 2011. Synthia: Verification and synthesis for timed automata. In Computer Aided Verification. G. Gopalakrishnan and S. Qadeer, Eds., Springer, 649--655."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_35"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_2_1_59_1","doi-asserted-by":"crossref","unstructured":"A.\n      Pnueli\n     and \n      R.\n      Rosner\n  . \n  1989\n  b. On the synthesis of an asynchronous reactive module. In Proceedings of the Conference on Automata Languages and Programming (ICALP'89). G. Ausiello M. Dezani-Ciancaglini and S. R. D. Rocca Eds. Lecture Notes in Computer Science vol. \n  372 Springer 652--671.   A. Pnueli and R. Rosner. 1989b. On the synthesis of an asynchronous reactive module. In Proceedings of the Conference on Automata Languages and Programming (ICALP'89). G. Ausiello M. Dezani-Ciancaglini and S. R. D. Rocca Eds. Lecture Notes in Computer Science vol. 372 Springer 652--671.","DOI":"10.1007\/BFb0035790"},{"volume-title":"Proceedings of the 46th IEEE Conference on Decision and Control. 4656--4661","author":"Pola G.","key":"e_1_2_1_60_1","unstructured":"G. Pola , A. Girard , and P. Tabuada . 2007. Symbolic models for nonlinear control systems using approximate bisimulation . In Proceedings of the 46th IEEE Conference on Decision and Control. 4656--4661 . G. Pola, A. Girard, and P. Tabuada. 2007. Symbolic models for nonlinear control systems using approximate bisimulation. In Proceedings of the 46th IEEE Conference on Decision and Control. 4656--4661."},{"key":"e_1_2_1_61_1","doi-asserted-by":"crossref","unstructured":"QKS Web Page. 2011. http:\/\/mclab.di.uniroma1.it\/.  QKS Web Page. 2011. http:\/\/mclab.di.uniroma1.it\/.","DOI":"10.1016\/B978-0-08-096932-9.10014-6"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1137\/0325013"},{"key":"e_1_2_1_63_1","doi-asserted-by":"crossref","unstructured":"S. Sankaranarayanan and A. Tiwari. 2011. Relational abstractions for continuous and hybrid systems. In Computer Aided Verification. G. Gopalakrishnan and S. Qadeer Eds. Springer 686--702.   S. Sankaranarayanan and A. Tiwari. 2011. Relational abstractions for continuous and hybrid systems. In Computer Aided Verification. G. Gopalakrishnan and S. Qadeer Eds. Springer 686--702.","DOI":"10.1007\/978-3-642-22110-1_56"},{"key":"e_1_2_1_64_1","unstructured":"SCADE Web Page. 2012. http:\/\/www.esterel-technologies.com\/products\/scade-system\/.  SCADE Web Page. 2012. http:\/\/www.esterel-technologies.com\/products\/scade-system\/."},{"key":"e_1_2_1_65_1","doi-asserted-by":"crossref","unstructured":"S.\n      Schewe\n     and \n      B.\n      Finkbeiner\n  . \n  2006\n  . Synthesis of asynchronous systems. In Proceedings of the 16th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'06). G. Puebla Ed. Lecture Notes in Computer Science Series vol. \n  4407 Springer 127--142.   S. Schewe and B. Finkbeiner. 2006. Synthesis of asynchronous systems. In Proceedings of the 16 th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'06). G. Puebla Ed. Lecture Notes in Computer Science Series vol. 4407 Springer 127--142.","DOI":"10.1007\/978-3-540-71410-1_10"},{"volume-title":"Proceedings of the 35th Annual IEEE Power Electronics Specialist Conference (PESC'04)","author":"Schrom G.","key":"e_1_2_1_66_1","unstructured":"G. Schrom , P. Hazucha , J. Hahn , D. Gardner , B. Bloechel , G. Dermer , S. Narendra , T. Karnik , and V. De . 2004. A 480-mhz, multi-phase interleaved buck dc-dc converter with hysteretic control . In Proceedings of the 35th Annual IEEE Power Electronics Specialist Conference (PESC'04) . 4702--4707. G. Schrom, P. Hazucha, J. Hahn, D. Gardner, B. Bloechel, G. Dermer, S. Narendra, T. Karnik, and V. De. 2004. A 480-mhz, multi-phase interleaved buck dc-dc converter with hysteretic control. In Proceedings of the 35th Annual IEEE Power Electronics Specialist Conference (PESC'04). 4702--4707."},{"key":"e_1_2_1_67_1","unstructured":"Simulink Web Page. 2012. http:\/\/www.mathworks.it\/products\/simulink\/.  Simulink Web Page. 2012. http:\/\/www.mathworks.it\/products\/simulink\/."},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1109\/63.484413"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993557"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706337"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_25"},{"key":"e_1_2_1_72_1","unstructured":"Texas Instruments. 2001. Slvp182: High accuracy synchronous buck dc-dc converter. http:\/\/focus.ti.com.cn\/cn\/lit\/ug\/slvu046\/slvu046.pdf.  Texas Instruments. 2001. Slvp182: High accuracy synchronous buck dc-dc converter. http:\/\/focus.ti.com.cn\/cn\/lit\/ug\/slvu046\/slvu046.pdf."},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-007-0044-3"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.1996.572981"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.1997.652410"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.5555\/552895.857374"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.5555\/519308.786897"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.5555\/645433.652617"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.1997.649708"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPEL.2008.924843"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2559934","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2559934","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:10:25Z","timestamp":1750234225000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2559934"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2]]},"references-count":80,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["10.1145\/2559934"],"URL":"https:\/\/doi.org\/10.1145\/2559934","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2014,2]]},"assertion":[{"value":"2012-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-02-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}