Description method and formal verification method with section behavior model based on software architecture
| 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 |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
野呂 昌満 南山大学, 理工学部, 教授 (40189452)
沢田 篤史 南山大学, 理工学部, 教授 (40273841)
|
|---|
| Project Period (FY) |
2019-04-01 – 2022-03-31
|
| Project Status |
Completed (Fiscal Year 2021)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2021: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2020: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2019: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| Keywords | 形式手法 / 形式仕様 / 形式仕様言語 / モデル検査 / ソフトウェアアーキテクチャ / 並列システム / イベントの同時性 / プロセス代数 / CSP / 同時性 / 振る舞い検証 / 詳細化検証 / UML / 組み込みシステム / 並列・並行システム / アーキテクチャ / 並行システム |
|---|
| Outline of Research at the Start |
高度に情報化されたネットワーク社会では，異なったシステムを統合してシステムのシステムを構築することが求められる．並列に動作するシステムでは，複数の事象が並列に発生するので，同時に発生する事象を考慮する必要がある．この並列事象の同時性を正しく認識できないことはシステム障害（failure）の原因となる．このようなシステムの信頼性を高めるためには，従来のテスト技術だけでは十分ではない．本研究では，並列事象の同時性を区間に局所化した「区間振る舞いモデル」を提案し，並列事象の同時性を並行システムとして実現するさいの振る舞い仕様の記述法とその検証法を体系化することにより，形式検証技術の実用化を目指す．
|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
並行システムの振る舞いの記述・検証のための言語としてプロセス代数では，事象の同時性を表現するためのステップ意味論などが理論的な研究は行われているが，同時性を考慮した振る舞い仕様の設計方法に関する研究成果はまだない．本研究では，事象の同時性を区間として局所化した構造を定式化して，その意味を既存のモデル検査を有するプロセス代数で定義することにより，事象の同時性を考慮した開発環境の基礎を築く．
|
Report
(4 results)
Research Products
(10 results)
