Specification Methods for Runtime Verification of Reflective Software
| 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
|
| Project Status |
Completed (Fiscal Year 2014)
|
| Budget Amount *help |
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2014: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2013: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2012: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
|
|---|
| 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.
|
Report
(4 results)
Research Products
(31 results)
-
-
-
-
-
-
-
-
-
-
-
-
-
-
[Presentation] Aπ計算のCoqによる形式化2014
Author(s)
安武祥平, 渡部卓雄
Organizer
日本ソフトウェア科学会第31回大会
Place of Presentation
名古屋大学・東山キャンパス
Year and Date
2014-09-07 – 2014-09-10
Related Report
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
