Interface Specification Assurance Methods

PSL supports property inheritance by verification units. The lack of formal semantics of the inherit operator is an obstacle to reduce the complexity of system design and verification. This paper presents a verification-layer specification assurance tool. Based on the component-based design methodology, we propose a principled organization of component specifications, and apply SAT solvers to verify the consistency of specifications, the compatibility of components, the refinement relation among specifications, and the correctness of specification inheritance. We also discuss the implementation aspect of such a tool