In software product line development, consistency among artifacts is important because commonalities and variabilities increase the complexity of relations among artifacts. For small scale models, the relations among elements can be easily identified and tracked by manually analyzing the descriptions of models. But when the complexity of models is high, a more systematic approach is required for identifying traceability information and verifying consistency between models. In this paper, by utilizing Formal Concept Analysis (FCA) and Prototype Verification System (PVS), we present a formal approach for identifying traceability and verifying consistency between feature model and component and connector view of software architecture.