KJCKorea
Journal Central

@article{ART001739439},
author={Chee-Yang Song and Eun-Sook Cho and Kim Chul Jin},
title={A Formal Specification and Checking Technique of Feature model using Z language},
journal={Journal of The Korea Society of Computer and Information},
issn={1598-849X},
year={2013},
volume={18},
number={1},
pages={123-136}

TY - JOUR
AU - Chee-Yang Song
AU - Eun-Sook Cho
AU - Kim Chul Jin
TI - A Formal Specification and Checking Technique of Feature model using Z language
JO - Journal of The Korea Society of Computer and Information
PY - 2013
VL - 18
IS - 1
PB - The Korean Society Of Computer And Information
SP - 123
EP - 136
SN - 1598-849X
AB - 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.
KW - Feature model;Z;Formal specification;Model checking;Z/Eves
DO -
UR -
ER -

Chee-Yang Song, Eun-Sook Cho and Kim Chul Jin. (2013). A Formal Specification and Checking Technique of Feature model using Z language. Journal of The Korea Society of Computer and Information, 18(1), 123-136.

Chee-Yang Song, Eun-Sook Cho and Kim Chul Jin. 2013, "A Formal Specification and Checking Technique of Feature model using Z language", Journal of The Korea Society of Computer and Information, vol.18, no.1 pp.123-136.

Chee-Yang Song, Eun-Sook Cho, Kim Chul Jin "A Formal Specification and Checking Technique of Feature model using Z language" Journal of The Korea Society of Computer and Information 18.1 pp.123-136 (2013) : 123.

Chee-Yang Song, Eun-Sook Cho, Kim Chul Jin. A Formal Specification and Checking Technique of Feature model using Z language. 2013; 18(1), 123-136.

Chee-Yang Song, Eun-Sook Cho and Kim Chul Jin. "A Formal Specification and Checking Technique of Feature model using Z language" Journal of The Korea Society of Computer and Information 18, no.1 (2013) : 123-136.

Chee-Yang Song; Eun-Sook Cho; Kim Chul Jin. A Formal Specification and Checking Technique of Feature model using Z language. Journal of The Korea Society of Computer and Information, 18(1), 123-136.

Chee-Yang Song; Eun-Sook Cho; Kim Chul Jin. A Formal Specification and Checking Technique of Feature model using Z language. Journal of The Korea Society of Computer and Information. 2013; 18(1) 123-136.

Chee-Yang Song, Eun-Sook Cho, Kim Chul Jin. A Formal Specification and Checking Technique of Feature model using Z language. 2013; 18(1), 123-136.

Chee-Yang Song, Eun-Sook Cho and Kim Chul Jin. "A Formal Specification and Checking Technique of Feature model using Z language" Journal of The Korea Society of Computer and Information 18, no.1 (2013) : 123-136.