Description method and formal verification method with section behavior model based on software architecture

2021 Fiscal Year Final Research Report

• Project/Area Number: 19K11911
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60050:Software-related
• Research Institution: Nanzan University
• Principal Investigator: Chang Han-Myung 南山大学, 理工学部, 准教授 (90329756)
• Co-Investigator(Kenkyū-buntansha): 野呂 昌満 南山大学, 理工学部, 教授 (40189452) ; 沢田 篤史 南山大学, 理工学部, 教授 (40273841)
• Project Period (FY): 2019-04-01 – 2022-03-31
• Keywords: 形式手法 / 形式仕様 / 形式仕様言語 / モデル検査 / ソフトウェアアーキテクチャ

Outline of Final Research Achievements

Since multiple things operate in parallel in an IoT system, it is necessary to consider events that occur simultaneously. Failure to correctly recognize the simultaneity of these events can be the cause of system failures. It is difficult to guarantee the correctness of a parallel system by testing alone. Systematizing a method for describing and verifying event concurrency in the system design phase is expected to contribute to improving the quality of parallel system design.

Free Research Field

形式手法に基づくソフトウェア開発手法

Academic Significance and Societal Importance of the Research Achievements

並行システムの振る舞いの記述・検証のための言語としてプロセス代数では，事象の同時性を表現するためのステップ意味論などが理論的な研究は行われているが，同時性を考慮した振る舞い仕様の設計方法に関する研究成果はまだない．本研究では，事象の同時性を区間として局所化した構造を定式化して，その意味を既存のモデル検査を有するプロセス代数で定義することにより，事象の同時性を考慮した開発環境の基礎を築く．