Synthesis of embedded systems satisfying quantitative constraints by formal methods
| Project/Area Number |
16K00092
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Chitose Institute of Science and Technology (2019-2021)
Tohoku University of Community Service and Science (2017-2018)
Tokyo Institute of Technology (2016) |
|---|
Principal Investigator |
Hagihara Shigeki 公立千歳科学技術大学, 理工学部, 准教授 (70334547)
|
|---|
| Project Period (FY) |
2016-04-01 – 2022-03-31
|
| Project Status |
Completed (Fiscal Year 2021)
|
| Budget Amount *help |
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2019: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2018: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2017: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2016: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
|
|---|
| Keywords | 形式手法 / 組み込みシステム / 自動合成 / 時間論理 / 検証 / 定量的制約 / 組込みシステム / システム検証・合成 / ソフトウェア工学 / 高信頼ソフトウェア開発 |
|---|
| Outline of Final Research Achievements |
Embedded systems are desired to satisfy not only qualitative constraints, but also quantitative constraints. Methods are required to develop systems which necessarily satisfy these constraints. We construct several fundamental techniques for synthesis of embedded systems of practical size, which satisfy these constraints by formal methods.
|
| Academic Significance and Societal Importance of the Research Achievements |
現実的な仕様からシステムを系統的に構成する手法の研究は、ソフトウェア工学の分野で盛んに行われてきたが、それらはデータオリエンテッドな対応であり、それらから得られるのは「経験則」であると指摘されてきた。「法則」を得る方法として形式手法が注目されている。これまで形式手法は、解析に要する計算量の膨大さにより、現実規模の仕様に適用するのが困難であった。本研究は現実規模の仕様に対して、形式手法で解析が可能な範囲、即ち「法則」が適用可能な範囲を明確にするという学術的な特色がある。
|
Report
(7 results)
Research Products
(19 results)
