Formal Verification of Dynamic Evolution Processes of UML Models Using Aspects

Yasuyuki Tahara, Akihiko Ohsuga, Shinichi Honiden

研究成果: Conference contribution

4 被引用数 (Scopus)

抄録

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.

本文言語English
ホスト出版物のタイトル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.
ページ152-162
ページ数11
ISBN(電子版)9781538615508
DOI
出版ステータスPublished - 2017 7月 3
外部発表はい
イベント12th IEEE/ACM International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2017 - Buenos Aires, Argentina
継続期間: 2017 5月 222017 5月 23

出版物シリーズ

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

Other

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

ASJC Scopus subject areas

  • 制御と最適化
  • ソフトウェア
  • 人工知能

フィンガープリント

「Formal Verification of Dynamic Evolution Processes of UML Models Using Aspects」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル