{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T04:52:31Z","timestamp":1755838351987,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642452925"},{"type":"electronic","value":"9783642452932"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-45293-2_5","type":"book-chapter","created":{"date-parts":[[2013,11,25]],"date-time":"2013-11-25T13:47:06Z","timestamp":1385387226000},"page":"62-76","source":"Crossref","is-referenced-by-count":2,"title":["Interrupt Modeling and Verification for Embedded Systems Based on Time Petri Nets"],"prefix":"10.1007","author":[{"given":"Gang","family":"Hou","sequence":"first","affiliation":[]},{"given":"Kuanjiu","family":"Zhou","sequence":"additional","affiliation":[]},{"given":"Junwang","family":"Chang","sequence":"additional","affiliation":[]},{"given":"Rui","family":"Li","sequence":"additional","affiliation":[]},{"given":"Mingchu","family":"Li","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Rammig, F., Rust, C.: Modeling of dynamically modifiable embedded real-time systems. In: Proc. of the Ninth IEEE International Workshop on Object-Oriented Real-Time Dependable Systems, p. 28 (2003)","DOI":"10.1109\/WORDS.2003.1267487"},{"key":"5_CR2","unstructured":"Gu, Z., Shin, K.G.: An Integrated Approach to Modeling and Analysis of Embedded Real-time Systems Based on Timed Petri Nets. In: Proc. of the 23rd International Conference on Distributed Computing Systems, pp. 350\u2013359 (2003)"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Costa, A., Gomes, L.: Petri net Splitting Operation within Embedded Systems Co-design. In: Proc. of 5th IEEE International Conference on Industrial Informatics, pp. 503\u2013508 (2007)","DOI":"10.1109\/INDIN.2007.4384808"},{"key":"5_CR4","first-page":"6","volume":"32","author":"H. Zhang","year":"2006","unstructured":"Zhang, H., Ai, Y.: Schedule Modeling Based on Petri Nets for Distributed Real-time Embedded Systems. Computer Engineering\u00a032, 6\u20138 (2006)","journal-title":"Computer Engineering"},{"key":"5_CR5","series-title":"Mathematical and Engineering Methods in Computer Science","first-page":"1","volume-title":"Rigorous system design: the BIP approach","author":"A. Basu","year":"2012","unstructured":"Basu, A., Bensalem, S., Bozga, M., et al.: Rigorous system design: the BIP approach. Mathematical and Engineering Methods in Computer Science, pp. 1\u201319. Springer, Heidelberg (2012)"},{"key":"5_CR6","unstructured":"Merlin, P.M.: A study of the recoverability of computing systems. Ph.D. dissertation, University of California, Irvine (1974)"},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"1456","DOI":"10.1016\/j.jss.2005.12.021","volume":"79","author":"F. Cassez","year":"2006","unstructured":"Cassez, F., Roux, O.H.: Structural translation from time Petri nets to timed automata. Journal of Systems and Software\u00a079, 1456\u20131468 (2006)","journal-title":"Journal of Systems and Software"},{"key":"5_CR8","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10626-006-8133-9","volume":"16","author":"D. Lime","year":"2006","unstructured":"Lime, D., Roux, O.H.: Model checking of time Petri nets using the state Class timed automaton. Journal of Discrete Event Dynamic Systems\u2014Theory and Applications (DEDS)\u00a016, 179\u2013205 (2006)","journal-title":"Journal of Discrete Event Dynamic Systems\u2014Theory and Applications (DEDS)"},{"key":"5_CR9","first-page":"6","volume":"20","author":"X. Chuanliang","year":"2009","unstructured":"Chuanliang, X.: A Translation Method from Time Petri nets to Timed Automata. Journal of System Simulation\u00a020, 6\u20138 (2009)","journal-title":"Journal of System Simulation"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/3-540-48683-6_3","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1999","unstructured":"Alur, R.: Timed automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 8\u201322. Springer, Heidelberg (1999)"},{"key":"5_CR11","volume-title":"Handbook of Satisfiability","author":"C. Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Handbook of Satisfiability. IOS Press, Fairfax (2009)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-540-68855-6_4","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2008","author":"M. Veanes","year":"2008","unstructured":"Veanes, M., Bj\u00f8rner, N., Raschke, A.: An SMT Approach to Bounded Reachability Analysis of Model Programs. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol.\u00a05048, pp. 53\u201368. Springer, Heidelberg (2008)"},{"key":"5_CR14","first-page":"126","volume":"31","author":"W. Xiaoliang","year":"2010","unstructured":"Xiaoliang, W.: Bounded model checking of timed automata based on Yices. Computer Engineering and Design\u00a031, 126\u2013129 (2010)","journal-title":"Computer Engineering and Design"},{"key":"5_CR15","first-page":"946","volume":"94","author":"K. Weiqiang","year":"2011","unstructured":"Weiqiang, K., Shiraishi, T., Katahira, N., Watanabe, M., Katayama, T., Fukuda, A.: An SMT-based Approach to Bounded Model Checking of Designs in State Transition Matrix. IEICE Transactions on Information and Systems\u00a094, 946\u2013957 (2011)","journal-title":"IEICE Transactions on Information and Systems"},{"key":"5_CR16","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/s10817-006-9026-1","volume":"35","author":"C. Barrett","year":"2005","unstructured":"Barrett, C., Moura, L., Stump, A.: Design and results of the first satisfiability modulo theories competition. Journal of Automated Reasoning\u00a035, 373\u2013390 (2005)","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-540-24605-3_34","volume-title":"Theory and Applications of Satisfiability Testing","author":"D. Berre Le","year":"2004","unstructured":"Le Berre, D., Simon, L.: The essentials of the SAT 2003 competition. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 452\u2013467. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Advanced Parallel Processing Technologies"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-45293-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T23:03:32Z","timestamp":1746054212000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-45293-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642452925","9783642452932"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-45293-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}