Specification and Runtime Verification Methods for Adaptive Parallel Systems based on Group-Wide Reflection

2017 Fiscal Year Final Research Report

• Project/Area Number: 15K00089
• 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): 2015-04-01 – 2018-03-31
• Keywords: 広域自己反映計算 / 自己反映計算 / アクターモデル / 関数リアクティブプログラミング

Outline of Final Research Achievements

The goal of this project is to provide a framework for specification and run-time verification of actor-based reflective systems. To achieve the goal, we took a new approach to the actor-based group-wide reflection (GWR), which allows each actor to have capabilities of reasoning about/acting upon the collective behavior of the group it belongs to. We applied the proposed method to implement concurrent context-oriented programming (COP) systems. To realize COP in concurrent systems based on asynchronous communication, we must take care to control synchronizations among context changes and other computations. We adopt an instance of GWR to solve the synchronization problem regarding messages that cross two contexts. We also developed a static verification framework for actor-based systems in Coq, as well as a run-time verification library for Akka-based applications.

Free Research Field

プログラミング言語