{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T16:45:19Z","timestamp":1725727519506},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642391750"},{"type":"electronic","value":"9783642391767"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39176-7_5","type":"book-chapter","created":{"date-parts":[[2013,5,30]],"date-time":"2013-05-30T04:58:44Z","timestamp":1369889924000},"page":"61-80","source":"Crossref","is-referenced-by-count":6,"title":["On-the-Fly Control Software Synthesis"],"prefix":"10.1007","author":[{"given":"Vadim","family":"Alimguzhin","sequence":"first","affiliation":[]},{"given":"Federico","family":"Mari","sequence":"additional","affiliation":[]},{"given":"Igor","family":"Melatti","sequence":"additional","affiliation":[]},{"given":"Ivano","family":"Salvo","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Tronci","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-540-31954-2_4","volume-title":"Hybrid Systems: Computation and Control","author":"M. Agrawal","year":"2005","unstructured":"Agrawal, M., Thiagarajan, P.S.: The discrete time behavior of lazy linear hybrid automata. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 55\u201369. Springer, Heidelberg (2005)"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E.: Automatic control software synthesis for quantized discrete time hybrid systems. In: CDC (2012)","DOI":"10.1109\/CDC.2012.6426260"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E.: On model based synthesis of embedded control software. In: EMSOFT, pp. 227\u2013236 (2012)","DOI":"10.1145\/2380356.2380398"},{"issue":"1","key":"5_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. TCS\u00a0138(1), 3\u201334 (1995)","journal-title":"TCS"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R.: Formal verification of hybrid systems. In: EMSOFT, pp. 273\u2013278 (2011)","DOI":"10.1145\/2038642.2038685"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-16558-0_10","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"T. Basten","year":"2010","unstructured":"Basten, T., et al.: Model-driven design-space exploration for embedded systems: The octopus toolset. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part I. LNCS, vol.\u00a06415, pp. 90\u2013105. Springer, Heidelberg (2010)"},{"key":"5_CR7","unstructured":"Bemporad, A.: Hybrid Toolbox (2004), \n                  \n                    http:\/\/cse.lab.imtlucca.it\/~bemporad\/hybrid\/toolbox\/"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-24743-2_9","volume-title":"Hybrid Systems: Computation and Control","author":"A. Bemporad","year":"2004","unstructured":"Bemporad, A., Giorgetti, N.: A SAT-based hybrid solver for optimal control of hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 126\u2013141. Springer, Heidelberg (2004)"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Benerecetti, M., Faella, M., Minopoli, S.: Revisiting synthesis of switching controllers for linear hybrid systems. In: CDC-ECC, pp. 4753\u20134758 (2011)","DOI":"10.1109\/CDC.2011.6161190"},{"key":"5_CR10","volume-title":"Modern control theory","author":"W.L. Brogan","year":"1991","unstructured":"Brogan, W.L.: Modern control theory, 3rd edn. Prentice-Hall, Inc., Upper Saddle River (1991)","edition":"3"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Buttazzo, G.C.: Hard Real-Time Computing Systems, 3rd edn. Springer (2011)","DOI":"10.1007\/978-1-4614-0676-1"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/11539452_9","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"F. Cassez","year":"2005","unstructured":"Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 66\u201380. Springer, Heidelberg (2005)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-22256-6_9","volume-title":"Implementation and Application of Automata","author":"G. Castiglione","year":"2011","unstructured":"Castiglione, G., Restivo, A., Sciortino, M.: Nondeterministic moore automata and brzozowski\u2019s algorithm. In: Bouchou-Markhoff, B., Caron, P., Champarnaud, J.-M., Maurel, D. (eds.) CIAA 2011. LNCS, vol.\u00a06807, pp. 88\u201399. Springer, Heidelberg (2011)"},{"key":"5_CR14","unstructured":"Cimatti, A., Roveri, M., Traverso, P.: Strong planning in non-deterministic domains via model checking. In: AIPS, pp. 36\u201343 (1998)"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Easwaran, A., Lee, I., Shin, I., Sokolsky, O.: Compositional schedulability analysis of hierarchical real-time systems. In: ISORC, pp. 274\u2013281 (2007)","DOI":"10.1109\/ISORC.2007.25"},{"issue":"3","key":"5_CR16","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","volume":"10","author":"G. Frehse","year":"2008","unstructured":"Frehse, G.: Phaver: algorithmic verification of hybrid systems past hytech. Int. J. Softw. Tools Technol. Transf.\u00a010(3), 263\u2013279 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/3-540-63166-6_47","volume-title":"Computer Aided Verification","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal: Status & Developments. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 456\u2013459. Springer, Heidelberg (1997)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"582","DOI":"10.1007\/3-540-63165-8_213","volume-title":"Automata, Languages and Programming","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Kopke, P.W.: Discrete-time control for rectangular hybrid automata. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol.\u00a01256, pp. 582\u2013593. Springer, Heidelberg (1997)"},{"issue":"5","key":"5_CR19","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The spin model checker. IEEE Trans. on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"5_CR20","unstructured":"Simulink by mathworks, \n                  \n                    http:\/\/www.mathworks.com"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Jha, S., Seshia, S.A., Tiwari, A.: Synthesis of optimal switching logic for hybrid systems. In: EMSOFT, pp. 107\u2013116. ACM (2011)","DOI":"10.1145\/2038642.2038660"},{"issue":"1","key":"5_CR22","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1109\/9.273337","volume":"39","author":"G. Kreisselmeier","year":"1994","unstructured":"Kreisselmeier, G., Birkh\u00f6lzer, T.: Numerical nonlinear regulator design. IEEE Trans. on on Automatic Control\u00a039(1), 33\u201346 (1994)","journal-title":"IEEE Trans. on on Automatic Control"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Lublinerman, R., Szegedy, C., Tripakis, S.: Modular code generation from synchronous block diagrams: modularity vs. code size. In: POPL, pp. 78\u201389 (2009)","DOI":"10.1145\/1594834.1480893"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Saha, I., Zamani, M.: Performance-aware scheduler synthesis for control systems. In: EMSOFT 2011, pp. 299\u2013308 (2011)","DOI":"10.1145\/2038642.2038689"},{"key":"5_CR25","unstructured":"Mari, F., Melatti, I., Salvo, I., Tronci, E.: Model based synthesis of control software from system level formal specifications. ACM Trans. Softw. Eng. Methodol. (to appear, 2013), A preliminary version is available at http:\/\/arxiv.org\/pdf\/1107.5638v2"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-642-14295-6_20","volume-title":"Computer Aided Verification","author":"F. Mari","year":"2010","unstructured":"Mari, F., Melatti, I., Salvo, I., Tronci, E.: Synthesis of quantized feedback control software for discrete time linear hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 180\u2013195. Springer, Heidelberg (2010)"},{"key":"5_CR27","unstructured":"Mari, F., Melatti, I., Salvo, I., Tronci, E.: Linear constraints as a modeling language for discrete time hybrid systems. In: ICSEA 2012, pp. 664\u2013671 (2012)"},{"issue":"3&4","key":"5_CR28","first-page":"212","volume":"5","author":"F. Mari","year":"2012","unstructured":"Mari, F., Melatti, I., Salvo, I., Tronci, E.: Synthesizing control software from boolean relations. Int. J. on Advances in SW\u00a05(3&4), 212\u2013223 (2012)","journal-title":"Int. J. on Advances in SW"},{"key":"5_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-32943-2_19","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2012","author":"F. Mari","year":"2012","unstructured":"Mari, F., Melatti, I., Salvo, I., Tronci, E.: Undecidability of quantized state feedback control for discrete time linear hybrid systems. In: Roychoudhury, A., D\u2019Souza, M. (eds.) ICTAC 2012. LNCS, vol.\u00a07521, pp. 243\u2013258. Springer, Heidelberg (2012)"},{"key":"5_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1007\/978-3-642-14295-6_49","volume-title":"Computer Aided Verification","author":"M. Mazo Jr.","year":"2010","unstructured":"Mazo Jr., M., Davitian, A., Tabuada, P.: PESSOA: A tool for embedded controller synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 566\u2013569. Springer, Heidelberg (2010)"},{"issue":"4","key":"5_CR31","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1016\/j.sysconle.2011.02.002","volume":"60","author":"M. Mazo","year":"2011","unstructured":"Mazo, M., Tabuada, P.: Symbolic approximate time-optimal control. Systems & Control Letters\u00a060(4), 256\u2013263 (2011)","journal-title":"Systems & Control Letters"},{"key":"5_CR32","unstructured":"Atmel megaAVR Microcontroller (2013), \n                  \n                    http:\/\/www.atmel.com\/products\/microcontrollers\/avr\/megaavr.aspx"},{"issue":"10","key":"5_CR33","doi-asserted-by":"publisher","first-page":"2508","DOI":"10.1016\/j.automatica.2008.02.021","volume":"44","author":"G. Pola","year":"2008","unstructured":"Pola, G., Girard, A., Tabuada, P.: Approximately bisimilar symbolic models for nonlinear control systems. Automatica\u00a044(10), 2508\u20132516 (2008)","journal-title":"Automatica"},{"key":"5_CR34","unstructured":"Reactis White Paper (2013), \n                  \n                    http:\/\/www.reactive-systems.com\/simulink-testing-validation.html"},{"key":"5_CR35","doi-asserted-by":"crossref","unstructured":"Roy, P., Tabuada, P., Majumdar, R.: Pessoa 2.0: a controller synthesis tool for cyber-physical systems. In: HSCC 2011, pp. 315\u2013316 (2011)","DOI":"10.1145\/1967701.1967748"},{"key":"5_CR36","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0577-7","volume-title":"Mathematical Control Theory: Deterministic Finite Dimensional Systems","author":"E.D. Sontag","year":"1998","unstructured":"Sontag, E.D.: Mathematical Control Theory: Deterministic Finite Dimensional Systems, 2nd edn. Springer, New York (1998)","edition":"2"},{"key":"5_CR37","unstructured":"Tronci, E.: Automatic synthesis of controllers from formal specifications. In: ICFEM, pp. 134\u2013143. IEEE (1998)"},{"key":"5_CR38","unstructured":"Wong-Toi, H.: The synthesis of controllers for linear hybrid automata. In: CDC, vol.\u00a05, pp. 4607\u20134612. IEEE (1997)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39176-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T09:03:31Z","timestamp":1557738211000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39176-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642391750","9783642391767"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39176-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}