A BEHAVIOURAL MODELING AND VERIFICATION FOR TIMED SERVICE-ORIENTED PRODUCT LINES

摘要：

　　Modeling and verification of behavioral variability in service-oriented product family descriptions is very important.Many existing methods can only model the basic service behaviors,and time constraints are not taken into consideration,which is an important parameter in service behaviors.In this paper,we described an approach for modeling and verification of behaviors for a timed service family.Firstly,we propose featured Timed Automata,a formalism designed to describe the combined behavior of a timed service family,which leverages on establishing relationships between features and transitions.Then,we use product Computation Tree Logic to model properties of service families,which extend Computation Tree Logic to take into account the product constraints.Finally,we have verified a travel agency service family by the model checker UPPAAL,which shows that our approach helps to verify timed service families effectively in the early phases of development.

关键词： Service-oriented product lines Timed automata Behavioral modeling Timed temporal logic Model checking

作者: Hongxia Zhang Hua Zou Fangchun Yang Rongheng Lin

作者单位: College of Computer & Communication Engineering China University of Petroleum,Qingdao 266580,China;S State Key Laboratory of Networking & Switching Beijing University of Posts and Telecommunications,Be

会议类型: 国际会议

会议名称: 2012 2nd IEEE International Conference on Cloud Computing and Intelligence Systems (2012年第2届IEEE云计算与智能系统国际会议(IEEE CCIS2012))

会议地点: 杭州

会议语种:英文

页码: 33-38

在线出版日期: 2012-10-30（万方平台首次上网日期，不代表论文的发表时间）