In embedded system development, software depends on hardware and we have to change software specification frequently because of hardware specification changes. Therefore in embedded software development, it is important to get reusable software. To get reusable software, it is important to divide common and variant features. To analyze features, FODA is effective. But because FODA uses natural languages, we can't validate the consistency of the models and can't solve interaction problems. To validate the consistency and solve interaction problems, we have to get strict model. Formal methods are effective methods to get strict model. Therefore, purpose of our research is to get reusable strict embedded systems specifications. We intend to use formal methods to solve feature interaction problem and get strict reusable embedded systems specifications.