Integrating behavior analysis into architectural modeling

Abstract

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.

Keywords

software architecture / component behavior / bidirectional transformation / architecture analysis and design language (AADL) / model checking

References

[1] Zheng Y, Taylor R. A classification and rationalization of model-based software development. Software & Systems Modeling, 2013, 12(4): 669-678

[2] Wu W. Architectural reasoning for safety-critical software applications. Dissertation: Department of Computer Science, University of York, 2007

[3] Almorsy M, Grundy J, Ibrahim A S. Automated software architecture security risk analysis using formalized signatures. In: Proceedings of the 2013 International Conference on Software Engineering. 2013, 662-671

[4] Feiler P H, Gluch D P, Hudak J J. The architecture analysis & design language (AADL): An introduction. DTIC Document, 2006

[5] Johnsen A, Lundqvist K, Pettersson P, Jaradat O. Automated verification of AADL-specifications using UPPAAL. In: Proceedings of the 14th IEEE International Symposium on High-Assurance Systems Engineering (HASE). 2012, 130-138

[6] Ölveczky P C, Boronat A, Meseguer J. Formal semantics and analysis of behavioral AADL models in real-time Maude. Formal Techniques for Distributed Systems. LNCS, 2010, 6117: 47-62

[7] Johnsen A, Pettersson P, Lundqvist K. An architecture-based verification technique for AADL specifications. In: Proceedings of the 5th European Conference on Software Architecture (ECSA). 2011, 105-113

[8] Zhang P, Muccini H, Li B. A classification and comparison of model checking software architecture techniques. Journal of Systems and Software, 2010, 83(5): 723-744

[9] Yang Z, Hu K, Ma D, Pi L. Towards a formal semantics for the AADL behavior annex. In: Proceedings of the 2009 Design, Automation & Test in Europe Conference & Exhibition. 2009, 1166-1171

[10] Wang B, Hu Z, Sun Q, Zhao H, Xiong Y, Zhang W, Mei H. Supporting feature model refinement with updatable view. Frontiers of Computer Science, 2013, 7(2): 257-271

[11] Xiong Y, Hu Z, Zhao H, Song H, Takeichi M, Mei H. Supporting automatic model inconsistency fixing. In: Proceedings of the 7th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering. 2009, 315-324

[12] Dashofy E M, Van der Hoek A, Taylor R N. A highly-extensible, XMLbased architecture description language. In: Proceedings of the 2001 Working IEEE/IFIP Conference on Software Architecture. 2001, 103-112

[13] Dashofy E, Asuncion H, Hendrickson S, Suryanarayana G, Georgas J, Taylor R. Archstudio 4: an architecture-based meta-modeling environment. In: Proceedings of the 29th International Conference on Software Engineering-Companion Volume. 2007, 67-68

[14] Kramer J, Magee J, Uchitel S. Software architecture modeling & analysis: a rigorous approach. In: Formal Methods for Software Architectures. 2003, 44-51

[15] Allen R, Garlan D. A formal basis for architectural connection. ACM Transactions on Software Engineering and Methodology (TOSEM), 1997, 6(3): 213-249

[16] Garlan D, Monroe R, Wile D. Acme: an architecture description interchange language. In: CASCON First Decade High Impact Papers. 2010, 159-173

[17] Malavolta I, Muccini H, Pelliccione P, Tamburri D A. Providing architectural languages and tools interoperability through model transformation technologies. IEEE Transactions on Software Engineering, 2010, 36(1): 119-140

[18] Malavolta I, Muccini H, Pelliccione P. Integrating AADL within a multi-domain modeling framework. In: Proceedings of the 14th IEEE International Conference on Engineering of Complex Computer Systems. 2009, 341-346

[19] Hettel T, Lawley M, Raymond K. Model synchronisation: definitions for round-trip engineering. In: Proceedings of the 1st International Conference on Model Transformations. 2008, 31-45

[20] Hidaka S, Hu Z, Inaba K, Kato H, Matsuda K, Nakano K. Bidirectionalizing graph transformations. In: Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming. 2010, 205-216

[21] Song H, Huang G, Chauvel F, Xiong Y, Hu Z, Sun Y, Mei H. Supporting runtime software architecture: a bidirectional-transformationbased approach. Journal of Systems and Software, 2011, 84(5): 711-723

[22] Yu Y, Lin Y, Hu Z, Hidaka S, Kato H, Montrieux L. Maintaining invariant traceability through bidirectional transformations. In: Proceedings of the 2012 International Conference on Software Engineering. 2012, 540-550

[23] Xiong Y, Liu D, Hu Z, Zhao H, Takeichi M, Mei H. Towards automatic model synchronization from model transformations. In: Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering. 2007, 164-173

[24] Feiler P, Rugina A. Dependability modeling with the architecture analysis & design language (AADL). DTIC Document, 2007

[25] Dissaux P, Bodeveix J P, Filali M, Gaufillet P, Vernadat F. AADL behavioral annex. In: Proceedings of the 2006 Data Systems in Aerospace Conference. 2006

[26] Hidaka S, Hu Z, Inaba K, Kato H, Nakano K. GRoundTram: an integrated framework for developing well-behaved bidirectional model transformations. In: Proceedings of 26th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2011, 480-483

[27] Hidaka S, Hu Z, Kato H, Nakano K. A compositional approach to bidirectional model transformation. In: Proceedings of the 31st International Conference on Software Engineering-Companion Volume. 2009, 235-238

[28] Hidaka S, Hu Z, Inaba K, Kato H, Matsuda K, Nakano K. GRoundTram Version 0.9. 3 User Manual, 2008

RIGHTS & PERMISSIONS

2014 Higher Education Press and Springer-Verlag Berlin Heidelberg