본문 바로가기
  • Home

A Formal Specification and Checking Technique of Feature model using Z language

  • Journal of The Korea Society of Computer and Information
  • Abbr : JKSCI
  • 2013, 18(1), pp.123-136
  • Publisher : The Korean Society Of Computer And Information
  • Research Area : Engineering > Computer Science

Chee-Yang Song 1 Eun-Sook Cho 2 Kim Chul Jin 3

1경북대학교
2서일대학
3인하공업전문대학

Accredited

ABSTRACT

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.

Citation status

* References for papers published after 2022 are currently being built.