earticle

영어

Modeling and verification of behavioral variability in service-oriented product line descriptions is very important. Time is a pivotal parameter in representing behaviors of services, which is difficult for scalable modeling and efficient automated checking. In this paper, we describe an approach for modeling and efficient verification of service-oriented product lines. Firstly, we propose feature timed automata, formalism designed to describe the combined behavior of a timed service family, which leverages on establishing relationships between features and transitions. Then, we present feature computation tree logic to model timed properties of service families, which extend computation tree logic to take into account the products constraints. Finally, using our methodology, we analyze a travel agency service family using the model checker UPPAAL. The experiment shows that our approach helps to verify timed service families effectively in the early phases of development.