{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:32:16Z","timestamp":1725485536803},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540001416"},{"type":"electronic","value":"9783540361350"}],"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-36135-9_15","type":"book-chapter","created":{"date-parts":[[2007,5,31]],"date-time":"2007-05-31T22:43:21Z","timestamp":1180651401000},"page":"226-242","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Visual Specifications for Modular Reasoning about Asynchronous Systems"],"prefix":"10.1007","author":[{"given":"Nina","family":"Amla","sequence":"first","affiliation":[]},{"given":"E.","family":"Allen Emerson","sequence":"additional","affiliation":[]},{"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[]},{"given":"Richard J.","family":"Trefler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,11,5]]},"reference":[{"key":"15_CR1","unstructured":"N. Amla, E.A. Emerson, R.P. Kurshan, and K.S. Namjoshi. Model checking synchronous timing diagrams. In FMCAD, 2000."},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"N. Amla, E.A. Emerson, R.P. Kurshan, and K.S. Namjoshi. RTDT: a front-end for e.cient model checking of synchronous timing diagrams. In CAV, 2001.","DOI":"10.1007\/3-540-44585-4_38"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"N. Amla, E.A. Emerson, and K.S. Namjoshi. Efficient decompositional model checking for regular timing diagrams. In CHARME, 1999.","DOI":"10.1007\/3-540-48153-2_7"},{"key":"15_CR4","series-title":"Lect Notes Comput Sci","volume-title":"TACAS","author":"N. Amla","year":"2001","unstructured":"N. Amla, E.A. Emerson, K.S. Namjoshi, and R. Trefler. Assumeguarantee based compositional reasoning for synchronous timing diagrams. In TACAS, volume 2031 of LNCS, 2001."},{"key":"15_CR5","unstructured":"N. Amla, E.A. Emerson, K. Namjoshi, and R. Trefler. Compositional Reasoning for Asynchronous Systems, 2002. URL: \n                  http:\/\/-www.cs.bell-labs.com\/who\/kedar\/publications.html\n                  \n                ."},{"key":"15_CR6","unstructured":"R. Alur and R. Grosu. Shared variable interaction diagrams. In 16th IEEE International Conference on Automated Software Engineering, 2001."},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"M. Abadi and L. Lamport. Conjoining specifications. ACM Trans. on Programming Languages and Systems (TOPLAS), May 1995.","DOI":"10.1145\/203095.201069"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"B. Alpern and F. Schneider. Defining liveness. Information Processing Letters, 21(4), 1985.","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"R. Alur and M. Yannakakis. Model checking of message sequence charts. In Proc. TenthInternational Conference on Concurrency Theory, 1999.","DOI":"10.1007\/3-540-48320-9_10"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"W. Damm and D. Harel. LSCs: Breathing life into message sequence charts. Formal Methods in System Design, 19(1), 2001.","DOI":"10.1023\/A:1011227529550"},{"key":"15_CR11","unstructured":"W. Damm, B. Josko, and Rainer Schl\u00f6r. Specification and verification of VHDL-based system-level hardware designs. In Egon Borger, editor, Specification and Validation Methods. Oxford University Press, 1994."},{"key":"15_CR12","unstructured":"W-P. de Roever, F. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods. Cambridge University Press, 2001."},{"key":"15_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Compositionality: The Significant Difference","author":"W.-P. Roever de","year":"1997","unstructured":"W-P. de Roever, H. Langmaack, and A. Pnueli, editors. Compositionality: The Significant Difference, volume 1536 of LNCS. Springer-Verlag, 1997."},{"issue":"3","key":"15_CR14","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E.A. Emerson","year":"1987","unstructured":"E.A. Emerson and C. Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8(3):275\u2013306, 1987.","journal-title":"Science of Computer Programming"},{"key":"15_CR15","unstructured":"K. Fisler. A Unified Approachto Hardware Verification Througha Heterogeneous Logic of Design Diagrams. PhD thesis, Computer Science Department, Indiana University, August 1996."},{"key":"15_CR16","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"R.H. Hardin","year":"1996","unstructured":"R.H. Hardin, Z. Har\u2019el, and R.P. Kurshan. COSPAN. In CAV, volume 1102 of LNCS, 1996."},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"G. Holzmann. The SPIN model checker. IEEE Transactions on Software Engineering, 23(5), May 1997.","DOI":"10.1109\/32.588521"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"G.J. Holzmann and D. Peled. An improvement in formal verification. In FORTE, 1994.","DOI":"10.1007\/978-0-387-34878-0_13"},{"key":"15_CR19","series-title":"Lect Notes Comput Sci","volume-title":"TACAS","author":"J. Klose","year":"2001","unstructured":"J. Klose and H. Wittke. An automata based interpretation of live sequence charts. In TACAS, volume 2031 of LNCS, 2001."},{"key":"15_CR20","unstructured":"P.B. Ladkin and S. Leue. What do message sequence charts mean? In Formal Description Techniques, 1994."},{"key":"15_CR21","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":"15_CR22","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Specification and verification of concurrent programs by forall-automata. In POPL, 1987.","DOI":"10.1145\/41625.41626"},{"key":"15_CR23","unstructured":"A. Muscholl and D. Peled. Analyzing message sequence charts. In 2nd Workshop on SDL and MSC, 2000."},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"A. Muscholl, D. Peled, and Z. Su. Deciding properties for message sequence charts. In FoSSaCS, 1998.","DOI":"10.1007\/BFb0053553"},{"key":"15_CR25","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"K.S. Namjoshi","year":"2000","unstructured":"K.S. Namjoshi and R.J. Trefler. On the completeness of compositional reasoning. In CAV, volume 1855 of LNCS. Springer-Verlag, 2000."},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"M. Plathand M. Ryan. Feature integration using a feature construct. Science of Computer Programming, 41(1), 1999.","DOI":"10.1016\/S0167-6423(00)00018-6"},{"key":"15_CR27","unstructured":"M.H. Smith, G.J. Holzmann, and K. Etessami. Events and constraints: A graphical editor for capturing logic requirements of programs. In 5th International Symposium on Requirements Engineering, 2001."}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Networked and Distributed Sytems \u2014 FORTE 2002"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36135-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T09:27:07Z","timestamp":1558258027000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36135-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001416","9783540361350"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-36135-9_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"5 November 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}