Integrating behavior analysis into architectural modeling

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 transformation 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.