{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,2]],"date-time":"2025-03-02T05:51:09Z","timestamp":1740894669522,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540236108"},{"type":"electronic","value":"9783540304760"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30476-0_35","type":"book-chapter","created":{"date-parts":[[2011,1,12]],"date-time":"2011-01-12T17:51:35Z","timestamp":1294854695000},"page":"426-440","source":"Crossref","is-referenced-by-count":8,"title":["Verification of Analog and Mixed-Signal Circuits Using Timed Hybrid Petri Nets"],"prefix":"10.1007","author":[{"given":"Scott","family":"Little","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Walter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicholas","family":"Seegmiller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chris","family":"Myers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tomohiro","family":"Yoneda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"35_CR1","doi-asserted-by":"crossref","unstructured":"Hedrich, L., Barke, E.: A formal approach to nonlinear analog circuit verification. In: International Conference on Computer-Aided Design, pp. 123\u2013127 (1995)","DOI":"10.1109\/ICCAD.1995.480002"},{"key":"35_CR2","doi-asserted-by":"crossref","unstructured":"Hendricx, S., Claesen, L.: A symbolic core approach to the formal verification of integrated mixed-mode applications. In: European Design and Test Conference, pp. 432\u2013436 (1997)","DOI":"10.1109\/EDTC.1997.582396"},{"key":"35_CR3","doi-asserted-by":"crossref","unstructured":"Hedrich, L., Barke, E.: A formal approach to verification of linear analog circuits with parameter tolerances. In: Design, Automation and Test in Europe Proceedings, pp. 649\u2013654 (1998)","DOI":"10.1109\/DATE.1998.655927"},{"key":"35_CR4","doi-asserted-by":"crossref","unstructured":"Ghosh, A., Vemuri, R.: Formal verification of synthesized analog designs. In: International Conference on Computer Design, pp. 40\u201345 (1999)","DOI":"10.1109\/ICCD.1999.808362"},{"key":"35_CR5","doi-asserted-by":"crossref","unstructured":"Salem, A.: Semi-formal verification of VHDL-AMS descriptions. In: International Symposium on Circuits and Systems, pp. 123\u2013127 (2002)","DOI":"10.1109\/ISCAS.2002.1010708"},{"key":"35_CR6","doi-asserted-by":"crossref","unstructured":"Hartong, W., Hedrich, L., Barke, E.: Model checking algorithms for analog verification. In: Design Automation Conference, pp. 542\u2013547 (2002)","DOI":"10.1145\/514053.514055"},{"key":"35_CR7","doi-asserted-by":"crossref","unstructured":"Hartong, W., Hedrich, L., Barke, E.: On discrete modeling and model checking for nonlinear analog systems. In: Computer Aided Verification. 14th International Conference, pp. 401\u2013413 (2002)","DOI":"10.1007\/3-540-45657-0_33"},{"key":"35_CR8","unstructured":"Gupta, S., Krogh, B.H., Rutenbar, R.A.: Towards formal verification of analog and mixed-signal designs. In: TECHCON 2003 (2003)"},{"key":"35_CR9","doi-asserted-by":"crossref","unstructured":"Yoneda, T., Schlingloff, B.: Efficient verification of parallel real-time systems. Formal Methods in System Design (1997)","DOI":"10.1023\/A:1008682131325"},{"key":"35_CR10","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1109\/43.845076","volume":"19","author":"W. Belluomini","year":"2000","unstructured":"Belluomini, W., Myers, C.J.: Timed state space exploration using posets. IEEE Transactions on Computer-Aided Design\u00a019, 501\u2013520 (2000)","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"35_CR11","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, 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"key":"35_CR12","doi-asserted-by":"crossref","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: Hybrid Systems, pp. 209\u2013229 (1992)","DOI":"10.1007\/3-540-57318-6_30"},{"key":"35_CR13","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, 181\u2013201 (1996)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"35_CR14","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. International Journal on Software Tools for Technology Transfer\u00a01, 110\u2013122 (1997)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"35_CR15","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1023\/A:1008395301582","volume":"11","author":"H. Chen","year":"2001","unstructured":"Chen, H., Hanisch, H.M.: Analysis of hybrid systems based on hybrid net condition\/ event system model. Discrete Event Dynamic Systems: Theory and Applications\u00a011, 163\u2013185 (2001)","journal-title":"Discrete Event Dynamic Systems: Theory and Applications"},{"key":"35_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/3-540-46430-1_6","volume-title":"Hybrid Systems: Computation and Control","author":"E. Asarin","year":"2000","unstructured":"Asarin, E., Bournez, O., Dang, T., Maler, O.: Approximate reachability analysis of piecewise-linear dynamical systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol.\u00a01790, p. 20. Springer, Heidelberg (2000)"},{"key":"35_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/3-540-36580-X_37","volume-title":"Hybrid Systems: Computation and Control","author":"A. Tiwari","year":"2003","unstructured":"Tiwari, A.: Approximate reachability for linear systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol.\u00a02623, pp. 514\u2013525. Springer, Heidelberg (2003)"},{"key":"35_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-45069-6_19","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"2003","unstructured":"Boigelot, B., Herbreteau, F., Jodogne, S.: Hybrid acceleration using real vector automata (extended abstract). In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 193\u2013205. Springer, Heidelberg (2003)"},{"key":"35_CR19","first-page":"2867","volume-title":"Proceedings of the 40th IEEE Conference on Decision and Control","author":"B. Silva","year":"2003","unstructured":"Silva, B., Stursberg, O., Krogh, B., Engell, S.: An assessment of the current status of algorithmic approaches to the verification of hybrid systems. In: Proceedings of the 40th IEEE Conference on Decision and Control, vol.\u00a03, pp. 2867\u20132874. IEEE Press, Los Alamitos (2003)"},{"key":"35_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? In: Proc. 27th Annual ACM Symp. on Theory of Computing, pp. 373\u2013382 (1995)","DOI":"10.1145\/225058.225162"},{"key":"35_CR21","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1109\/70.864231","volume":"16","author":"F. Balduzzi","year":"2000","unstructured":"Balduzzi, F., Giua, A., Menga, G.: First-order hybrid petri nets: A model for optimization and control. IEEE Transactions on Robotics and Automation\u00a016, 382\u2013399 (2000)","journal-title":"IEEE Transactions on Robotics and Automation"},{"key":"35_CR22","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1023\/A:1008330914786","volume":"11","author":"R. David","year":"2001","unstructured":"David, R., Alla, H.: On hybrid petri nets. Discrete Event Dynamic Systems: Theory and Applications\u00a011, 9\u201340 (2001)","journal-title":"Discrete Event Dynamic Systems: Theory and Applications"},{"key":"35_CR23","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1023\/A:1008387132533","volume":"11","author":"B. Tuffin","year":"2001","unstructured":"Tuffin, B., Chen, D.S., Trivedi, K.S.: Comparison of hybrid systems and fluid stochastic petri nets. Discrete Event Dynamic Systems: Theory and Applications\u00a011, 77\u201395 (2001)","journal-title":"Discrete Event Dynamic Systems: Theory and Applications"},{"key":"35_CR24","doi-asserted-by":"crossref","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Proceedings of the Workshop on Automatic Verification Methods for Finite- State Systems (1989)","DOI":"10.1007\/3-540-52148-8_17"},{"key":"35_CR25","doi-asserted-by":"crossref","unstructured":"Myers, C.J., Belluomini, W., Killpack, K., Mercer, E., Peskin, E., Zheng, H.: Timed circuits: A new paradigm for high-speed design. In: Proc. of Asia and South Pacific Design Automation Conference, 335\u2013340 (2001)","DOI":"10.1145\/370155.370379"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30476-0_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T17:14:25Z","timestamp":1740849265000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30476-0_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540236108","9783540304760"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30476-0_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}