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.

목차

Abstract
 1. Introduction
 2. Running Example: Travel Agency
 3. Feature Timed Automata
 4. The Temporal Logics for FTA
 5. Model Checking a Family of Services
 6. Related Work
 7. Conclusion and Future Work
 Acknowledgment
 References

키워드

저자

• Hongxia Zhang [ College of Computer & Communication Engineering, China University of Petroleum,Qingdao, P. R. China ]
• Fei Wang [ School of Economics & Management,China University of Petroleum Qingdao, P. R. China ]

참고문헌

발행기관

간행물

표지보기 관심저널 등록

• 간행물명

  International Journal of u- and e- Service, Science and Technology

• 간기

  격월간

• pISSN

  2005-4246

• 수록기간

  2008~2016

• 십진분류

  KDC 505 DDC 605