{"id":2013,"date":"2025-04-09T14:35:52","date_gmt":"2025-04-09T18:35:52","guid":{"rendered":"https:\/\/carleton.ca\/cybersea\/?p=2013"},"modified":"2026-01-26T10:41:49","modified_gmt":"2026-01-26T15:41:49","slug":"new-publication-reusable-formal-model-libraries-for-specifying-and-analyzing-security-objectives-in-event-b","status":"publish","type":"post","link":"https:\/\/carleton.ca\/cybersea\/2025\/new-publication-reusable-formal-model-libraries-for-specifying-and-analyzing-security-objectives-in-event-b\/","title":{"rendered":"New Publication: Reusable Formal Model Libraries for Specifying and Analyzing Security Objectives in Event-B"},"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: Reusable Formal Model Libraries for Specifying and Analyzing Security Objectives in Event-B\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. In this paper, we propose an integrated approach for specifying and verifying security objectives in component-based software architecture models via reusable formal model libraries of security properties and constraints. Our solution is based on metamodeling techniques for specifying the software architecture structure and on formal techniques for precisely specifying and verifying security properties of a modeled system. We explore a set of representative security objectives from the Confidentiality, Integrity, Availability (CIA) classification. We also use model-driven engineering techniques for the development of a tool suite to support our approach. This paper was presented at&nbsp;the <a href=\"https:\/\/medi2024.dieti.unina.it\">13th International Conference on Model and Data Engineering (MEDI 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. In this paper, we propose an integrated approach for specifying and verifying security objectives in component-based software architecture models via reusable formal model libraries of security properties and constraints. Our solution is based on metamodeling [&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-2013","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\/2013","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=2013"}],"version-history":[{"count":3,"href":"https:\/\/carleton.ca\/cybersea\/wp-json\/wp\/v2\/posts\/2013\/revisions"}],"predecessor-version":[{"id":2025,"href":"https:\/\/carleton.ca\/cybersea\/wp-json\/wp\/v2\/posts\/2013\/revisions\/2025"}],"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=2013"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/carleton.ca\/cybersea\/wp-json\/wp\/v2\/categories?post=2013"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/carleton.ca\/cybersea\/wp-json\/wp\/v2\/tags?post=2013"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}