{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T13:24:51Z","timestamp":1726406691437},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540564966"},{"type":"electronic","value":"9783540475729"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56496-9_27","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:12:41Z","timestamp":1330254761000},"page":"343-356","source":"Crossref","is-referenced-by-count":6,"title":["Crocos: An integrated environment for interactive verification of SDL specifications"],"prefix":"10.1007","author":[{"given":"Dominique","family":"M\u00e9ry","sequence":"first","affiliation":[]},{"given":"Abdelillah","family":"Mokkedem","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"G. V. Bochmann and C. A. Sunshine. Formal methods in communication protocol design. In IEEE Transactions on Communications, pages 362\u2013372. IEEE, April 1980. COM-28.","DOI":"10.1109\/TCOM.1980.1094685"},{"key":"27_CR2","unstructured":"CCITT. Recommendation z. 100 Specification and Description Language SDL. Note, 1988."},{"key":"27_CR3","unstructured":"K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley Publishing Company, 1988. ISBN 0-201-05866-9."},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E.A Emerson, and A.P Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications: A practical approach. Tenth ACM Symposium on Principles of Programming Languages, pages 117\u2013126, 1983.","DOI":"10.1145\/567067.567080"},{"key":"27_CR5","unstructured":"M. Diaz, J.P. Ansard, J.P Courtiat, P. Azema, and V. Chari, editors. The formal description technique ESTELLE. North-Holland, 1989."},{"key":"27_CR6","unstructured":"E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"R. W. Floyd. Assigning meanings to programs. In J.T. Schwartz, editor, Proc. Symp. Appl. Math. 19, Mathematical Aspects of Computer Science, pages 19\u201332. American Mathematical Society, 1967.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"27_CR8","unstructured":"J. C. Godskesen. An operational Semantic Model for Basic SDL-Extended abstract. In O. Faergemand and R. Reed, editors, Fifth SDL Forum Evolving methods. North-Holland, 1991."},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"E.P. Gribomont. Stepwise refinement and concurrency: The finite-state case. In Jan L.A van de Snepscheut, editor, Science of Computer Programming, Mathematics of Program Construction, volume 14, pages 185\u2013228. North-Holland, October 1990.","DOI":"10.1016\/0167-6423(90)90020-E"},{"key":"27_CR10","unstructured":"C. A. R. Hoare, S. D. Brookes, and A. W. Roscoe. A theory of communicating sequential processes. Technical Report PRG-16, Oxford University Programming Research Group, 1981. Technical Monograph."},{"key":"27_CR11","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. P. Huet","year":"1975","unstructured":"G.P. Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"27_CR12","unstructured":"ISO. Information processing systems, open systems interconnection, est elle (formal description techniques based on an extended state transition model). Technical Report ISO\/IS 9074, ISO, 1988."},{"key":"27_CR13","unstructured":"ISO. Information processing systems \u2014 Open Systems Interconnection \u2014 LOTOS \u2014 A formal description technique based on the temporal ordering of observ ational behaviour, 1989-02-15 edition, 1989. ISO 8807:1989 (E)."},{"key":"27_CR14","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/BF00289062","volume":"14","author":"L. Lamport","year":"1980","unstructured":"L. Lamport. The \u2018Hoare Logic\u2019 of concurrent programs. Acta Informatica, 14:21\u201337, 1980.","journal-title":"Acta Informatica"},{"key":"27_CR15","unstructured":"L. Lamport. What good is temporal logic? pages 657\u2013677. IFIP, 1983."},{"key":"27_CR16","first-page":"200","volume-title":"LNCS 131","author":"Z. Manna","year":"1981","unstructured":"Z. Manna and A. Pnueli. Verification of concurrent programs: temporal proof principles. In Proceedings of the Workshop on Logics of programs, pages 200\u2013252, New York, 1981. Spinger Verlag. LNCS 131."},{"key":"27_CR17","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/0167-6423(84)90003-0","volume":"4","author":"Z. Manna","year":"1984","unstructured":"Z. Manna and A. Pnueli. Adequate proof principles for invariance and liveness properties of concurrent programms. Science of Computer Programming, 4:257\u2013290, december 1984.","journal-title":"Science of Computer Programming"},{"issue":"3","key":"27_CR18","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1051\/ita\/1987210302871","volume":"21","author":"D. M\u00e9ry","year":"1987","unstructured":"D. M\u00e9ry. M\u00e9thode axiomatique pour les propri\u00e9t\u00e9s de fatalit\u00e9 des programmes parall\u00e8les. RAIRO Informatique Th\u00e9orique et Application, 21(3):287\u2013322, 1987.","journal-title":"RAIRO Informatique Th\u00e9orique et Application"},{"key":"27_CR19","unstructured":"D. M\u00e9ry and A. Mokkedem. A proof environment for a subset of SDL. In O. Faergemand and R. Reed, editors, Fifth SDL Forum Evolving methods. North-Holland, 1991."},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"D. M\u00e9ry and A. Mokkedem. CROCOS: An Integrated Environment for Interactive Verification of SDL Specifications. In Participant's Proceedings of the Fourth Workshop on Computer-Aided Verification (CAV '92). Montreal, 1992.","DOI":"10.1007\/3-540-56496-9_27"},{"key":"27_CR21","unstructured":"D. M\u00e9ry, A. Mokkedem, and D. Roegel. Crocos: Un environnement de preuve interactive de specifications SDL. Technical Report 92-r-001, Universit\u00e9 de Nancy I, CRIN, 1991."},{"key":"27_CR22","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6:319\u2013340, 1976.","journal-title":"Acta Informatica"},{"key":"27_CR23","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0743-1066(86)90015-4","volume":"3","author":"L. Paulson","year":"1986","unstructured":"L. Paulson. Natural deduction as higher-order resolution. The Journal of Logic Programming, 3:237\u2013258, 1986.","journal-title":"The Journal of Logic Programming"},{"key":"27_CR24","unstructured":"L. Paulson and T. Nipkow. Isabelle tutorial and users's manual. Technical report, University of Cambridge, Computer Laboratory, 1990."},{"key":"27_CR25","volume-title":"Technical report","author":"G. D. Plotkin","year":"1981","unstructured":"G.D. Plotkin. A structural approach to operational semantics. Technical report, Aarhus University, Denmark, DAIMI, 1981. FN-19."},{"key":"27_CR26","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logics of programs. In Proceedings of 18th Symposium on Foundations of Computer Science, pages 46\u201357. IEEE, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"27_CR27","unstructured":"J.L. Richier, C. Rodriguez, J. Sifakis, and J. Voiron. Xesar A Tool for Protocol Validation. CAP Sogeti Innovation and LGI-IMAG, 1987. Version 1.2."},{"key":"27_CR28","unstructured":"R. Saracco, J. R. W. Smith, and R. Reed. Telecommunications Systems Engineering using SDL. North Holland."},{"key":"27_CR29","unstructured":"SEMA Group. CONCERTO Manuel de R\u00e9f\u00e9rence, July 1990."},{"key":"27_CR30","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1109\/MC.1979.1658889","volume":"12","author":"C. A. Sunshine","year":"1979","unstructured":"C. A. Sunshine. Formal methods for protocol specification and verification. Computer, 12:20\u201327, Sept. 1979.","journal-title":"Computer"},{"issue":"1\u20132","key":"27_CR31","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1\u20132):72\u201399, 1983.","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56496-9_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:04:04Z","timestamp":1605647044000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56496-9_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540564966","9783540475729"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-56496-9_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}