{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T09:49:06Z","timestamp":1742982546050,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031770180"},{"type":"electronic","value":"9783031770197"}],"license":[{"start":{"date-parts":[[2024,11,22]],"date-time":"2024-11-22T00:00:00Z","timestamp":1732233600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,22]],"date-time":"2024-11-22T00:00:00Z","timestamp":1732233600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-77019-7_16","type":"book-chapter","created":{"date-parts":[[2024,11,21]],"date-time":"2024-11-21T20:47:03Z","timestamp":1732222023000},"page":"272-289","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Theory of\u00a0Proc-Omata\u2014and\u00a0Proof Methods for\u00a0Process Architectures"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-4941-187X","authenticated-orcid":false,"given":"Beno\u00eet","family":"Ballenghien","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9648-7663","authenticated-orcid":false,"given":"Burkhart","family":"Wolff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,22]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","first-page":"1386","DOI":"10.4028\/www.scientific.net\/AMR.915-916.1386","volume":"915\u2013916","author":"J An","year":"2014","unstructured":"An, J., Zhang, L., You, C.: The design and implementation of data independence in the CSP model of security protocol. Adv. Mater. Res. 915\u2013916, 1386\u20131392 (2014). https:\/\/doi.org\/10.4028\/www.scientific.net\/AMR.915-916.1386","journal-title":"Adv. Mater. Res."},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-57288-8_3","volume-title":"NASA Formal Methods","author":"\u00c9 Andr\u00e9","year":"2017","unstructured":"Andr\u00e9, \u00c9., Nguyen, H.G., Petrucci, L., Sun, J.: Parametric model checking timed automata under non-zenoness assumption. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 35\u201351. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_3"},{"key":"16_CR3","unstructured":"Ballenghien, B., Taha, S., Wolff, B.: HOL-CSPM - architectural operators for HOL-CSP. Arch. Formal Proofs 2023 (2023). https:\/\/www.isa-afp.org\/entries\/HOL-CSPM.html"},{"key":"16_CR4","unstructured":"Ballenghien, B., Wolff, B.: An operational semantics in Isabelle\/HOL-CSP. In: Bertot, Y., Kutsia, T., Norrish, M. (eds.) 15th International Conference on Interactive Theorem Proving, ITP 2024. LIPIcs, vol.\u00a0309, pp. 29:1\u201329:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2023.29"},{"key":"16_CR5","doi-asserted-by":"publisher","unstructured":"Ballenghien, B., Wolff, B.: An operational semantics in Isabelle\/HOL-CSP. In: Bertot, Y., Kutsia, T., Norrish, M. (eds.) 15th International Conference on Interactive Theorem Proving, ITP 2024, 9\u201314 September 2024, Tbilisi, Georgia. LIPIcs, vol.\u00a0309, pp. 7:1\u20137:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2024.7","DOI":"10.4230\/LIPICS.ITP.2024.7"},{"key":"16_CR6","unstructured":"Ballenghien, B., Wolff, B.: Operational semantics formally proven in HOL-CSP. Archive of Formal Proofs (2023). https:\/\/isa-afp.org\/entries\/HOL-CSP_OpSem.html"},{"issue":"3","key":"16_CR7","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"SD Brookes","year":"1984","unstructured":"Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560\u2013599 (1984)","journal-title":"J. ACM"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/3-540-15670-4_14","volume-title":"Seminar on Concurrency","author":"SD Brookes","year":"1985","unstructured":"Brookes, S.D., Roscoe, A.W.: An improved failures model for communicating processes. In: Brookes, S.D., Roscoe, A.W., Winskel, G. (eds.) CONCURRENCY 1984. LNCS, vol. 197, pp. 281\u2013305. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/3-540-15670-4_14"},{"key":"16_CR9","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-1-4471-3182-3_9","volume-title":"IV Higher Order Workshop, Banff 1990","author":"AJ Camilleri","year":"1991","unstructured":"Camilleri, A.J.: A higher order logic mechanization of the CSP failure-divergence semantics. In: Birtwistle, G. (ed.) IV Higher Order Workshop, Banff 1990, pp. 123\u2013150. Springer, London (1991). https:\/\/doi.org\/10.1007\/978-1-4471-3182-3_9"},{"issue":"4","key":"16_CR10","doi-asserted-by":"publisher","first-page":"347","DOI":"10.3233\/FI-2021-2010","volume":"178","author":"S Conchon","year":"2021","unstructured":"Conchon, S., Delzanno, G., Ferrando, A.: Declarative parameterized verification of distributed protocols via the cubicle model checker. Fundam. Informaticae 178(4), 347\u2013378 (2021). https:\/\/doi.org\/10.3233\/FI-2021-2010","journal-title":"Fundam. Informaticae"},{"key":"16_CR11","doi-asserted-by":"publisher","DOI":"10.1016\/J.ROBOT.2023.104549","volume":"170","author":"P Crisafulli","year":"2023","unstructured":"Crisafulli, P., Taha, S., Wolff, B.: Modeling and analysing cyber-physical systems in HOL-CSP. Robotics Auton. Syst. 170, 104549 (2023). https:\/\/doi.org\/10.1016\/J.ROBOT.2023.104549","journal-title":"Robotics Auton. Syst."},{"key":"16_CR12","unstructured":"da\u00a0Silva Carvalho\u00a0de Freitas, C.A.: A theory for communicating, sequential processes in Coq (2020). https:\/\/api.semanticscholar.org\/CorpusID:259373665"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"660","DOI":"10.1007\/978-3-642-14295-6_56","volume-title":"Computer Aided Verification","author":"EM Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PARAM: a model checker for parametric Markov models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 660\u2013664. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_56"},{"key":"16_CR14","doi-asserted-by":"publisher","unstructured":"Hess, A.V., M\u00f6dersheim, S.A., Brucker, A.D.: Stateful protocol composition in Isabelle\/HOL. ACM Trans. Priv. Secur. 26(3), 25:1\u201325:36 (2023). https:\/\/doi.org\/10.1145\/3577020","DOI":"10.1145\/3577020"},{"key":"16_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)"},{"key":"16_CR16","doi-asserted-by":"publisher","unstructured":"Igried, B., Setzer, A.: Programming with monadic CSP-style processes in dependent type theory. In: Proceedings of the 1st International Workshop on Type-Driven Development, TyDe 2016, pp. 28\u201338. Association for Computing Machinery, New York (2016). https:\/\/doi.org\/10.1145\/2976022.2976032","DOI":"10.1145\/2976022.2976032"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Igried, B., Setzer, A.: Trace and stable failures semantics for CSP-AGDA. arXiv preprint arXiv:1709.04714 (2017)","DOI":"10.4204\/EPTCS.258.3"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Isobe, Y., Roggenbach, M.: A complete axiomatic semantics for the CSP stable-failures model. In: CONCUR 2006 - Concurrency Theory, 17th International Conference, Bonn, Germany, 27\u201330 August 2006, pp. 158\u2013172 (2006)","DOI":"10.1007\/11817949_11"},{"key":"16_CR19","doi-asserted-by":"publisher","unstructured":"Isobe, Y., Roggenbach, M.: CSP-prover: a proof tool for the verification of scalable concurrent systems. Inf. Media Technol. 5(1), 32\u201339 (2010). https:\/\/doi.org\/10.11185\/imt.5.32","DOI":"10.11185\/imt.5.32"},{"key":"16_CR20","unstructured":"Lazic, R.S.: A semantic study of data-independence with applications to the mechanical verification of concurren. Ph.D. thesis, University of Oxford (1999)"},{"key":"16_CR21","doi-asserted-by":"publisher","unstructured":"M\u00fcller, O., Nipkow, T., von Oheimb, D., Slotosch, O.: HOLCF = HOL + LCF. J-FP 9(2), 191\u2013223 (1999). https:\/\/doi.org\/10.1017\/S095679689900341X","DOI":"10.1017\/S095679689900341X"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0055126","volume-title":"Theorem Proving in Higher Order Logics","author":"T Nipkow","year":"1998","unstructured":"Nipkow, T.: Verified lexical analysis. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 1\u201315. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055126"},{"key":"16_CR23","unstructured":"Nipkow, T.: Functional automata. Arch. Formal Proofs 2004 (2004). https:\/\/www.isa-afp.org\/entries\/Functional-Automata.shtml"},{"key":"16_CR24","unstructured":"Noce, P.: Conservation of CSP noninterference security under sequential composition. Archive of Formal Proofs (2016). https:\/\/www.isa-afp.org\/entries\/Noninterference_Sequential_Composition.shtml"},{"key":"16_CR25","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1093\/logcom\/2.5.557","volume":"2","author":"AW Roscoe","year":"1992","unstructured":"Roscoe, A.W.: An alternative order for the failures model. J. Log. Comput. 2, 557\u2013577 (1992)","journal-title":"J. Log. Comput."},{"issue":"1","key":"16_CR26","doi-asserted-by":"publisher","first-page":"147","DOI":"10.3233\/JCS-1999-72-303","volume":"7","author":"AW Roscoe","year":"1999","unstructured":"Roscoe, A.W., Broadfoot, P.J.: Proving security protocols with model checkers by data independence techniques. J. Comput. Secur. 7(1), 147\u2013190 (1999)","journal-title":"J. Comput. Secur."},{"key":"16_CR27","unstructured":"Roscoe, A.: Theory and Practice of Concurrency. Prentice Hall, Hoboken (1997)"},{"key":"16_CR28","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BFb0073967","volume-title":"Toposes, Algebraic Geometry and Logic","author":"D Scott","year":"1972","unstructured":"Scott, D.: Continuous lattices. In: Lawvere, F.W. (ed.) Toposes, Algebraic Geometry and Logic. LNM, vol. 274, pp. 97\u2013136. Springer, Heidelberg (1972). https:\/\/doi.org\/10.1007\/BFb0073967"},{"key":"16_CR29","unstructured":"Taha, S., Wolff, B., Ye, L.: The HOL-CSP refinement toolkit. Arch. Formal Proofs 2020 (2020). https:\/\/www.isa-afp.org\/entries\/CSP_RefTK.html"},{"key":"16_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-030-63461-2_23","volume-title":"Integrated Formal Methods","author":"S Taha","year":"2020","unstructured":"Taha, S., Wolff, B., Ye, L.: Philosophers may dine - definitively! In: Dongol, B., Troubitsyna, E. (eds.) IFM 2020. LNCS, vol. 12546, pp. 419\u2013439. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63461-2_23"},{"key":"16_CR31","unstructured":"Taha, S., Ye, L., Wolff, B.: HOL-CSP Version 2.0. Archive of Formal Proofs (2019). http:\/\/isa-afp.org\/entries\/HOL-CSP.html"},{"key":"16_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/3-540-63533-5_17","volume-title":"FME \u201997: Industrial Applications and Strengthened Foundations of Formal Methods","author":"H Tej","year":"1997","unstructured":"Tej, H., Wolff, B.: A corrected failure-divergence model for CSP in Isabelle\/HOL. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 318\u2013337. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63533-5_17"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2024"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-77019-7_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,21]],"date-time":"2024-11-21T21:30:08Z","timestamp":1732224608000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-77019-7_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,22]]},"ISBN":["9783031770180","9783031770197"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-77019-7_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,22]]},"assertion":[{"value":"22 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bangkok","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Thailand","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2024.cs.ait.ac.th\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}