{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:08:54Z","timestamp":1725484134045},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439288"},{"type":"electronic","value":"9783540456148"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_19","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:45:28Z","timestamp":1179377128000},"page":"330-349","source":"Crossref","is-referenced-by-count":2,"title":["Interference Analysis for Dependable Systems Using Refinement and Abstraction"],"prefix":"10.1007","author":[{"given":"Claus","family":"Pahl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"19_CR1","unstructured":"IETF PKIX Working Group. Internet X.509 Public Key Infrastructure, 2000. http:\/\/www.ietf.org\/internet-drafts\/draft-ietf-pkix-roadmap-06.txt ."},{"key":"19_CR2","unstructured":"C. Morgan. Programming from Specifications 2e. Addison-Wesley, 1994."},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"R.J.R. Back and J. von Wright. The Refinement Calculus: A Systematic Introduction. Springer-Verlag, 1998.","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Dexter Kozen and Jerzy Tiuryn. Logics of programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol. B, pages 789\u2013840. Elsevier Science Publishers, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50019-6"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol. B, pages 995\u20131072. Elsevier Science Publishers, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"L. Lamport. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3):872\u2013923, May 1994.","DOI":"10.1145\/177492.177726"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"K.M. Chandy and J. Misra. Parallel Program Design. Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"19_CR8","unstructured":"N.A. Durgin and J.C. Mitchell. Analysis of Security Protocols. In M. Broy and R. Steinbruggen, editors, Calculational System Design, pages 369\u2013395. IOS Press, 1999."},{"key":"19_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings 2nd Int. Conference UML\u2019 99-The Unified Modeling Language","author":"G.T. Leavens","year":"1999","unstructured":"G.T. Leavens and A.L. Baker. Enhancing the Pre-and Postcondition Technique for More Expressive Specifications. In R. France and B. Rumpe, editors, Proceedings 2nd Int. Conference UML\u2019 99-The Unified Modeling Language. Springer Verlag, LNCS 1723, 1999."},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Bertrand Meyer. Applying Design by Contract. Computer, pages 40\u201351, October 1992.","DOI":"10.1109\/2.161279"},{"key":"19_CR11","unstructured":"J.B. Warmer and A.G. Kleppe. The Object Constraint Language-Precise Modeling With UML. Addison-Wesley, 1998."},{"key":"19_CR12","volume-title":"Proceedings 2nd International Workshop on Component-Oriented Programming WCOP\u2019 97","author":"M. B\u00fcchi","year":"1997","unstructured":"M. B\u00fcchi and E. Sekerinski. Formal Methods for Component Software: The Refinement Calculus Perspective. In Proceedings 2nd International Workshop on Component-Oriented Programming WCOP\u2019 97. Turku Center for Computer Science, General Publication No.5-97, Turku University, Finland, 1997."},{"key":"19_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Proc. Symposium Formal Methods Europe 2001, Berlin, Germany","author":"C. Pahl","year":"2001","unstructured":"C. Pahl. Components, Contracts and Connectors for the Unified Modelling Language. In Proc. Symposium Formal Methods Europe 2001, Berlin, Germany. Springer-Verlag, LNCS-Series, 2001."},{"key":"19_CR14","unstructured":"B. Mermet and D. M\u00e9ry. Incremental Specification of Telecommunication Services. In M. Hinchey, editor, International Conference on Formal Engineering Methods ICFEM. IEEE Press, 1997."},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"J.-P. Gibson, G. Hamilton, and D. M\u00e9ry. Integration Problems in Telephone Feature Requirements. In A. Galloway and K. Taguchi, editors, Proc. IFM\u201999 Integrated Formal Methods. Springer-Verlag, 1999.","DOI":"10.1007\/978-1-4471-0851-1_8"},{"key":"19_CR16","unstructured":"R. Milner. Communicating and Mobile Systems: the \u03c0-Calculus. Cambridge University Press, 1999."},{"issue":"12","key":"19_CR17","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R.M. Needham","year":"1978","unstructured":"R.M. Needham and M.D. Schroeder. Using Encryption for Authentication in Large Networks of Computers. Communications of the ACM, 21(12):993\u2013999, 1978.","journal-title":"Communications of the ACM"},{"key":"19_CR18","unstructured":"W. Stallings. Cryptography and Network Security. Prentice Hall, 1999."},{"key":"19_CR19","series-title":"Lect Notes Comput Sci","volume-title":"Proc. FME\u20192001 Symposium Formal Methods Europe","author":"B.K. Aichernig","year":"2001","unstructured":"B.K. Aichernig. Test-case calculation through abstraction. In J.N. Oliveira and P. Zave, editors, Proc. FME\u20192001 Symposium Formal Methods Europe. Springer-Verlag, LNCS Series No. 2021, 2001."},{"key":"19_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M. Abadi","year":"1999","unstructured":"M. Abadi and A. Gordon. A Calculus for Cryptographic Protocols: the spi Calculus. Information and Computation, 148:1\u201370, 1999.","journal-title":"Information and Computation"},{"key":"19_CR21","doi-asserted-by":"crossref","unstructured":"L.C. Paulson. Proving Properties of Security Protocols by Induction. In 10th IEEE Computer Security Foundations Workshop, pages 70\u201383. 1997.","DOI":"10.1109\/CSFW.1997.596788"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"D. Dolev and A. Yao. On the Security of Public-key Protocols. IEEE Transactions on Information Theory, 29(2), 1983.","DOI":"10.1109\/TIT.1983.1056650"},{"key":"19_CR23","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","volume":"56","author":"G. Lowe","year":"1995","unstructured":"G. Lowe. An attack on the Needham-Schroeder public-key protocol. Information Processing Letters, 56:131\u2013133, 1995.","journal-title":"Information Processing Letters"},{"key":"19_CR24","unstructured":"R. Focardi, A. Ghelli, and R. Gorrieri. Using non interference for the analysis of security protocols. In H. Orman and C. Meadows, editors, DIMACS Workshop on Design and Formal Verification of Security Protocols. DIMACS, Rutgers University, 1997. http:\/\/dimacs.rutgers.edu\/Workshops\/Security ."},{"key":"19_CR25","unstructured":"M. Butler. On the Use of Data Refinement in the Development of Secure Communications Systems. Technical Report DSSE-TR-2001-1, University of Southampton Declarative Systems and Software Engineering, 2001."},{"key":"19_CR26","unstructured":"I. Zakiuddin, J. Woodcock, M. Goldsmith, and J. Hulance. Formal Verification for Survivable Key Management Systems. In Proc. IEEE Information Survivability Workshop. http:\/\/www.cert.org\/research\/isw\/isw2000\/ , 2000."},{"key":"19_CR27","series-title":"Lect Notes Comput Sci","volume-title":"Proc. FME\u201996 Symposium Formal Methods Europe","author":"J. Peleska","year":"1996","unstructured":"J. Peleska. Test automation for safety-critical systems: Industrial applications and future developments. In M.-C. Gaudel and J. Woodcock, editors, Proc. FME\u201996 Symposium Formal Methods Europe. Springer-Verlag, LNCS Series, 1996."},{"key":"19_CR28","series-title":"Lect Notes Comput Sci","volume-title":"Proc. FME\u201999 Symposium Formal Methods Europe","author":"R. Back","year":"1999","unstructured":"R. Back, A. Mikhajlova, and J. von Wright. Reasoning about interactive systems. In J.M. Wing, J. Woodcock, and J. Davies, editors, Proc. FME\u201999 Symposium Formal Methods Europe. Springer-Verlag, LNCS Series No. 1709, 1999."},{"key":"19_CR29","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1002\/(SICI)1099-1689(199903)9:1<27::AID-STVR172>3.0.CO;2-B","volume":"9","author":"J. Derrick","year":"1999","unstructured":"J. Derrick and E. Boiten. Testing Refinements of State-based Formal Specifications. Software Testing, Verification and Reliability, 9:27\u201350, 1999.","journal-title":"Software Testing, Verification and Reliability"},{"key":"19_CR30","unstructured":"C. Pahl. Analysing Security Properties using Refinement. In Proc. International Workshop on Refinement of Critical Systems RCS\u201902, 2002. (to appear)."},{"key":"19_CR31","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"19_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-49057-4","volume-title":"Proc. 6th Static Analysis Symposium","author":"M. M\u00fcller-Olm","year":"1999","unstructured":"M. M\u00fcller-Olm, D. Schmidt, and B. Steffen. Model Checking-a Tutorial Introduction. In Proc. 6th Static Analysis Symposium. Springer-Verlag, LNCS 1694, 1999."}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T04:05:44Z","timestamp":1556424344000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}