Integrating behavior analysis into architectural modeling

doi:10.1007/s11704-014-3505-z

Front. Comput. Sci.

2015, Vol. 9

Issue (1) : 15-33 https://doi.org/10.1007/s11704-014-3505-z

RESEARCH ARTICLE

Integrating behavior analysis into architectural modeling

Luxi CHEN¹,Linpeng HUANG^1,^*(

),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

Download: PDF(2170 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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

Corresponding Author(s): Linpeng HUANG

Issue Date: 09 February 2015

Cite this article:

Luxi CHEN,Linpeng HUANG,Chen LI, et al. Integrating behavior analysis into architectural modeling[J]. Front. Comput. Sci., 2015, 9(1): 15-33.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-014-3505-z
https://academic.hep.com.cn/fcs/EN/Y2015/V9/I1/15

1	Zheng Y, Taylor R. A classification and rationalization of model-based software development. Software & Systems Modeling, 2013, 12(4): 669-678 https://doi.org/10.1007/s10270-013-0355-3
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 https://doi.org/10.1016/j.jss.2009.11.709
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 https://doi.org/10.1007/s11704-013-2047-0
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 https://doi.org/10.1109/WICSA.2001.948416
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 https://doi.org/10.1145/258077.258078
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 https://doi.org/10.1109/TSE.2009.51
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 https://doi.org/10.1145/1863543.1863573
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 https://doi.org/10.1016/j.jss.2010.12.009
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

[1]

Supplementary Material

Download

[1]	Yuanrui ZHANG, Frédéric MALLET, Yixiang CHEN. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Front. Comput. Sci., 2020, 14(1): 105-129.
[2]	Kazuhiro OGATA. A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions[J]. Front. Comput. Sci., 2019, 13(1): 51-72.
[3]	Anil Kumar KARNA, Yuting CHEN, Haibo YU, Hao ZHONG, Jianjun ZHAO. The role of model checking in software engineering[J]. Front. Comput. Sci., 2018, 12(4): 642-668.
[4]	Yu ZHOU, Nvqi ZHOU, Tingting HAN, Jiayi GU, Weigang WU. Probabilistic verification of hierarchical leader election protocol in dynamic systems[J]. Front. Comput. Sci., 2018, 12(4): 763-776.
[5]	Fei HE, Yuan GAO, Liangze YIN. Efficient software product-line model checking using induction and a SAT solver[J]. Front. Comput. Sci., 2018, 12(2): 264-279.
[6]	Zhibin YANG,Jean-Paul BODEVEIX,Mamoun FILALI,Kai HU,Yongwang ZHAO,Dianfu MA. Towards a verified compiler prototype for the synchronous language SIGNAL[J]. Front. Comput. Sci., 2016, 10(1): 37-53.
[7]	Xing CHEN,Aipeng LI,Xue’e ZENG,Wenzhong GUO,Gang HUANG. Runtime model based approach to IoT application development[J]. Front. Comput. Sci., 2015, 9(4): 540-553.
[8]	Laixiang SHAN,Xiaomin DU,Zheng QIN. Efficient approach of translating LTL formulae into Büchi automata[J]. Front. Comput. Sci., 2015, 9(4): 511-523.
[9]	Yuanjie SI, Jun SUN, Yang LIU, Jin Song DONG, Jun PANG, Shao Jie ZHANG, Xiaohu YANG. Model checking with fairness assumptions using PAT[J]. Front. Comput. Sci., 2014, 8(1): 1-16.
[10]	Savas KONUR. A survey on temporal logics for specifying and verifying real-time systems[J]. Front. Comput. Sci., 2013, 7(3): 370-403.
[11]	Gang HUANG, Xing CHEN, Ying ZHANG, Xiaodong ZHANG. Towards architecture-based management of platforms in the cloud[J]. Front Comput Sci, 2012, 6(4): 388-397.
[12]	Anh Tuan LUU, Jun SUN, Yang LIU, Jin Song DONG, Xiaohong LI, Thanh Tho QUAN. SeVe: automatic tool for verification of security protocols[J]. Front Comput Sci, 2012, 6(1): 57-75.
[13]	Conghua ZHOU, Bo SUN, Zhifeng LIU. Abstraction for model checking multi-agent systems[J]. Front Comput Sci Chin, 2011, 5(1): 14-25.
[14]	Jiaqi ZHU, Hanpin WANG, Zhongyuan XU, Chunxiang XU, . A new model for model checking: cycle-weighted Kripke structure[J]. Front. Comput. Sci., 2010, 4(1): 78-88.
[15]	Wanwei LIU, Ji WANG, Huowang CHEN, Xiaodong MA, Zhaofei WANG. symbolic model checking APSL[J]. Front Comput Sci Chin, 2009, 3(1): 130-141.

Viewed

Full text

Abstract

Cited

Shared

Discussed