| Project/Area Number |
23K11048
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
GAINA Daniel 九州大学, マス・フォア・インダストリ研究所, 准教授 (80595778)
|
|---|
| Project Period (FY) |
2023-04-01 – 2027-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2026: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2025: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2024: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2023: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| Keywords | transition algebra / calculi / Maude / concurrency / theorem proving / reconfigurable systems / hybrid systems |
|---|
| Outline of Research at the Start |
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.
|
| Outline of Annual Research Achievements |
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.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
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.
|
| Strategy for Future Research Activity |
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.
|
