Interface Specification Assurance Methods

Naiyong Jin
East China Normal University


Abstract

Interface plays a critical role in component-based system design. Interface specifications shall expose sufficient information to predict that modules behind them can work properly. As written by human beings, a specification tends to be erroneous. This paper aims at a framework for interface specification assurance. We classify interface properties to assumptions and guarantees, and check the role of an interface property by their type and syntax. We reduce the interface existence problem and the environment/module compatibility problem to satisfiability checking. The framework presented in this paper can be implemented readily by formal verification drivers.