{"id":2015,"date":"2025-04-17T14:38:39","date_gmt":"2025-04-17T18:38:39","guid":{"rendered":"https:\/\/carleton.ca\/cybersea\/?p=2015"},"modified":"2026-01-26T10:41:49","modified_gmt":"2026-01-26T15:41:49","slug":"new-publication-a-formal-approach-for-verifying-and-validating-security-objectives-in-software-architecture","status":"publish","type":"post","link":"https:\/\/carleton.ca\/cybersea\/2025\/new-publication-a-formal-approach-for-verifying-and-validating-security-objectives-in-software-architecture\/","title":{"rendered":"New Publication: A Formal Approach for Verifying and Validating Security Objectives in Software Architecture"},"content":{"rendered":"\n<section class=\"w-screen px-6 cu-section cu-section--white ml-offset-center md:px-8 lg:px-14\">\n    <div class=\"space-y-6 cu-max-w-child-5xl  md:space-y-10 cu-prose-first-last\">\n\n            <div class=\"cu-textmedia flex flex-col lg:flex-row mx-auto gap-6 md:gap-10 my-6 md:my-12 first:mt-0 max-w-5xl\">\n        <div class=\"justify-start cu-textmedia-content cu-prose-first-last\" style=\"flex: 0 0 100%;\">\n            <header class=\"font-light prose-xl cu-pageheader md:prose-2xl cu-component-updated cu-prose-first-last\">\n                                    <h1 class=\"cu-prose-first-last font-semibold !mt-2 mb-4 md:mb-6 relative after:absolute after:h-px after:bottom-0 after:bg-cu-red after:left-px text-3xl md:text-4xl lg:text-5xl lg:leading-[3.5rem] pb-5 after:w-10 text-cu-black-700 not-prose\">\n                        New Publication: A Formal Approach for Verifying and Validating Security Objectives in Software Architecture\n                    <\/h1>\n                \n                                \n                            <\/header>\n\n                    <\/div>\n\n            <\/div>\n\n    <\/div>\n<\/section>\n\n<p>Our recent work on &#8220;<a href=\"https:\/\/doi.org\/10.1007\/978-3-031-85356-2_10\">A Formal Approach for Verifying and Validating Security Objectives in Software Architecture<\/a>&#8221; is now available online. This paper proposes an approach for the design and analysis of secure software architecture in the context of a component-port-connector architecture model and message passing communication. We use the Event-B formal method to create the software architecture model and security in successive steps using the refinement process. We also use proof obligations to verify the security of the successive software architecture models. Furthermore, we use the ProB model-checker and animator for the model validation. This paper was presented at&nbsp;the <a href=\"https:\/\/www.vecos-world.org\/2024\/\">17th International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS 2024)<\/a>. See <a href=\"https:\/\/carleton.ca\/cybersea\/publications\/\">Publications<\/a> for more details!<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Our recent work on &#8220;A Formal Approach for Verifying and Validating Security Objectives in Software Architecture&#8221; is now available online. This paper proposes an approach for the design and analysis of secure software architecture in the context of a component-port-connector architecture model and message passing communication. We use the Event-B formal method to create the [&hellip;]<\/p>\n","protected":false},"author":2,"featured_media":431,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":"","_links_to":"","_links_to_target":""},"categories":[41],"tags":[],"class_list":["post-2015","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-publication"],"acf":{"cu_post_thumbnail":""},"_links":{"self":[{"href":"https:\/\/carleton.ca\/cybersea\/wp-json\/wp\/v2\/posts\/2015","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/carleton.ca\/cybersea\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/carleton.ca\/cybersea\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/carleton.ca\/cybersea\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/carleton.ca\/cybersea\/wp-json\/wp\/v2\/comments?post=2015"}],"version-history":[{"count":3,"href":"https:\/\/carleton.ca\/cybersea\/wp-json\/wp\/v2\/posts\/2015\/revisions"}],"predecessor-version":[{"id":2022,"href":"https:\/\/carleton.ca\/cybersea\/wp-json\/wp\/v2\/posts\/2015\/revisions\/2022"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/carleton.ca\/cybersea\/wp-json\/wp\/v2\/media\/431"}],"wp:attachment":[{"href":"https:\/\/carleton.ca\/cybersea\/wp-json\/wp\/v2\/media?parent=2015"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/carleton.ca\/cybersea\/wp-json\/wp\/v2\/categories?post=2015"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/carleton.ca\/cybersea\/wp-json\/wp\/v2\/tags?post=2015"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}