Student: Abigail Hammer, Undergraduate Student in Aerospace Engineering, Iowa State University
Research Mentor: Dr. Kristin Rozier
Exploiting Assume-Guarantee Contract Patterns to Optimize the Discovery of Design Space Dependencies
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 (AG) 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 exploit patterns present in Assume-Guarantee Contracts. Additionally, we are able to use this exploitation to provide vacuity checking for the specifications in the AG contract. We identify requirements that are unable to enter undesired states or do not provide expected results due to the nature of the requirement’s patterns.