시각적이고 비정형적인 구조로 표현된 휘처 모델(Feature model)은 구문적 명확성을 보장할 수 없고, 자동화 툴(tool)에 의한 구문(syntax)의 검증이 어렵다. 따라서, 휘처 모델이 가진 구조물의 구문적 명확성을 입증하기 위한 정형적 명세와 모델 검사(model checking)가 필요하다. 본 논문은 Z 언어를 이용한 휘처 모델의 정형적 명세와 모델 검사를 통해서, 휘처 모델의 정확성을 검사하는 기법을 제시한다. 이를 위해, 휘처 모델과 Z간 변환 규칙을 정의하고, 이 규칙에 의거하여 휘처 모델의 구문에 대해 Z 스키마(schema)로 명세한다. 모델 검사는 Z 스키마 명세에 대해 Z/Eves 툴을 사용하여 구문, 타입 검사(type checking), 그리고 도메인 검사(domain checking)를 수행하여 모델의 모호성을 검사한다. 이로서, 휘처 모델의 구조물을 좀더 명확하게 표현할 수 있으며, 설계된 모델의 오류를 검사할 수 있다.
The Feature model can not be guaranteed the syntactic accuracy of its model and be difficult the validation using automatic tool for its syntax, because this model is expressed by a graphical and informal structure in itself. Therefore, there is a need to formalize and check for the feature model, to precisely define syntax for construct of the model. This paper presents a Z formal specification and a model checking mechanism of the feature model to guarantee the correctness of the model. It first defines the translation rules between feature model and Z, and then converts the syntax of the feature model into the Z schema specification by applying these rules. Finally, the Z schema specification is checked syntax, type, and domain errors using the Z/Eves validation tool to assure the correctness of its specification, With the use of the proposed method, we may express more precisely the construct of the feature model. Moreover the domain analyst are able to usefully verify the errors of the generated feature model.