{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T20:53:42Z","timestamp":1742936022671,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642260094"},{"type":"electronic","value":"9783642260100"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-26010-0_13","type":"book-chapter","created":{"date-parts":[[2011,12,2]],"date-time":"2011-12-02T08:25:49Z","timestamp":1322814349000},"page":"112-121","source":"Crossref","is-referenced-by-count":2,"title":["Formal Verification of DEV&DESS Formalism Using Symbolic Model Checker HyTech"],"prefix":"10.1007","author":[{"given":"Han","family":"Choi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sungdeok","family":"Cha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jae Yeon","family":"Jo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Junbeom","family":"Yoo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hae Young","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Won-Tae","family":"Kim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"13_CR1","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. Theoretical Computer Science\u00a0138(1), 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"13_CR2","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1109\/JPROC.2002.805817","volume":"91","author":"R. Alur","year":"2003","unstructured":"Alur, R., Dang, T., Esposito, J., Hur, Y., Ivan\u010di\u0107, F., Vijay Kumar, I.L., Mishra, P., Pappas, G.J., Sokolsky, O.: Hierarchical modeling and analysis of embedded systems. Proceedings of the IEEE\u00a091(1), 11\u201328 (2003)","journal-title":"Proceedings of the IEEE"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126 (1994)","DOI":"10.1016\/0304-3975(94)90010-8"},{"issue":"3","key":"13_CR4","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"R. Alur","year":"1996","unstructured":"Alur, R., Henzinger, T.A., Ho, P.H.: Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering\u00a022(3), 181\u2013201 (1996)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/3-540-60472-3","volume-title":"Hybrid Systems II","author":"P.J. Antsaklis","year":"1995","unstructured":"Antsaklis, P.J., Stiver, J.A., Lemmon, M.D.: Interface and Controller Design for Hybrid Control Systems. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol.\u00a0999, pp. 462\u2013492. Springer, Heidelberg (1995)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-45657-0_30","volume-title":"Computer Aided Verification","author":"E. Asarin","year":"2002","unstructured":"Asarin, E., Dang, T., Maler, O.: The d\/dt Tool for Verification of Hybrid Systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 365\u2013770. Springer, Heidelberg (2002)"},{"issue":"7","key":"13_CR7","doi-asserted-by":"publisher","first-page":"888","DOI":"10.1109\/5.871300","volume":"88","author":"A. Balluchi","year":"2000","unstructured":"Balluchi, A., Benvenuti, L., Benedetto, M., Pinello, C., Sangiovanni-Vincentelli, A.: Automotive engine control and hybrid systems: challenges and opportunities. Proceedings of the IEEE\u00a088(7), 888\u2013912 (2000)","journal-title":"Proceedings of the IEEE"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-48983-5_10","volume-title":"Hybrid Systems: Computation and Control","author":"A. Chutinan","year":"1999","unstructured":"Chutinan, A., Krogh, B.H.: Verification of Polyhedral-Invariant Hybrid Automata Using Polygonal Flow Pipe Approximations. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol.\u00a01569, pp. 76\u201390. Springer, Heidelberg (1999)"},{"key":"13_CR9","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/BFb0020947","volume-title":"Hybrid Systems III","author":"C. Daws","year":"1996","unstructured":"Daws, C., Olivero, A., Trypakis, S., Yovine, S.: The Tool Kronos. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol.\u00a01066, pp. 208\u2013219. Springer, Heidelberg (1996)"},{"issue":"3","key":"13_CR11","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1109\/TSMCA.2006.886378","volume":"37","author":"J.M. Esposito","year":"2007","unstructured":"Esposito, J.M., Kim, M.: Using formal modeling with an automated analysis tool to design and parametrically analyze a multirobot coordination protocol: A case study. IEEE Transactions on Systems, Man and Cybernetics, Part A: Systems and Humans\u00a037(3), 285\u2013297 (2007)","journal-title":"IEEE Transactions on Systems, Man and Cybernetics, Part A: Systems and Humans"},{"issue":"1-2","key":"13_CR12","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.H., Wong-Toi, H.: Hytech: a model checker for hybrid systems. Software Tools for Technology Transfer\u00a01(1-2), 110\u2013122 (1997)","journal-title":"Software Tools for Technology Transfer"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0027241","volume-title":"Formal Methods for Industrial Applications","author":"T.A. Henzinger","year":"1996","unstructured":"Henzinger, T.A., Wong-Toi, H.: Using Hytech to Synthesize Control Parameters for a Steam Boiler. In: Abrial, J.-R., B\u00f6rger, E., Langmaack, H. (eds.) Dagstuhl Seminar 1995. LNCS, vol.\u00a01165, pp. 265\u2013282. Springer, Heidelberg (1996)"},{"issue":"3","key":"13_CR14","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1177\/1548512910389203","volume":"8","author":"T.G. Kim","year":"2011","unstructured":"Kim, T.G., Sung, C.H., Hong, S.Y., Hong, J.H., Choi, C.B., Kim, J.H., Seo, K.M., Bae, J.W.: Devsim++ toolset for defense modeling and simulation and interoperation. The Journal of Defense Modeling and Simulation: Applications, Methodology, Technology\u00a08(3), 129\u2013142 (2011)","journal-title":"The Journal of Defense Modeling and Simulation: Applications, Methodology, Technology"},{"key":"13_CR15","unstructured":"Lee, D.A., Lee, J.H., Yoo, J., Kim, D.H.: Systematic verification of operational flight program through reverse engineering. In: International Conference on Advanced Software Engineering & Its Applications (submitted, 2011)"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/3-540-46430-1_27","volume-title":"Hybrid Systems: Computation and Control","author":"I. Mitchell","year":"2000","unstructured":"Mitchell, I., Tomlin, C.J.: Level Set Methods for Computation in Hybrid Systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol.\u00a01790, pp. 310\u2013323. Springer, Heidelberg (2000)"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Praehofer, H.: Systems Theoretic Foundations for Combined Discrete Continuous System Simulation. Ph.D. thesis, Department of Systems Theory, University of Linz, Autria (1991)","DOI":"10.1080\/03081079108935175"},{"key":"13_CR18","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/BF01439846","volume":"3","author":"H. Praehofer","year":"1993","unstructured":"Praehofer, H., Auernig, F., Reisinger, G.: An environment for devs-based multiformalism simulation in common lisp\/CLOS. Discrete Event Dynamic Systems: Theory and Application\u00a03, 119\u2013149 (1993)","journal-title":"Discrete Event Dynamic Systems: Theory and Application"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Praehofer, H., Pree, D.: Visual modeling of devs-based multiformalism systems based on higraphs. In: Simulation Conference Proceedings, pp. 595\u2013603 (December 1993)","DOI":"10.1145\/256563.256737"},{"issue":"4","key":"13_CR20","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/9.664154","volume":"43","author":"C. Tomlin","year":"1998","unstructured":"Tomlin, C., Pappas, G., Sastry, S.: Conflict resolution for air traffic management: a study in multiagent hybrid systems. IEEE Transactions on Automatic Control\u00a043(4), 509\u2013521 (1998)","journal-title":"IEEE Transactions on Automatic Control"},{"key":"13_CR21","unstructured":"UPPAAL (2010), \n                  \n                    https:\/\/2.zoppoz.workers.dev:443\/http\/www.uppaal.com\/"},{"key":"13_CR22","unstructured":"Zeigler, B.P., Praehofer, H., Kim, T.G.: Theory of Modeling and Simulation. Academic Press (2000)"}],"container-title":["Communications in Computer and Information Science","Control and Automation, and Energy System Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-26010-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T22:30:10Z","timestamp":1558391410000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/link.springer.com\/10.1007\/978-3-642-26010-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642260094","9783642260100"],"references-count":22,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-642-26010-0_13","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2011]]}}}