{"id":{"repo_id":"carleton","oai_identifier":"oai:carleton.scholaris.ca:20.500.14718/42825"},"canonical_url":"https://search.dev.ndltd.org/etd/carleton/oai:carleton.scholaris.ca:20.500.14718/42825","repository":{"repo_id":"carleton","name":"Carleton University","base_url":"https://carleton.scholaris.ca/server/oai/request"},"display":{"title":"Modular Verification of Hierarchical Component-Based Software Systems","abstract":"Using Component-based Software Engineering approaches with Formal Methods has seen an influx of interest in the recent decades. The joining of these two disciplines have been stifled though due to unclear component specifications and expensive formal verification techniques, which hurt the reusability and scalability of complex software systems. In this work, we expand on current component-port-connector metamodels for formally specifying a system's architectural and behavioural requirements into a hierarchical component system structure by using abstract Composite Components. The Composite Components of a system model can then utilize modular verification for isolating the verification process into modules surrounding Composite Components and generating higher level properties. We formalize our metamodel in Alloy 6 and present a template for specifying system properties for modular verification which enables the reuse of previous verification efforts on satisfied modules. We conclude with an example case study system and analysis of the modular verification strategy.","abstract_html":"Using Component-based Software Engineering approaches with Formal Methods has seen an influx of interest in the recent decades. The joining of these two disciplines have been stifled though due to unclear component specifications and expensive formal verification techniques, which hurt the reusability and scalability of complex software systems. In this work, we expand on current component-port-connector metamodels for formally specifying a system's architectural and behavioural requirements into a hierarchical component system structure by using abstract Composite Components. The Composite Components of a system model can then utilize modular verification for isolating the verification process into modules surrounding Composite Components and generating higher level properties. We formalize our metamodel in Alloy 6 and present a template for specifying system properties for modular verification which enables the reuse of previous verification efforts on satisfied modules. We conclude with an example case study system and analysis of the modular verification strategy.","abstract_has_math":false,"creators":["Baak, James Alec William"],"institution":"Carleton University","degree_name":"Master of Applied Science (M.App.Sc.)","degree_level":"Master's","degree_discipline":"Engineering, Electrical and Computer","degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2023,"date_issued":"2023","date_published":"2023","updated_at":"2026-07-24T01:34:36Z","subjects":[],"languages":["en"],"rights":["Copyright © 2023 the author(s). Theses may be used for non-commercial research, educational, or related academic purposes only. Such uses include personal study, research, scholarship, and teaching. Theses may only be shared by linking to Carleton University Institutional Repository and no part may be used without proper attribution to the author. No part may be used for commercial purposes directly or indirectly via a for-profit platform; no adaptation or derivative works are permitted without consent from the copyright owner."],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier.doi","label":"DOI","values":["10.22215/etd/2023-15449"],"render_values":[{"text":"10.22215/etd/2023-15449","href":"https://doi.org/10.22215/etd/2023-15449","code":true}]}]},"links":{"outbound_url":"https://hdl.handle.net/20.500.14718/42825","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Baak, James Alec William"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2025-04-08T20:44:43Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2025-04-08T20:44:43Z"]},{"key":"dc:date.issued","label":"Date","values":["2023"]},{"key":"dc:publisher","label":"Institution","values":["Carleton University"]},{"key":"dc:type","label":"Dc Type","values":["thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Engineering, Electrical and Computer"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Master's"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master of Applied Science (M.App.Sc.)"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright © 2023 the author(s). Theses may be used for non-commercial research, educational, or related academic purposes only. Such uses include personal study, research, scholarship, and teaching. Theses may only be shared by linking to Carleton University Institutional Repository and no part may be used without proper attribution to the author. No part may be used for commercial purposes directly or indirectly via a for-profit platform; no adaptation or derivative works are permitted without consent from the copyright owner."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.doi","label":"DOI","values":["10.22215/etd/2023-15449"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/20.500.14718/42825"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["Using Component-based Software Engineering approaches with Formal Methods has seen an influx of interest in the recent decades. The joining of these two disciplines have been stifled though due to unclear component specifications and expensive formal verification techniques, which hurt the reusability and scalability of complex software systems. In this work, we expand on current component-port-connector metamodels for formally specifying a system's architectural and behavioural requirements into a hierarchical component system structure by using abstract Composite Components. The Composite Components of a system model can then utilize modular verification for isolating the verification process into modules surrounding Composite Components and generating higher level properties. We formalize our metamodel in Alloy 6 and present a template for specifying system properties for modular verification which enables the reuse of previous verification efforts on satisfied modules. We conclude with an example case study system and analysis of the modular verification strategy."]},{"key":"dc:title","label":"Title","values":["Modular Verification of Hierarchical Component-Based Software Systems"]}]}],"canonical_facts":{"dc:creator":["Baak, James Alec William"],"dc:date.accessioned":["2025-04-08T20:44:43Z"],"dc:date.available":["2025-04-08T20:44:43Z"],"dc:date.issued":["2023"],"dc:description.abstract":["Using Component-based Software Engineering approaches with Formal Methods has seen an influx of interest in the recent decades. The joining of these two disciplines have been stifled though due to unclear component specifications and expensive formal verification techniques, which hurt the reusability and scalability of complex software systems. In this work, we expand on current component-port-connector metamodels for formally specifying a system's architectural and behavioural requirements into a hierarchical component system structure by using abstract Composite Components. The Composite Components of a system model can then utilize modular verification for isolating the verification process into modules surrounding Composite Components and generating higher level properties. We formalize our metamodel in Alloy 6 and present a template for specifying system properties for modular verification which enables the reuse of previous verification efforts on satisfied modules. We conclude with an example case study system and analysis of the modular verification strategy."],"dc:identifier.doi":["10.22215/etd/2023-15449"],"dc:identifier.uri":["https://hdl.handle.net/20.500.14718/42825"],"dc:language.iso":["en"],"dc:publisher":["Carleton University"],"dc:rights":["Copyright © 2023 the author(s). Theses may be used for non-commercial research, educational, or related academic purposes only. Such uses include personal study, research, scholarship, and teaching. Theses may only be shared by linking to Carleton University Institutional Repository and no part may be used without proper attribution to the author. No part may be used for commercial purposes directly or indirectly via a for-profit platform; no adaptation or derivative works are permitted without consent from the copyright owner."],"dc:title":["Modular Verification of Hierarchical Component-Based Software Systems"],"dc:type":["thesis"],"thesis:degree_discipline":["Engineering, Electrical and Computer"],"thesis:degree_level":["Master's"],"thesis:degree_name":["Master of Applied Science (M.App.Sc.)"]},"updated_at":"2026-07-24T01:34:36Z"}