Formalization and Consistency Checking of Changes of Software System Configurations Using Alloy

Generally, functions and execution environment which form a software system are changed because requirements change, referred to as "software evolution\´\´. At this change, maintaining consistency of the configuration is important, in order to prevent trouble. However, it is difficult for software engineers to perform this kind of maintenance. Thus, when a configuration is changed, computer support is needed. In this paper, we propose a method of FMC (feature, module and connection) which focuses on the maintenance of configuration changes, and we formalize FMC by alloy. FMC is a modeling method which is based on the feature model of FODA. FMC abstracts functions, execution environment and correspondence relations between functions and execution environment. In addition, we describe how to check and correct inconsistency of FMC using alloy.