| 研究課題/領域番号 |
19K11911
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 南山大学 |
|---|
研究代表者 |
張 漢明 南山大学, 理工学部, 准教授 (90329756)
|
|---|
| 研究分担者 |
野呂 昌満 南山大学, 理工学部, 教授 (40189452)
沢田 篤史 南山大学, 理工学部, 教授 (40273841)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2022-03-31
|
| キーワード | 形式手法 / 形式仕様 / 形式仕様言語 / モデル検査 / ソフトウェアアーキテクチャ |
|---|
| 研究成果の概要 |
IoTシステムでは複数のものが並列に動作するので，同時に起こる事象を考慮する必要がある．この事象の同時性を正しく認識できないことがシステム障害（failure）の原因となりうる．並列システムの正しさをテストだけを用いて保証することは難しい．システムの設計段階において，事象の同時性を含んだる舞い仕様の記述法とその検証法を体系化することにより，並列システムの設計品質の向上に寄与することが期待できる．
|
| 自由記述の分野 |
形式手法に基づくソフトウェア開発手法
|
| 研究成果の学術的意義や社会的意義 |
並行システムの振る舞いの記述・検証のための言語としてプロセス代数では，事象の同時性を表現するためのステップ意味論などが理論的な研究は行われているが，同時性を考慮した振る舞い仕様の設計方法に関する研究成果はまだない．本研究では，事象の同時性を区間として局所化した構造を定式化して，その意味を既存のモデル検査を有するプロセス代数で定義することにより，事象の同時性を考慮した開発環境の基礎を築く．
|
