Specification Methods for Runtime Verification of Reflective Software

2014 Fiscal Year Final Research Report

• Project/Area Number: 24500033
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: Tokyo Institute of Technology
• Principal Investigator: WATANABE Takuo 東京工業大学, 情報理工学(系)研究科, 准教授 (20222408)
• Project Period (FY): 2012-04-01 – 2015-03-31
• Keywords: 自己反映計算 / 広域自己反映計算 / アクターモデル / 文脈指向プログラミング / 形式手法 / 実行時検証

Outline of Final Research Achievements

The main contributions of this work include (1) a novel construction method of group-wide reflective architectures and (2) extensible and modularized verification methods for concurrent language execution models. The key idea of the former is to apply parallel composition to actors that constitute the meta-level of the actor groups. This results in a uniform construction method for various types of meta-level actors. The proposed method can be used to implement concurrent context-oriented systems. For the latter, we proposed a method to support the extension of verified programs by interactively modifying their definitions and proofs and a modularized description/verification method for reflective concurrent systems.

Free Research Field

計算機ソフトウェア