Integrating behavior analysis into architectural modeling  

作　　者：Luxi CHEN Linpeng HUANG Chen LI Tao ZAN 

机构地区：[1]Department of Computer Science and Engineering, Shanghai Jiao Tong University, Shanghai 200240, China [2]Department of Informatics, The Graduate University for Advanced Studies, Tokyo 108430, Japan

出　　处：《Frontiers of Computer Science》2015年第1期15-33,共19页中国计算机科学前沿（英文版）

基　　金：The authors would like to thank anonymous reviewers for their helpful comments and suggestions. Special thanks to Raymond Cheng, Andrew Liu and Yuan Yao for their careful revisions. This work was supported by the National Natural Science Foundation of China under （Grant Nos. 91118004, 61232007）, and the Innovation Program of Shanghai Municipal Education Commission （13ZZ023）.

摘　　要：Architectural modeling and behavior analysis are two important concerns in the software development. They are often implemented separately, and specified by their own supporting notations. Architectural modeling helps to guarantee the system design to satisfy the requirement, and behavior analysis can ensure the interaction correctness. To improve the trustworthiness, methods trying to combine architectural modeling and behavior analysis notations together have been proposed, e.g., establishing a one-way mapping relation. However, the one-way relation cannot ensure updating one notation specifications in accordance with the other one, which results in inconsistency problems. In this paper, we present an approach to integrating behavior analysis into architectural modeling, which establishes the interoperability between architectural modeling notation and behavior analysis notation by a bidirectional mapping. The architecture is specified by the modeling language, architecture analysis and design language （AADL）, and then mapped to behavior analysis notation, Darwin/FSP （finite state process） through the bidirectional transformation. The bidirectional transformarion provides traceability, which makes behavior analysis result provided by a model checker can be traced and reflected back to the original AADL specifications. In this way, the behavior analysis is integrated into architectural modeling. The feasibility of our approach is shown by a control system example.Architectural modeling and behavior analysis are two important concerns in the software development. They are often implemented separately, and specified by their own supporting notations. Architectural modeling helps to guarantee the system design to satisfy the requirement, and behavior analysis can ensure the interaction correctness. To improve the trustworthiness, methods trying to combine architectural modeling and behavior analysis notations together have been proposed, e.g., establishing a one-way mapping relation. However, the one-way relation cannot ensure updating one notation specifications in accordance with the other one, which results in inconsistency problems. In this paper, we present an approach to integrating behavior analysis into architectural modeling, which establishes the interoperability between architectural modeling notation and behavior analysis notation by a bidirectional mapping. The architecture is specified by the modeling language, architecture analysis and design language （AADL）, and then mapped to behavior analysis notation, Darwin/FSP （finite state process） through the bidirectional transformation. The bidirectional transformarion provides traceability, which makes behavior analysis result provided by a model checker can be traced and reflected back to the original AADL specifications. In this way, the behavior analysis is integrated into architectural modeling. The feasibility of our approach is shown by a control system example.

关 键 词：software architecture component behavior bidirectional transformation architecture analysis and design language （AADL） model checking 

分 类 号：TP316.9[自动化与计算机技术—计算机软件与理论] TU-80[自动化与计算机技术—计算机科学与技术]