Exploiting Assume-Guarantee Contract Patterns to Optimize the Discovery of Design-space Dependencies
Date
2023-05
Authors
Hammer, Abigail
Major Professor
Advisor
Rozier, Kristin
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Model-checking large and extensive sets of requirements for a system often means tackling the challenging problem of state-space explosion The Discovering of Design-space Dependencies (D3) algorithm exploits relationships within systems in order to optimize the model-checking search. By incorporating Assume-Guarantee Contracts into the existing D3 algorithm, it is possible to further exploit the known patterns of the requirements in order to further reduce the model checking complexity. We detail a set of different variations for optimizing D3 processing that exploits patterns present in Assume-Guarantee Contracts. Additionally, we are able to use this exploitation to provide vacuity checking for specifications within the contract. We identify requirements that are unable to enter undesired states or provides expected results due to the nature of the requirement's patterns.
Series Number
Journal Issue
Is Version Of
Versions
Series
Series
Academic or Administrative Unit
Type
Presentation