Modular Verification of Hierarchical Component-Based Software Systems

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.

Name thesis:degree_name

Master of Applied Science (M.App.Sc.)

Level thesis:degree_level

Master's

Discipline thesis:degree_discipline

Engineering, Electrical and Computer

Grantor dc:publisher

Carleton University

Year dc:date.issued

2023

Author dc:creator

• Baak, James Alec William

Statement 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.

Language dc:language.iso

en

DOI

10.22215/etd/2023-15449

OAI identifier oai:identifier

oai:carleton.scholaris.ca:20.500.14718/42825