{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:38:57Z","timestamp":1725496737875},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540412199"},{"type":"electronic","value":"9783540409229"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-40922-x_18","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T04:41:36Z","timestamp":1196311296000},"page":"320-335","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Model Checking Synchronous Timing Diagrams"],"prefix":"10.1007","author":[{"given":"Nina","family":"Amla","sequence":"first","affiliation":[]},{"given":"E. Allen","family":"Emerson","sequence":"additional","affiliation":[]},{"given":"Robert P.","family":"Kurshan","sequence":"additional","affiliation":[]},{"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,6,18]]},"reference":[{"key":"18_CR1","unstructured":"N. Amla and E.A. Emerson. Regular Timing Diagrams. In LICS Workshop on Logic and Diagrammatic Information, June 1998."},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"N. Amla, E.A. Emerson, and K.S. Namjoshi. Efficient Decompositional Model Checking for Regular Timing Diagrams. In CHARME. Springer-Verlag, September 1999.","DOI":"10.1007\/3-540-48153-2_7"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"T. Amon, G. Borriello, T. Hu, and J. Liu. Symbolic Timing Verification of Timing Diagrams Using Presburger Formulas. In DAC, 1997.","DOI":"10.1145\/266021.266071"},{"key":"18_CR4","unstructured":"Bell Laboratories, Lucent Technologies. PCI Core User\u2019s Manual (Version 1.0). Technical report, July 1996."},{"key":"18_CR5","unstructured":"A. Benveniste. Safety Critical Embedded Systems Design: the SACRES approach. Technical report, INRIA, May 1998. URL: \n                    http:\/\/www.tni.fr\/sacres\/index.html"},{"key":"18_CR6","unstructured":"R. Brayton, G. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. Ranjan, S. Sarwary, T. Shiple, G. Swamy, and T. Villa. VIS. In FMCAD, 1996."},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"U. Brockmeyer and G. Wittich. Tamagotchis need not die-Veri.cation of STATEMATE Designs. In TACAS. Springer-Verlag, March 1998.","DOI":"10.1007\/BFb0054174"},{"key":"18_CR8","unstructured":"E. M. Clarke and E. A. Emerson. Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. In Workshop on Logics of Programs, volume 131. Springer Verlag, 1981."},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic Verification of Finite-State Concurrent Systems using Temporal Logic. ACM Transactions on Programming Languages and Systems, 8(2), 1986.","DOI":"10.1145\/5397.5399"},{"key":"18_CR10","unstructured":"W. Damm, B. Josko, and Rainer Schl\u00f6r. Specification and Verification of VHDLbased System-level Hardware Designs. In Egon Borger, editor, Specification and Validation Methods. Oxford University Press, 1994."},{"key":"18_CR11","unstructured":"K. Fisler. A Unified Approach to Hardware Verification Through a Heterogeneous Logic of Design Diagrams. PhD thesis, Computer Science Department, Indiana University, August 1996."},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"K. Fisler. Containment of Regular Languages in Non-Regular Timing Diagrams Languages is Decidable. In CAV. Springer Verlag, 1997.","DOI":"10.1007\/3-540-63166-6_17"},{"key":"18_CR13","unstructured":"W. Grass, C. Grobe, S. Lenk, W. Tiedemann, C.D. Kloos, A. Marin, and T. Robles. Transformation of Timing Diagram Speci.cations into VHDL Code. In Conference on Hardware Description Languages, 1995."},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"R.H. Hardin, Z. Har'El, and R.P. Kurshan. COSPAN. In CAV, volume 1102, 1996.","DOI":"10.1007\/3-540-61474-5_94"},{"key":"18_CR15","unstructured":"K. Kastein and M. McClure. Timing Designer use for Interface Verification at Symbios Logic. Integrated System Design, May 1997. URL: \n                    http:\/\/www.chronology.com"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"K. Khordoc and E. Cerny. Semantics and Verification of Timing Diagrams with Linear Timing Constraints. ACM Transactions on Design Automation of Electronic Systems, 3(1), 1998.","DOI":"10.1145\/270580.270582"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan. Computer-aided verification of coordinating processes: the Automata-theoretic approach. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that Finite State Concurrent Programs satisfy their Linear Specifications. In POPL, 1985.","DOI":"10.1145\/318593.318622"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"K. Luth. The ICOS Synthesis Environment. In Formal Techniques in Real-Time and Fault-Tolerant Systems, 1998. au]20._Z. Manna and A. Pnueli. Speci.cation and Veri.cation of Concurrent Programs by \u2228-Automata. In POPL, 1987.","DOI":"10.1007\/BFb0055356"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Press, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"18_CR21","unstructured":"D. Mitchell. Test Bench Generation from Timing Diagrams. In David Pellerin, editor, VHDL Made Easy. 1996. URL: \n                    http:\/\/www.syncad.com"},{"key":"18_CR22","unstructured":"PCI Special Interest Group. PCI Local Bus Speci.cation Rev 2.1. Technical report, June 1995."},{"key":"18_CR23","series-title":"Lect Notes Comput Sci","volume-title":"Specification and Verification of Concurrent Systems in CESAR","author":"J.P. Queille","year":"1982","unstructured":"J.P. Queille and J. Sifakis. Specification and Verification of Concurrent Systems in CESAR. In Proc. of the 5th International Symposium on Programming, volume 137 of LNCS, 1982."},{"key":"18_CR24","unstructured":"M. Vardi. Verification of Concurrent Programs. In POPL, 1987."},{"key":"18_CR25","unstructured":"M. Vardi and P. Wolper. An Automata-theoretic Approach to Automatic Program Verification. In LICS, 1986."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40922-X_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,30]],"date-time":"2020-01-30T10:30:51Z","timestamp":1580380251000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40922-X_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540412199","9783540409229"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-40922-x_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"18 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}