| 研究課題/領域番号 |
23K11048
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
GAINA Daniel 九州大学, マス・フォア・インダストリ研究所, 准教授 (80595778)
|
|---|
| 研究期間 (年度) |
2023-04-01 – 2027-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円)
2026年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2025年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2024年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2023年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
|
|---|
| キーワード | transition algebra / calculi / Maude / concurrency / theorem proving / reconfigurable systems / hybrid systems |
|---|
| 研究開始時の研究の概要 |
Modern software systems are often equipped with reconfigurable features. Reconfigurable systems are often used in safety-critical areas. The safety requirements can be fulfilled only by applying formal methods.
The objective is to develop a software tool for the formal verification of such systems.
|
| 研究実績の概要 |
The first year of the project was dedicated to designing the theorem prover.
Adjustments to the logical framework originally outlined by the PI in [Gaina, JACM 2020] were necessary to enable seamless integration within Maude, the programming language used for implementation. We introduced a novel logical system, called transition algebra, which enhances many-sorted first-order logic using features from dynamic logics. This allows us to capture system states as terms, and hence to reason about the structure of states more freely and in a more complex manner than it is possible in dynamic logic. For the development of a methodology tailored to reconfigurable systems, we explored Robin Milner’s calculus of communicating systems (CCSS) [Milner, Prentice-Hall 1989] as our primary case study. CCS is a process calculus that enables syntactic descriptions of concurrent systems to be written, and subsequently manipulated and analyzed. CCS is emblematic of a broad family of formal languages used for modeling and reasoning about concurrency. In a nutshell, CCS is a process calculus that enables syntactic descriptions of concurrent systems to be written, and subsequently manipulated and analyzed.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
Throughout the reporting period, the project progressed steadily, with significant advancements made towards the release of a prototype theorem prover. During the design phase, adjustments to the logical framework, as initially outlined, facilitated seamless integration within the Maude programming language. A notable highlight of this period was the introduction of transition algebra, which can also serve as a semantics for the Maude strategy language. Additionally, the exploration of Robin Milner’s calculus of communicating systems as a case study for developing a tailored methodology for reconfigurable systems proceeded without major obstacles. Overall, the project navigated its course with efficiency, promising further advances towards its objectives.
|
| 今後の研究の推進方策 |
The implementation of the theorem prover has started, and a prototype tool is scheduled for release in FY 2024. The actions of the transition algebra, as outlined previously, will be realized using the Maude strategy language. The core components of the tool are currently in development, encompassing the parser and tactics constructed from the proof rules of the underlying logic. These tactics will form the foundation for creating proof strategies aimed at efficiently discharging proof goals. Additionally, we are collaborating with partner universities across Europe to develop a graphical interface, ensuring smooth interaction with users. A comprehensive user guide will provide detailed specifications and verification methods supported by the tool.
|
