{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:41:16Z","timestamp":1725550876288},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540434771"},{"type":"electronic","value":"9783540460176"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46017-9_8","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:13Z","timestamp":1269897133000},"page":"79-94","source":"Crossref","is-referenced-by-count":5,"title":["Extending the Translation from SDL to Promela"],"prefix":"10.1007","author":[{"given":"Armelle","family":"Prigent","sequence":"first","affiliation":[]},{"given":"Franck","family":"Cassez","sequence":"additional","affiliation":[]},{"given":"Philippe","family":"Dhaussy","sequence":"additional","affiliation":[]},{"given":"Olivier","family":"Roux","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,23]]},"reference":[{"key":"8_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-46419-0_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Bosnacki","year":"2000","unstructured":"Dragan Bosnacki, Dennis Dams, Lesek Holenderski, and Natalia Sidorova. Model checking sdl with spin. In Susanne Graf and Michael Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems,, number 1785, pages 363\u2013377, Berlin, 2000. LNCS, Springer."},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"M. Bozga, J.C. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier, and J. Sifakis. If: An Intermediate Representation for SDL and its Applications. In Proceedings of SDL-FORUM\u201999, Montreal, Canada, June 1999.","DOI":"10.1016\/B978-044450228-5\/50028-X"},{"key":"8_CR3","unstructured":"M. Bozga, L. Ghirvu, S. Graf, L. Mounier, and J. Sifakis. The Intermediate Representation IF: Syntax and semantics. Technical report, V\u00e9rimag, Grenoble, 1999."},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by cons truction or approximation of fixpoints. In ACM Press, editor, Proceedings of the 4th Annual Symposium on Principles of Programming Languages,, 1977.","DOI":"10.1145\/512950.512973"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. In Proceedings of the 19th ACM symposium on principles of programming languages, ACM press, New-York, 1992.","DOI":"10.1145\/143165.143235"},{"issue":"1\u20132","key":"8_CR6","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/0304-3975(94)00136-7","volume":"146","author":"F. Cassez","year":"1995","unstructured":"Franck Cassez and Olivier Roux. Compilation of the ELECTRE reactive language into finite transition systems. Theoretical Computer Science, 146(1\u20132):109\u2013143, July 1995.","journal-title":"Theoretical Computer Science"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"G.J. Holzmann. The model checker spin. In IEEE Trans. on Software Engineering, volume 23, May 1997.","DOI":"10.1109\/32.588521"},{"key":"8_CR8","unstructured":"ITU-T International Telecommunication Union. Annex F.3 to Recommendation Z.100, Specification and Description Language (SDL)-SDL Formal Definition: Dynamic Semantics. 1994."},{"key":"8_CR9","unstructured":"ITU-T International Telecommunication Union. Recommendation Z.100, Specification and Description Language (SDL). 1994."},{"key":"8_CR10","series-title":"Lect Notes Comput Sci","first-page":"106","volume-title":"Effective recognizability and model checking of reactive fiffo automata","author":"G. Sutre","year":"1999","unstructured":"G. Sutre, A. Finkel, O. Roux, and F. Cassez. Effective recognizability and model checking of reactive fiffo automata. In Proc. 7th Int. Conf. Algebraic Methodology and Software Technology (AMAST\u201998),Amazonia, Brazil, Jan. 1999, volume 1548 of Lecture Notes in Computer Science, pages 106\u2013123. Springer, 1999."},{"key":"8_CR11","unstructured":"TELELOGIC. TAU\/SDT 3.3. TELELOGIC, June 1998."},{"key":"8_CR12","unstructured":"VERILOG. ObjectGEODE 4.0. CS VERILOG, March 1999."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46017-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,24]],"date-time":"2019-02-24T13:36:00Z","timestamp":1551015360000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46017-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434771","9783540460176"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-46017-9_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}