2021 Fiscal Year Annual Research Report
アーキテクチャに基づく区間振る舞いモデルを用いた記述法と形式検証法
| Project/Area Number |
19K11911
|
|---|
| Research Institution | Nanzan University |
|---|
Principal Investigator |
張 漢明 南山大学, 理工学部, 准教授 (90329756)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
野呂 昌満 南山大学, 理工学部, 教授 (40189452)
沢田 篤史 南山大学, 理工学部, 教授 (40273841)
|
|---|
| Project Period (FY) |
2019-04-01 – 2022-03-31
|
| Keywords | 並列システム / イベントの同時性 / プロセス代数 / CSP |
|---|
| Outline of Annual Research Achievements |
組込システムやIoTシステムなどの並列システムのソフトウェア開発では，事象の同時性を考慮することが必然である．本研究では，並列事象の同時性を区間に局所化した「区間振る舞いモデル」を提案し，並列事象の同時性を並行システムとして実現するさいの振る舞い仕様の記述法とその検証法を体系化することを目指した．
本年度は、研究課題(c) 振る舞いの正当性検証手法の開発および研究課題(d) 仕様記述・検証プロセスおよび検証支援環境の構築，について研究を進めた．正当性の検証は、実用性の観点から既存のCSPモデル検査ツールFDRの利用を前提として、区間振る舞いモデルを洗練した．プロセスを同時イベント記述のための1級エージェントとすることで，プロセスの合成演算子を統一的に扱うことが可能となる．同時事象を開始事象と終了事象を付加した事象の集合とし，その意味をCSPで記述することにより，既存ツールを用いた同時事象の扱いを可能にした．検証支援環境の一環として，誤り記述とその軌跡の間を対応づけたフォールトパターンに関する研究を行った．対象を限定した正しいシステム記述から典型的な誤りを想定することにより，軌跡のパターンから誤りを特定する方法を検討した．並行システムでは，プロセスのコンテキストスイッチが非決定的に切り替わるので，検討すべき動作履歴は単一プロセスに比べて複雑である．フォールトパタンは，開発者の経験に依存する並行システム記述のデバッグを系統的に行う技術として期待できる．
今後の課題として，実用的な並列システム開発における有効性を検討する必要がある．大規模システム開発では，モジュール化とモジュールの合成技術が不可欠である．また，図式表現による直感的な記述も必要となる．図式表現と形式表現を用いたフォーマルとセミフォーマルの統合環境の整備が求められる．
|
Research Products
(5 results)
