| 研究課題/領域番号 |
19K11911
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 南山大学 |
|---|
研究代表者 |
張 漢明 南山大学, 理工学部, 准教授 (90329756)
|
|---|
| 研究分担者 |
野呂 昌満 南山大学, 理工学部, 教授 (40189452)
沢田 篤史 南山大学, 理工学部, 教授 (40273841)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2022-03-31
|
| 研究課題ステータス |
完了 (2021年度)
|
| 配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2021年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2020年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2019年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
|
|---|
| キーワード | 形式手法 / 形式仕様 / 形式仕様言語 / モデル検査 / ソフトウェアアーキテクチャ / 並列システム / イベントの同時性 / プロセス代数 / CSP / 同時性 / 振る舞い検証 / 詳細化検証 / UML / 組み込みシステム / 並列・並行システム / アーキテクチャ / 並行システム |
|---|
| 研究開始時の研究の概要 |
高度に情報化されたネットワーク社会では，異なったシステムを統合してシステムのシステムを構築することが求められる．並列に動作するシステムでは，複数の事象が並列に発生するので，同時に発生する事象を考慮する必要がある．この並列事象の同時性を正しく認識できないことはシステム障害（failure）の原因となる．このようなシステムの信頼性を高めるためには，従来のテスト技術だけでは十分ではない．本研究では，並列事象の同時性を区間に局所化した「区間振る舞いモデル」を提案し，並列事象の同時性を並行システムとして実現するさいの振る舞い仕様の記述法とその検証法を体系化することにより，形式検証技術の実用化を目指す．
|
| 研究成果の概要 |
IoTシステムでは複数のものが並列に動作するので，同時に起こる事象を考慮する必要がある．この事象の同時性を正しく認識できないことがシステム障害（failure）の原因となりうる．並列システムの正しさをテストだけを用いて保証することは難しい．システムの設計段階において，事象の同時性を含んだる舞い仕様の記述法とその検証法を体系化することにより，並列システムの設計品質の向上に寄与することが期待できる．
|
| 研究成果の学術的意義や社会的意義 |
並行システムの振る舞いの記述・検証のための言語としてプロセス代数では，事象の同時性を表現するためのステップ意味論などが理論的な研究は行われているが，同時性を考慮した振る舞い仕様の設計方法に関する研究成果はまだない．本研究では，事象の同時性を区間として局所化した構造を定式化して，その意味を既存のモデル検査を有するプロセス代数で定義することにより，事象の同時性を考慮した開発環境の基礎を築く．
|
