2023 Fiscal Year Research-status Report
A theorem prover for the correct development of reconfigurable systems
| Project/Area Number |
23K11048
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
GAINA Daniel 九州大学, マス・フォア・インダストリ研究所, 准教授 (80595778)
|
|---|
| Project Period (FY) |
2023-04-01 – 2027-03-31
|
| Keywords | transition algebra / calculi / Maude / concurrency |
|---|
| 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.
|
| Causes of Carryover |
I would like to purchase a new laptop for presentations during academic meetings. Additionally, I will travel to Prague to participate in a conference called Advances in Modal Logic, AiML 2024. Following that, I will travel to Madrid and/or Bucharest to visit my collaborators and discuss further issues related to the implementation of the theorem prover proposed in this project.
|
