Efficient runtime formal verification of aspect-oriented models@run.time systems

2016 Fiscal Year Final Research Report

• Project/Area Number: 26330081
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: The University of Electro-Communications
• Principal Investigator: Tahara Yasuyuki 電気通信大学, 大学院情報理工学研究科, 准教授 (30390602)
• Project Period (FY): 2014-04-01 – 2017-03-31
• Keywords: ソフトウェア工学 / アスペクト指向 / models@run.time / 形式手法 / モデル検査 / リフレクション / 抽象化 / 自己適応システム

Outline of Final Research Achievements

We developed a code generation system that provides an abstraction / refinement relation between the model and the source code based on the framework of the formal model of aspect-oriented models@run.time system proposed by us. We extended the framework of the formal model so that it can deal with the behavior in which aspects are woven at runtime for adaptation, by adding, as new axioms, axiom changing rules that formalize aspect weaving using reflection. We developed a prototype of verification and adaptation integrating the code generation system and the verification system based on the design of the prototype of the verification / adaptation system. We also implemented, conducted experiments of, and evaluated the example web / ubiquitous application.

Free Research Field

ソフトウェア工学