{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T09:31:48Z","timestamp":1725874308760},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319510453"},{"type":"electronic","value":"9783319510460"}],"license":[{"start":{"date-parts":[[2016,12,18]],"date-time":"2016-12-18T00:00:00Z","timestamp":1482019200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-51046-0_4","type":"book-chapter","created":{"date-parts":[[2016,12,17]],"date-time":"2016-12-17T07:05:53Z","timestamp":1481958353000},"page":"65-87","source":"Crossref","is-referenced-by-count":3,"title":["FDR: From Theory to Industrial Application"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Gibson-Robinson","sequence":"first","affiliation":[]},{"given":"Guy","family":"Broadfoot","sequence":"additional","affiliation":[]},{"given":"Gustavo","family":"Carvalho","sequence":"additional","affiliation":[]},{"given":"Philippa","family":"Hopcroft","sequence":"additional","affiliation":[]},{"given":"Gavin","family":"Lowe","sequence":"additional","affiliation":[]},{"given":"Sidney","family":"Nogueira","sequence":"additional","affiliation":[]},{"given":"Colin","family":"O\u2019Halloran","sequence":"additional","affiliation":[]},{"given":"Augusto","family":"Sampaio","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,12,18]]},"reference":[{"key":"4_CR1","unstructured":"Unmanned Safe Maritime Operations Over The Horizon (USMOOTH) (2015). http:\/\/gtr.rcuk.ac.uk\/projects?ref=102303"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Arruda, F., Sampaio, A., Barros, F.: Capture and replay with text-based reuse and framework agnosticism. In: Software Engineering and Knowledge Engineering (2016)","DOI":"10.18293\/SEKE2016-228"},{"key":"4_CR3","unstructured":"Broadfoot, G.H.: Using CSP to support the cleanroom development method for software development. MSc Thesis, University of Oxford (2001)"},{"issue":"3,4","key":"4_CR4","doi-asserted-by":"crossref","first-page":"379","DOI":"10.3233\/JCS-2004-123-404","volume":"12","author":"PJ Broadfoot","year":"2004","unstructured":"Broadfoot, P.J., Roscoe, A.W.: Embedding agents within the intruder to detect parallel attacks. J. Comput. Secur. 12(3,4), 379\u2013408 (2004)","journal-title":"J. Comput. Secur."},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Carvalho, G., Barros, F.A., Carvalho, A., Cavalcanti, A., Mota, A., Sampaio, A., NAT2TEST tool: From natural language requirements to test cases based on CSP. In: Software Engineering and Formal Methods (2015)","DOI":"10.1007\/978-3-319-22969-0_20"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Carvalho, G., Sampaio, A., Mota, A.: A CSP timed input-output relation and a strategy for mechanised conformance verification. In: ICFEM (2013)","DOI":"10.1007\/978-3-642-41202-8_11"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Cavalcanti, A., Hierons, R.M., Nogueira, S., Sampaio, A.: A suspension-trace semantics for CSP. In: Theoretical Aspects of Software Engineering (2016)","DOI":"10.1109\/TASE.2016.9"},{"issue":"6","key":"4_CR8","doi-asserted-by":"crossref","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Creese, S., Goldsmith, M., Harrison, R., Roscoe, A.W., Whittaker, P., Zakiuddin, I.: Exploiting empirical engagement in authentication protocol design. In: Security in Pervasive Computing (2005)","DOI":"10.1007\/978-3-540-32004-3_14"},{"key":"4_CR10","unstructured":"de Jongh, H.: Brabantse vinding verslaat Indiase softwaremakers. http:\/\/fd.nl\/entrepreneur\/wereldveroveraars\/634621-1211\/brabantse-vinding-verslaat-indiase-softwaremakers"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Dilloway, C., Lowe, G.: Specifying secure transport layers. In: CSFW (2008)","DOI":"10.1109\/CSF.2008.14"},{"key":"4_CR12","unstructured":"Formal Systems (Europe) Limited (2013)"},{"issue":"2","key":"4_CR13","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/s10009-015-0377-y","volume":"18","author":"T Gibson-Robinson","year":"2016","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3: a parallel refinement checker for CSP. Int. J. Softw. Tools Technol. Transf. 18(2), 149\u2013167 (2016)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Osaiweran, A., Wesselius, J.H.: Analyzing the effects of formal methods on the development of industrial control software. In: ICSM (2011)","DOI":"10.1109\/ICSM.2011.6081983"},{"key":"4_CR15","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall Inc., Upper Saddle River (1985)"},{"issue":"6","key":"4_CR16","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/j.entcs.2005.04.008","volume":"128","author":"PJ Hopcroft","year":"2005","unstructured":"Hopcroft, P.J., Broadfoot, G.H.: Combining the box structure development method and CSP. Electron. Notes Theoret. Comput. Sci. 128(6), 127\u2013144 (2005)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: TACAS (1996)","DOI":"10.1007\/3-540-61042-1_43"},{"issue":"1\u20132","key":"4_CR18","doi-asserted-by":"crossref","first-page":"53","DOI":"10.3233\/JCS-1998-61-204","volume":"6","author":"G Lowe","year":"1998","unstructured":"Lowe, G.: Casper: a compiler for the analysis of security protocols. J. Comput. Secur. 6(1\u20132), 53\u201384 (1998)","journal-title":"J. Comput. Secur."},{"key":"4_CR19","volume-title":"Principles of Information Systems Analysis and Design","author":"HD Mills","year":"1986","unstructured":"Mills, H.D., Linger, R.C., Hevner, A.R.: Principles of Information Systems Analysis and Design. Academic Press, New York (1986)"},{"issue":"12","key":"4_CR20","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R Needham","year":"1978","unstructured":"Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993\u2013999 (1978)","journal-title":"Commun. ACM"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Nogueira, S., Sampaio, A., Mota, A.: Test generation from state based use case models. Formal Aspects of Comput. (2014)","DOI":"10.1007\/s00165-012-0258-z"},{"key":"4_CR22","unstructured":"O\u2019Halloran, C.: A calculus of information flow. In: ESORICS (1990)"},{"key":"4_CR23","unstructured":"O\u2019Halloran, C.: Category theory and information flow applied to computer security. DPhil Thesis, University of Oxford (1993)"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"O\u2019Halloran, C.: Assessing Safety Critical COTS Systems (1999)","DOI":"10.1007\/978-1-4471-0823-8_5"},{"issue":"3","key":"4_CR25","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1002\/(SICI)1097-024X(199803)28:3<329::AID-SPE157>3.0.CO;2-H","volume":"28","author":"SJ Prowell","year":"1998","unstructured":"Prowell, S.J., Poore, J.H.: Sequence-based software specification of deterministic systems. Softw. Practi. Experience 28(3), 329\u2013344 (1998)","journal-title":"Softw. Practi. Experience"},{"key":"4_CR26","unstructured":"REF 2014. Automated software design and verification. http:\/\/impact.ref.ac.uk\/CaseStudies\/CaseStudy.aspx?Id=4907"},{"key":"4_CR27","unstructured":"Roscoe, A.W.: Model-checking CSP. In: A Classical Mind, pp. 353\u2013378. Prentice Hall International (UK) Ltd., Hertfordshire (1994)"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W.: Modelling and verifying key-exchange protocols using CSP and FDR. In: CSFW (1995)","DOI":"10.1109\/CSFW.1995.518556"},{"key":"4_CR29","volume-title":"The Theory and Practice of Concurrency","author":"AW Roscoe","year":"1997","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Englewood Cliffs (1997)"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W.: CSP is expressive enough for $$\\pi $$ . In: Reflections on the Work of CAR Hoare (2010)","DOI":"10.1007\/978-1-84882-912-1"},{"key":"4_CR31","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding Concurrent Systems","author":"AW Roscoe","year":"2010","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Springer, Heidelberg (2010)"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W., Broadfoot, P.J.: Proving security protocols with model checkers by data independence techniques. J. Comput. Secur. (1999)","DOI":"10.3233\/JCS-1999-72-303"},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M.H., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or how to check $$10^{20}$$ dining philosophers for deadlock. In: TACAS (1995)","DOI":"10.1007\/3-540-60630-0_7"},{"key":"4_CR34","unstructured":"Roscoe, A.W., Goldsmith, M.: The perfect spy for model-checking crypto-protocols. In: DIMACS (1997)"},{"key":"4_CR35","unstructured":"Roscoe, A.W., Goldsmith, M.H., Cox, A.D.B., Scattergood, J.B.: Formal Methods in the Development of the H1 Transputer. In: WOTUG (1991)"},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W., Hopcroft, P.J.: Theories of programming and formal methods. Chapter Slow Abstraction via Priority (2013)","DOI":"10.1007\/978-3-642-39698-4_20"},{"issue":"4","key":"4_CR37","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1002\/stvr.1498","volume":"24","author":"A Sampaio","year":"2014","unstructured":"Sampaio, A., Nogueira, S., Mota, A., Isobe, Y.: Sound and mechanised compositional verification of input-output conformance. Softw. Testing Verification Reliab. 24(4), 289\u2013319 (2014)","journal-title":"Softw. Testing Verification Reliab."},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"Tretmans, J.: Test Generation with Inputs, Outputs, and Quiescence. In: TACAS (1996)","DOI":"10.1007\/3-540-61042-1_42"},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"Tudor, N.J., Botham, J.: Proving properties of automotive systems of systems under ISO 26262 using automated formal methods. In: System Safety and Cyber Security (2014)","DOI":"10.1049\/cp.2014.0964"},{"key":"4_CR40","unstructured":"Zakiuddin, I., Moffat, N., O\u2019Halloran, C., Ryan, P.: Chasing events to certify a critical system. Technical report (1998)"}],"container-title":["Lecture Notes in Computer Science","Concurrency, Security, and Puzzles"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-51046-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,16]],"date-time":"2019-09-16T12:59:58Z","timestamp":1568638798000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-51046-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,18]]},"ISBN":["9783319510453","9783319510460"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-51046-0_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016,12,18]]}}}