We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 35 Issue 5
September  2020
Turn off MathJax
Article Contents
Abstract
References
Related Articles
Supplements
De-Shuai Han, Qi-Liang Yang, Jian-Chun Xing, Guang-Lian Ma. EasyModel: A Refinement-Based Modeling and Verification Approach for Self-Adaptive Software[J]. Journal of Computer Science and Technology, 2020, 35(5): 1016-1046. DOI: 10.1007/s11390-020-0499-x
Citation: De-Shuai Han, Qi-Liang Yang, Jian-Chun Xing, Guang-Lian Ma. EasyModel: A Refinement-Based Modeling and Verification Approach for Self-Adaptive Software[J]. Journal of Computer Science and Technology, 2020, 35(5): 1016-1046. DOI: 10.1007/s11390-020-0499-x
shu

EasyModel: A Refinement-Based Modeling and Verification Approach for Self-Adaptive Software

  • 1 College of Combat Support, Rocket Force University of Engineering, Xi'an 710025, China;
    2 College of Defense Engineering, Army Engineering University of PLA, Nanjing 210007, China;
    3 Teaching and Research Support Center, Rocket Force University of Engineering, Xi'an 710025, China

Funds: The work was supported by the National Key Research and Development Program of China under Grant No. 2017YFC0704100.
More Information
  • Corresponding author:

    Qi-Liang Yang E-mail: yql@893.com.cn

  • Received Date: April 05, 2020
  • Revised Date: July 24, 2020
  • Published Date: September 19, 2020
    Abstract
  • Self-adaptive software (SAS) is gaining popularity as it can reconfigure itself in response to the dynamic changes in the operational context or itself. However, early modeling and formal analysis of SAS systems becomes increasingly difficult, as the system scale and complexity is rapidly increasing. To tackle the modeling difficulty of SAS systems, we present a refinement-based modeling and verification approach called EasyModel. EasyModel integrates the intuitive Unified Modeling Language (UML) model with the stepwise refinement Event-B model. Concretely, EasyModel: 1) creates a UML profile called AdaptML that provides an explicit description of SAS characteristics, 2) proposes a refinement modeling mechanism for SAS systems that can deal with system modeling complexity, 3) offers a model transformation approach and bridges the gap between the design model and the formal model of SAS systems, and 4) provides an efficient way to verify and guarantee the correct behaviour of SAS systems. To validate EasyModel, we present an example application and a subject-based experiment. The results demonstrate that EasyModel can effectively reduce the modeling and formal verification difficulty of SAS systems, and can incorporate the intuitive merit of UML and the correct-by-construction merit of Event-B.
    • FullText(HTML)
    • References (46)
  • [1]
    Salehie M, Tahvildari L. Self-adaptive software:Landscape and research challenges. ACM Transactions on Autonomous and Adaptive Systems, 2009, 4(2):Article No. 14.
    [2]
    de Lemos R, Garlan D, Ghezzi C et al. Software engineering for self-adaptive systems:Research challenges in the provision of assurances. In Proc. the International Seminar on Software Engineering for Self-Adaptive Systems, December 2017, pp.3-30.
    [3]
    Weyns D. Software engineering of self-adaptive systems. In Handbook of Software Engineering, Cha S, Taylor R N, Kang K (eds.), Springer, 2019, pp.399-443.
    [4]
    Luckey M, Engels G. High-quality specification of selfadaptive software systems. In Proc. the 8th International Symposium on Software Engineering for Adaptive and SelfManaging Systems, May 2013, pp.143-152.
    [5]
    Han D S, Yang Q L, Xing J C et al. FAME:A UML-based framework for modeling fuzzy self-adaptive software. Information & Software Technology, 2016, 76:118-134.
    [6]
    Said M B, Kacem Y H, Kerboeuf M et al. Design patterns for self-adaptive RTE systems specification. International Journal of Reconfigurable Computing, 2014, 2014:Article No. 536362.
    [7]
    de la Iglesia D G, Weyns D. MAPE-K formal templates to rigorously design behaviors for self-adaptive systems. ACM Transactions on Autonomous & Adaptive Systems, 2015, 10(3):Article No. 15.
    [8]
    Iftikhar M U, Weyns D. ActivFORMS:A runtime environment for architecture-based adaptation with guarantees. In Proc. the IEEE Int. Conf. Software Architecture, April 2017, pp.278-281.
    [9]
    Camilli M, Gargantini A, Scandurra P. Zone-based formal specification and timing analysis of real-time self-adaptive systems. Science of Computer Programming, 2018, 159:28-57.
    [10]
    Ding Z, Zhou Y, Zhou M. Modeling self-adaptive software systems by fuzzy rules and Petri nets. IEEE Transactions on Fuzzy Systems, 2018, 26(2):967-984.
    [11]
    Almeida A, Bencomo N, Batista T et al. Dynamic decisionmaking based on NFR for managing software variability and configuration selection. In Proc. the 30th Annual ACM Symp. Applied Computing, April 2015, pp.1376-1382.
    [12]
    Weyns D, Iftikhar M U. Model-based simulation at runtime for self-adaptive systems. In Proc. the 2016 IEEE Int. Conf. Autonomic Computing, July 2016, pp.364-373.
    [13]
    Ahmad M, Belloir N, Bruel J M. Modeling and verification of functional and non-functional requirements of ambient self-adaptive systems. Journal of Systems & Software, 2015, 107:50-70.
    [14]
    Abrial J R. Modeling in Event-B:System and Software Engineering. Cambridge University Press, 2013.
    [15]
    Han D, Yang Q, Xing J. UML-Based modeling and formal verification for software self-adaptation. Journal of Software, 2015, 26(4):730-746. (in Chinese)
    [16]
    Object Management Group, The OMG unified modeling language (OMG UML), superstructure, version 2.4.1, OMG Document No. formal/2011-08-06, 2011.
    [17]
    Gérard S, Dumoulin C, Tessier P, Selic B. Papyrus:A UML2 tool for domain-specific language modeling. In Proc. Int. Conf. Model-Based Engineering of Embedded RealTime Systems, November 2007, pp.361-368.
    [18]
    Abrial J R, Butler M, Hallerstede S et al. Rodin an open toolset for modelling and reasoning in Event-B. International Journal on Software Tools for Technology Transfer, 2010, 12(6):447-466.
    [19]
    Leuschel M, Butler M. ProB:A model checker for B. In Proc. International Symposium of Formal Methods Europe, September 2003, pp.855-874.
    [20]
    Mentré D, Marché C, Filliâtre J C et al. Discharging proof obligations from Atelier B using multiple automated provers. In Proc. the 3rd Int. Conf. Abstract State Machines, Alloy, B, VDM, and Z, June 2012, pp.238-251.
    [21]
    Boniol F, Wiels V, Ameur Y A, Schewe K D. The landing gear case study:Challenges and experiments. International Journal on Software Tools for Technology Transfer, 2017, 19(2):133-140.
    [22]
    Su W, Abrial J R. Aircraft landing gear system:Approaches with Event-B to the modeling of an industrial system. International Journal on Software Tools for Technology Transfer, 2017, 19(2):141-166.
    [23]
    Laibinis L, Klionskiy D, Troubitsyna E et al. Modelling resilience of data processing capabilities of CPS. In Proc. the 6th International Workshop on Software Engineering for Resilient Systems, October 2014, pp.55-70.
    [24]
    Cheng S W. Rainbow:Cost-effective software architecturebased self-adaptation[Ph.D. Thesis]. Carnegie Mellon University, 2008.
    [25]
    Kephart J O, Chess D M. The vision of autonomic computing. IEEE Computer, 2003, 36(1):41-50.
    [26]
    Vandome A F, Mcbrewster J, Miller F P. ATLAS Transformation Language. Alphascript Publishing, 2010.
    [27]
    Hachicha M, Dammak E, Halima R B et al. A correct by construction approach for modeling and formalizing selfadaptive systems. In Proc. the 17th IEEE/ACIS Int. Conf. Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing, June 2016, pp.379-384.
    [28]
    Vogel T. Model-driven engineering of self-adaptive software[Ph.D. Thesis]. University of Potsdam, 2018.
    [29]
    Vogel T, Giese H. Model-driven engineering of self-adaptive software with EUREMA. ACM Transactions on Autonomous & Adaptive Systems, 2014, 8(4):Article No. 18.
    [30]
    Cámara J, Lopes A, Garlan D et al. Adaptation impact and environment models for architecture-based self-adaptive systems. Science of Computer Programming, 2016, 127:50-75.
    [31]
    Han D, Xing J, Yang Q et al. Modeling and verification approach for temporal properties of self-adaptive software dynamic processes. Journal of Computer Applications, 2018, 38(3):799-805. (in Chinese)
    [32]
    Krupitzer C, Roth F M, VanSyckel S et al. A survey on engineering approaches for self-adaptive systems. Pervasive and Mobile Computing, 2015, 17:184-206.
    [33]
    Abuseta Y, Swesi K. Design patterns for self-adaptive systems engineering. International Journal of Software Engineering & Applications, 2015, 6(4):11-28.
    [34]
    Becker S, Dziwok S, Gerking C et al. The MechatronicUML method:Model-driven software engineering of self-adaptive mechatronic systems. In Proc. the 36th Int. Conf. Software Engineering, May 2014, pp.614-615.
    [35]
    Heinzemann C, Becker S, Volk A. Transactional execution of hierarchical reconfigurations in cyber-physical systems. Software & Systems Modeling, 2019, 18(1):157-189.
    [36]
    da Silva J P S, Ecar M, Pimenta M S et al. A systematic literature review of UML-based domain specific modeling languages for self-adaptive systems. In Proc. the 13th IEEE/ACM Int. Symp. Software Engineering for Adaptive and Self-Managing Systems, May 2018, pp.87-93.
    [37]
    Moritani B I, Lee J. An approach for managing a distributed feature model to evolve self-adaptive dynamic software product lines. In Proc. the 21st International Systems and Software Product Line Conference, September 2017, pp.107-110.
    [38]
    Chen T, Li K, Bahsoon R et al. FEMOSAA:Featureguided and knee-driven multi-objective optimization for self-adaptive software. ACM Transactions on Software Engineering and Methodology, 2018, 27(2):Article No. 5.
    [39]
    de la Iglesia D G, Calderón J F, Weyns D et al. A selfadaptive multi-agent system approach for collaborative mobile learning. IEEE Transactions on Learning Technologies, 2015, 8(2):158-172.
    [40]
    Wang L, Li Q. A multiagent-based framework for selfadaptive software with search-based optimization. In Proc. IEEE Int. Conf. Software Maintenance and Evolution, October 2016, pp.621-625.
    [41]
    Iftikhar M U, Weyns D. ActivFORMS:A runtime environment for architecture-based adaptation with guarantees. In Proc. Int. Conf. Software Architecture Workshops, April 2017, pp.278-281.
    [42]
    Abbas N, Andersson J, Iftikhar U M et al. Rigorous architectural reasoning for self-adaptive software systems. In Proc. the 1st Workshop on Qualitative Reasoning about Software Architectures, April 2016, pp.11-18.
    [43]
    Abbas N, Andersson J. Architectural reasoning support for product-lines of self-adaptive software systems-A case study. In Proc. the 9th European Conference on Software Architecture, September 2015, pp.20-36.
    [44]
    Su G, Chen T, Feng Y et al. An iterative decision-making scheme for Markov decision processes and its application to self-adaptive systems. In Proc. the 19th Int. Conf. Fundamental Approaches to Software Engineering, April 2016, pp.269-286.
    [45]
    Filieri A, Tamburrelli G, Ghezzi C. Supporting selfadaptation via quantitative verification and sensitivity analysis at run time. IEEE Transactions on Software Engineering, 2016, 42(1):75-99.
    [46]
    Göthel T, Jähnig N, Seif S. Refinement-based modelling and verification of design patterns for self-adaptive systems. In Proc. the 19th Int. Conf. Formal Engineering Methods, November 2017. pp.157-173.
    • Relative Articles

  • Related Articles

    [1]Inès Mouakher, Fatma Dhaou, J. Christian Attiogbé. Event-Based Semantics of UML 2.X Concurrent Sequence Diagrams for Formal Verification[J]. Journal of Computer Science and Technology, 2022, 37(1): 4-28. DOI: 10.1007/s11390-021-1673-5
    [2]Heng-Feng Wei, Rui-Ze Tang, Yu Huang, Jian Lv. Jupiter Made Abstract, and Then Refined[J]. Journal of Computer Science and Technology, 2020, 35(6): 1343-1364. DOI: 10.1007/s11390-020-0516-0
    [3]Rui Hou, Ji-Gang Wu, Yawen Chen, Haibo Zhang, Xiu-Feng Sui. Constructing Edge-Colored Graph for Heterogeneous Networks[J]. Journal of Computer Science and Technology, 2015, 30(5): 1154-1160. DOI: 10.1007/s11390-015-1551-0
    [4]Jun-Zuo Lai, Wen-Tao Zhu, Robert H. Deng, Sheng-Li Liu, Wei-Dong Kou. New Constructions for Identity-Based Unidirectional Proxy Re-Encryption[J]. Journal of Computer Science and Technology, 2010, 25(4): 793-806. DOI: 10.1007/s11390-010-1062-y
    [5]Rui Xue, Ning-Hui Li, Jiang-Tao Li. Algebraic Construction for Zero-Knowledge Sets[J]. Journal of Computer Science and Technology, 2008, 23(2): 166-175.
    [6]Ewen Denney. Simply-typed Underdeterminism[J]. Journal of Computer Science and Technology, 1998, 13(6): 491-508.
    [7]Zhang Tong. Intuitionistic Logic as the Implement of Incremental Model Construction for Natural Language[J]. Journal of Computer Science and Technology, 1998, 13(1): 13-17.
    [8]Zhang Jian. Automatic Construction of Finite Algebras[J]. Journal of Computer Science and Technology, 1995, 10(3): 206-213.
    [9]Zeng Jianchao, Hidehiko Sanada, Yoshikazu, Tezuka Xu Guangyou. A Form-Correcting System of Chinese Characters Using a Model of Correcting Procedures of Calligraphists[J]. Journal of Computer Science and Technology, 1995, 10(1): 23-34.
    [10]Lu Ruzhan, Zhang Zheng, Sun Yongqiang. Construction of the Model of the Lambda Calculus System with Algebraic Operators[J]. Journal of Computer Science and Technology, 1991, 6(1): 108-112.
    • Supplements (2)

  • Others

  • Cited by

    Periodical cited type(8)

    1. Runfang Wu, Ye Du, Yu Tang. A Research landscape on formal verification of UML dynamic modeling. The Journal of Supercomputing, 2025, 81(8) DOI:10.1007/s11227-025-07464-8
    2. Deshuai Han, Yanping Cai, WenJie Chen, et al. Timed-SAS: Modeling and Analyzing the Time Behaviors of Self-Adaptive Software under Uncertainty. Applied Sciences, 2023, 13(3): 2018. DOI:10.3390/app13032018
    3. Riadh Ben Halima, Marwa Hachicha, Ahmed Jemal, et al. MAPE-K patterns for self-adaptation in cyber-physical systems. The Journal of Supercomputing, 2023, 79(5): 4917. DOI:10.1007/s11227-022-04828-2
    4. Muhammad Abid Jamil, Mohamed K. Nour, Saud S. Alotaibi, et al. Adaptive Test Suits Generation for Self-Adaptive Systems Using SPEA2 Algorithm. Applied Sciences, 2023, 13(20): 11324. DOI:10.3390/app132011324
    5. Marwa Hachicha, Riadh Ben Halima, Ahmed Hadj Kacem. Modeling Autonomic Systems. International Journal of Software Innovation, 2022, 10(1): 1. DOI:10.4018/IJSI.303585
    6. Mouna Ben Said, Nader Ben Amor, Fatma Ben Taher, et al. Multi-constraints self-adaptation for reconfigurable multimedia embedded systems. The Journal of Supercomputing, 2022, 78(7): 9038. DOI:10.1007/s11227-021-04269-3
    7. Henrik Ejersbo, Kenneth Lausdahl, Mirgita Frasheri, et al. Dynamic Runtime Integration of New Models in Digital Twins. 2023 IEEE/ACM 18th Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), DOI:10.1109/SEAMS59076.2023.00016
    8. Deshuai Han, Guanglian Ma, Yanping Cai, et al. ProbaSAS: Modeling and Decision-Making Approach for Self-Adaptive Software Systems under Uncertainty. 2022 41st Chinese Control Conference (CCC), DOI:10.23919/CCC55666.2022.9901985

    Other cited types(0)

Catalog

    Get Citation
    PDF
    XML
    Read Online
    Article views (91) PDF downloads (0) Cited by(8)
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    Institute of Computing Technology, Chinese Academy of Sciences
    P.O. Box 2704, Beijing 100190, P.R. China

    Tel.: 86-10-62610746 E-mail: jcst@ict.ac.cn

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return