Formal Verification of Dynamic Evolution Processes of UML Models Using Aspects

Yasuyuki Tahara, Akihiko Ohsuga, Shinichi Honiden

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

The rapidly changing requirements and environments of system operation demand dynamic changes to systems with as short downtimes as possible. System availability is a relevant feature for such dynamic changes, which we call dynamic evolution. One of the most promising approaches to highly available dynamic evolution is dynamic aspect weaving, a technique of aspect-oriented programming technology. It enables part of a program to dynamically change without stopping its execution. Another feature relevant to dynamic evolution is the assurance of correctness of evolution. However, this is not easy for dynamic evolution, mainly because the evolution process is rather complicated. Formal modeling and verification (specifically, model checking) are other promising technologies. Many researchers have proposed various approaches to model and verify dynamic evolution. However, highly available dynamic evolution processes tend to be too complicated to verify with existing techniques because such processes need to be simultaneously controlled with system functionalities and the operations for evolution that include dynamic aspect weaving. We propose a formal verification tool called CAMPer that analyzes the unified modeling language (UML) models of dynamic evolution processes that consist of multiple steps with sophisticated control that includes dynamic aspect weaving. This tool is able to verify functional requirements for the processes that would be complicated to attain high availability. Our approach uses the Maude specification language to systematically express dynamic evolution and dynamic aspect weaving by using reflection. We also used a model checker for Maude to verify the evolution processes. We conducted experiments using an example Tele Assistance System (TAS) to demonstrate the advantages of our approach and evaluate its feasibility.

Original languageEnglish
Title of host publicationProceedings - 2017 IEEE/ACM 12th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2017
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages152-162
Number of pages11
ISBN (Electronic)9781538615508
DOIs
Publication statusPublished - 2017 Jul 3
Externally publishedYes
Event12th IEEE/ACM International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2017 - Buenos Aires, Argentina
Duration: 2017 May 222017 May 23

Other

Other12th IEEE/ACM International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2017
CountryArgentina
CityBuenos Aires
Period17/5/2217/5/23

Fingerprint

Unified Modeling Language
Language Model
Formal Verification
Verify
Maude
Formal verification
Availability
Aspect oriented programming
Aspect-oriented Programming
Formal Modeling
High Availability
Specification languages
Requirements
Specification Languages
Model checking
Model Checking

Keywords

  • algebraic specifications
  • aspect-oriented software development
  • CAM (Component Aspect Model)
  • dynamic aspect weaving
  • dynamic evolution
  • formal verification
  • Maude
  • model checking
  • reflection
  • UML

ASJC Scopus subject areas

  • Control and Optimization
  • Software
  • Artificial Intelligence

Cite this

Tahara, Y., Ohsuga, A., & Honiden, S. (2017). Formal Verification of Dynamic Evolution Processes of UML Models Using Aspects. In Proceedings - 2017 IEEE/ACM 12th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2017 (pp. 152-162). [7968143] Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/SEAMS.2017.4

Formal Verification of Dynamic Evolution Processes of UML Models Using Aspects. / Tahara, Yasuyuki; Ohsuga, Akihiko; Honiden, Shinichi.

Proceedings - 2017 IEEE/ACM 12th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2017. Institute of Electrical and Electronics Engineers Inc., 2017. p. 152-162 7968143.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Tahara, Y, Ohsuga, A & Honiden, S 2017, Formal Verification of Dynamic Evolution Processes of UML Models Using Aspects. in Proceedings - 2017 IEEE/ACM 12th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2017., 7968143, Institute of Electrical and Electronics Engineers Inc., pp. 152-162, 12th IEEE/ACM International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2017, Buenos Aires, Argentina, 17/5/22. https://doi.org/10.1109/SEAMS.2017.4
Tahara Y, Ohsuga A, Honiden S. Formal Verification of Dynamic Evolution Processes of UML Models Using Aspects. In Proceedings - 2017 IEEE/ACM 12th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2017. Institute of Electrical and Electronics Engineers Inc. 2017. p. 152-162. 7968143 https://doi.org/10.1109/SEAMS.2017.4
Tahara, Yasuyuki ; Ohsuga, Akihiko ; Honiden, Shinichi. / Formal Verification of Dynamic Evolution Processes of UML Models Using Aspects. Proceedings - 2017 IEEE/ACM 12th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2017. Institute of Electrical and Electronics Engineers Inc., 2017. pp. 152-162
@inproceedings{df53f4bc39f0493f9931c3a45a301c9d,
title = "Formal Verification of Dynamic Evolution Processes of UML Models Using Aspects",
abstract = "The rapidly changing requirements and environments of system operation demand dynamic changes to systems with as short downtimes as possible. System availability is a relevant feature for such dynamic changes, which we call dynamic evolution. One of the most promising approaches to highly available dynamic evolution is dynamic aspect weaving, a technique of aspect-oriented programming technology. It enables part of a program to dynamically change without stopping its execution. Another feature relevant to dynamic evolution is the assurance of correctness of evolution. However, this is not easy for dynamic evolution, mainly because the evolution process is rather complicated. Formal modeling and verification (specifically, model checking) are other promising technologies. Many researchers have proposed various approaches to model and verify dynamic evolution. However, highly available dynamic evolution processes tend to be too complicated to verify with existing techniques because such processes need to be simultaneously controlled with system functionalities and the operations for evolution that include dynamic aspect weaving. We propose a formal verification tool called CAMPer that analyzes the unified modeling language (UML) models of dynamic evolution processes that consist of multiple steps with sophisticated control that includes dynamic aspect weaving. This tool is able to verify functional requirements for the processes that would be complicated to attain high availability. Our approach uses the Maude specification language to systematically express dynamic evolution and dynamic aspect weaving by using reflection. We also used a model checker for Maude to verify the evolution processes. We conducted experiments using an example Tele Assistance System (TAS) to demonstrate the advantages of our approach and evaluate its feasibility.",
keywords = "algebraic specifications, aspect-oriented software development, CAM (Component Aspect Model), dynamic aspect weaving, dynamic evolution, formal verification, Maude, model checking, reflection, UML",
author = "Yasuyuki Tahara and Akihiko Ohsuga and Shinichi Honiden",
year = "2017",
month = "7",
day = "3",
doi = "10.1109/SEAMS.2017.4",
language = "English",
pages = "152--162",
booktitle = "Proceedings - 2017 IEEE/ACM 12th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2017",
publisher = "Institute of Electrical and Electronics Engineers Inc.",

}

TY - GEN

T1 - Formal Verification of Dynamic Evolution Processes of UML Models Using Aspects

AU - Tahara, Yasuyuki

AU - Ohsuga, Akihiko

AU - Honiden, Shinichi

PY - 2017/7/3

Y1 - 2017/7/3

N2 - The rapidly changing requirements and environments of system operation demand dynamic changes to systems with as short downtimes as possible. System availability is a relevant feature for such dynamic changes, which we call dynamic evolution. One of the most promising approaches to highly available dynamic evolution is dynamic aspect weaving, a technique of aspect-oriented programming technology. It enables part of a program to dynamically change without stopping its execution. Another feature relevant to dynamic evolution is the assurance of correctness of evolution. However, this is not easy for dynamic evolution, mainly because the evolution process is rather complicated. Formal modeling and verification (specifically, model checking) are other promising technologies. Many researchers have proposed various approaches to model and verify dynamic evolution. However, highly available dynamic evolution processes tend to be too complicated to verify with existing techniques because such processes need to be simultaneously controlled with system functionalities and the operations for evolution that include dynamic aspect weaving. We propose a formal verification tool called CAMPer that analyzes the unified modeling language (UML) models of dynamic evolution processes that consist of multiple steps with sophisticated control that includes dynamic aspect weaving. This tool is able to verify functional requirements for the processes that would be complicated to attain high availability. Our approach uses the Maude specification language to systematically express dynamic evolution and dynamic aspect weaving by using reflection. We also used a model checker for Maude to verify the evolution processes. We conducted experiments using an example Tele Assistance System (TAS) to demonstrate the advantages of our approach and evaluate its feasibility.

AB - The rapidly changing requirements and environments of system operation demand dynamic changes to systems with as short downtimes as possible. System availability is a relevant feature for such dynamic changes, which we call dynamic evolution. One of the most promising approaches to highly available dynamic evolution is dynamic aspect weaving, a technique of aspect-oriented programming technology. It enables part of a program to dynamically change without stopping its execution. Another feature relevant to dynamic evolution is the assurance of correctness of evolution. However, this is not easy for dynamic evolution, mainly because the evolution process is rather complicated. Formal modeling and verification (specifically, model checking) are other promising technologies. Many researchers have proposed various approaches to model and verify dynamic evolution. However, highly available dynamic evolution processes tend to be too complicated to verify with existing techniques because such processes need to be simultaneously controlled with system functionalities and the operations for evolution that include dynamic aspect weaving. We propose a formal verification tool called CAMPer that analyzes the unified modeling language (UML) models of dynamic evolution processes that consist of multiple steps with sophisticated control that includes dynamic aspect weaving. This tool is able to verify functional requirements for the processes that would be complicated to attain high availability. Our approach uses the Maude specification language to systematically express dynamic evolution and dynamic aspect weaving by using reflection. We also used a model checker for Maude to verify the evolution processes. We conducted experiments using an example Tele Assistance System (TAS) to demonstrate the advantages of our approach and evaluate its feasibility.

KW - algebraic specifications

KW - aspect-oriented software development

KW - CAM (Component Aspect Model)

KW - dynamic aspect weaving

KW - dynamic evolution

KW - formal verification

KW - Maude

KW - model checking

KW - reflection

KW - UML

UR - http://www.scopus.com/inward/record.url?scp=85027185337&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85027185337&partnerID=8YFLogxK

U2 - 10.1109/SEAMS.2017.4

DO - 10.1109/SEAMS.2017.4

M3 - Conference contribution

SP - 152

EP - 162

BT - Proceedings - 2017 IEEE/ACM 12th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2017

PB - Institute of Electrical and Electronics Engineers Inc.

ER -