{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:38:28Z","timestamp":1742913508014,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319478456"},{"type":"electronic","value":"9783319478463"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47846-3_6","type":"book-chapter","created":{"date-parts":[[2016,10,14]],"date-time":"2016-10-14T02:53:57Z","timestamp":1476413637000},"page":"74-89","source":"Crossref","is-referenced-by-count":0,"title":["A Case Study of Formal Approach to Dynamically Reconfigurable Systems by Using Dynamic Linear Hybrid Automata"],"prefix":"10.1007","author":[{"given":"Ryo","family":"Yanase","sequence":"first","affiliation":[]},{"given":"Tatsunori","family":"Sakai","sequence":"additional","affiliation":[]},{"given":"Makoto","family":"Sakai","sequence":"additional","affiliation":[]},{"given":"Satoshi","family":"Yamane","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,15]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 138, 3\u201334 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 209\u2013229. Springer, Heidelberg (1993)"},{"key":"6_CR3","unstructured":"Amano, H., Adachi, Y., Tsutsumi, S., Ishikawa, K.: A context dependent clock control mechanism for dynamically reconfigurable processors. Technical report of IEICE, vol. 104, no. 589, pp. 13\u201316 (2005)"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Attie, P.C., Lynch, N.A.: Dynamic input\/output automata, a formal model for dynamic systems. In: Proceedings of the Twentieth Annual ACM Symposium on Principles of Distributed Computing, PODC 2001, pp. 314\u2013316 (2001)","DOI":"10.1145\/383962.384051"},{"issue":"1\u20132","key":"6_CR5","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1\u20132), 3\u201321 (2008)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"6_CR6","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1023\/A:1008719024240","volume":"14","author":"B Boigelot","year":"1999","unstructured":"Boigelot, B., Godefroid, P.: Symbolic verification of communication protocols with infinite state spaces using QDDs. Form. Methods Syst. Des. 14(3), 237\u2013255 (1999)","journal-title":"Form. Methods Syst. Des."},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/BFb0032741","volume-title":"Static Analysis","author":"B Boigelot","year":"1997","unstructured":"Boigelot, B., Godefroid, P., Willems, B., Wolper, P.: The power of QDDs (extended abstract). In: Hentenryck, P. (ed.) SAS 1997. LNCS, vol. 1302, pp. 172\u2013186. Springer, Heidelberg (1997). doi: 10.1007\/BFb0032741"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1007\/3-540-63165-8_211","volume-title":"Automata, Languages and Programming","author":"A Bouajjani","year":"1997","unstructured":"Bouajjani, A., Habermehl, P.: Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 560\u2013570. Springer, Heidelberg (1997)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"issue":"1","key":"6_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1155\/ES\/2006\/56320","volume":"2006","author":"P Garcia","year":"2006","unstructured":"Garcia, P., Compton, K., Schulte, M., Blem, E., Fu, W.: An overview of reconfigurable hardware in embedded systems. EURASIP J. Embed. Syst. 2006(1), 1\u201319 (2006)","journal-title":"EURASIP J. Embed. Syst."},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HyTech: a model checker for hybrid. Softw. Tools Technol. Transf. 1(Cav 97), 110\u2013122 (1997)","DOI":"10.1007\/s100090050008"},{"key":"6_CR13","unstructured":"Lockwood, J.W., Moscola, J., Kulig, M., Reddick, D., Brooks, T.: Internet worm and virus protection in dynamically reconfigurable hardware. In: Military and Aerospace Programmable Logic Device (MAPLD), p. E10 (2003)"},{"issue":"1","key":"6_CR14","first-page":"190","volume":"28","author":"S Minami","year":"2011","unstructured":"Minami, S., Takinai, S., Sekoguchi, S., Nakai, Y., Yamane, S.: Modeling, specification and model checking of dynamically reconfigurable processors. Comput. Softw. 28(1), 190\u2013216 (2011). Japan Society for Software Science and Technology","journal-title":"Comput. Softw."},{"issue":"11","key":"6_CR15","first-page":"1259","volume":"46","author":"M Motomura","year":"2005","unstructured":"Motomura, M., Fujii, T., Furuta, K., Anjo, K., Yabe, Y., Togawa, K., Yamada, J., Izawa, Y., Sasaki, R.: New generation microprocessor architecture (2): dynamically reconfigurable processor (DRP). IPSJ Mag. 46(11), 1259\u20131265 (2005)","journal-title":"IPSJ Mag."},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-540-32275-7_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and abstract DPLL modulo theories. In: Baader, F., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3452, pp. 36\u201350. Springer, Heidelberg (2005). doi: 10.1007\/978-3-540-32275-7_3"},{"issue":"20","key":"6_CR17","first-page":"55","volume":"111","author":"Y Ono","year":"2011","unstructured":"Ono, Y., Yamane, S.: Computation of quantifier elimination of linear inequalities of first order predicate logic. COMP Comput. 111(20), 55\u201359 (2011). IEICE Technical report","journal-title":"COMP Comput."},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/3-540-36190-1_3","volume-title":"Concurrency and Hardware Design","author":"V Varshavsky","year":"2002","unstructured":"Varshavsky, V., Marakhovsky, V.: GALA (Globally Asynchronous - Locally Arbitrary) design. In: Cortadella, J., Yakovlev, A., Rozenberg, G. (eds.) Concurrency and Hardware Design. LNCS, vol. 2549, pp. 61\u2013107. Springer, Heidelberg (2002)"},{"issue":"3","key":"6_CR19","first-page":"1","volume":"6","author":"H Yamada","year":"2013","unstructured":"Yamada, H., Nakai, Y., Yamane, S.: Proposal of specification language and verification experiment for dynamically reconfigurable system. J. Inf. Process. Soc. Jpn. Program. 6(3), 1\u201319 (2013)","journal-title":"J. Inf. Process. Soc. Jpn. Program."}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47846-3_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T11:53:30Z","timestamp":1568462010000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47846-3_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319478456","9783319478463"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47846-3_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}