Exploiting Assume-Guarantee Contract Patterns to Optimize the Discovery of Design-space Dependencies

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.