2020 Fiscal Year Research-status 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 / UML |
|---|
| Outline of Annual Research Achievements |
並列に動作するシステムでは，複数の事象が同時に発生する可能性があり，この並列事象の同時性を正しく認識できないことがシステム障害（failure）の原因となる．本研究では，並列事象の同時性を区間に局所化した「区間振る舞いモデル」を提案し，並列事象の同時性を並行システムとして実現するさいの振る舞い仕様の記述法とその検証法を体系化することを目指している．本年度は，「区間振る舞いモデル」に基づいて，UMLを利用した形式仕様の構成法と振る舞い仕様の正当性検証を支援する方法を提示することを目指した．
本研究では，提案する区間振る舞いモデルの「区間の構造」，「CSPによる区間の意味」，「UMLのアクティビティ図による表現」を提示した．区間振る舞いモデルを実用化するためには，抽象度の高い検証可能な振る舞い表現と，直感的な理解を促進するための図式表現が必要である．区間の構造は，同時に起こる判断を区間に限定し，区間の構成に関わる事象だけに事象を限定する．区間の振る舞いはブラックボックス化して，区間内で同時事象を含めた起こり得る入力事象と出力事象を定義する．入力事象と出力事象の関係を抽象化写像を用いて定義する．区間間の関係は，出力事象を用いて表現されるので，入力事象が未定義でも区間間の振る舞いを定義することができる．これが，モデル検査を実用化するための事象の数の削減に寄与する．入力事象と抽象化写像を用いて，詳細な振る舞いを表現することも可能である．
今後の課題として，CSPを用いた形式検証の事例の提示，並列性を備えたプロセス代数との関係があげられる．仕様・設計の段階で振る舞いの性質を検証することは重要である．今後，自動販売機システムと現金自動預払機システムなどの具体的な事例に対して，抽象モデルと具象モデルの記述を行い，詳細化関係の検証を行うことにより，区間振る舞いモデルの実用性を検討する．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究では，並列システムの開発における上流工程の仕様・設計の段階で，事象の同時性を記述・検証する方法を提示することが最も重要な課題の1つである．並列・分散システムでは同時に事象が発生することは本質的に避けられない．高い信頼性が求められるシステムでは，同時に事象が発生することを考慮して，同時事象が発生したさいの仕様を規定し，その仕様が満たされていることを検証する必要がある．本年度は，(a) 区間振る舞いモデルの定式化．(b) アーキテクチャの振る舞いモデルの定式化．(c) 振る舞いの正当性検証手法の開発．(d) 仕様記述・検証プロセスおよび検証支援環境の構築，の研究課題に対して(b)および(c)を重点的に取り組んだ．
アーキテクチャの振る舞いモデルの定式化については，提案する区間振る舞いモデルの「区間の構造」，「CSPによる区間の意味」，「UMLのアクティビティ図による表現」を提示した．区間振る舞いモデルでは，ステップ意味論の記法を取り入れて，事象を集合を用いて表現した．区間は，区間の範囲を規定する開始境界と終了境界，入力事象集合と出力事象集合，および，入力事象集合と出力事象集合間の抽象化写像から構成した．区間は，基本区間を基にして，逐次区間，選択区間，および，並列区間の複合区間から構成される．自動販売機システムと現金自動預払機システムを事例として，区間振る舞いモデルを用いた記述例を示した．
振る舞いの正当性検証手法の開発については，既存のプロセス代数の同時性を調査した．本研究では，区間の区切りを導入することで，事象の同時性についてインターリーブモデルを用いた意味づけを行うことにより，既存の実用的なツールの利用を可能とした．区間の区切りの導入により，仕様の段階で，並行システムを振る舞いの観点から分割とその責務を明示する記述と検証方法の基礎づけを与えた．
|
| Strategy for Future Research Activity |
今年度の成果を踏まえて，研究課題(c) 振る舞いの正当性検証手法の開発．(d) 仕様記述・検証プロセスおよび検証支援環境の構築，について研究を進める．
「振る舞いの正当性検証手法の開発」では，同時性に着目した事象の抽出，および，区間内における抽象化写像を導入することにより，振る舞い仕様の分割と振る舞いの抽象化を可能にした．さらに，プログラムの段階における振る舞いと，区間振る舞いモデルを対応づけることにより，区間振る舞いモデルがプログラムの振る舞いの仕様としての役割を果たし，プログラムの振る舞い検証が可能となる．プログラムの振る舞いをCSPで記述することにより，プログラムの振る舞いと区間振る舞いモデルの対応をCSPで表現し，モデル検査器FDRを用いた検証方法を提示する．
「仕様記述・検証プロセスおよび検証支援環境の構築」では，UMLと区間振る舞いモデルの対応づけを行うことにより，実用的な検証支援環境の構築を目指す．仕様記述者は，使い慣れた図式構文を用いてシステムの振る舞いを記述することができ，一方で，その意味は既存の形式仕様言語で理解することができる．アーキテクチャの記述から，設計および実現段階の記述の間の追跡を可能にして，それらの間の満たすべき条件を提示する．同時に起こる事象を事象の集合として抽象化して概念の形式化することにより，形式的な検証の有用性を議論する．
検証時の課題として，検証失敗時における反例の分析が挙げられる．本研究の事例検証を通して，典型的な誤りを集積して分析することによりフォールトパターンとして提示することによるデバッグの支援を図る．ツール支援では，表記法の修正・変更が想定される．これらの変更に柔軟に対応することができるツールのアーキテクチャを検討する．
|
| Causes of Carryover |
2020年度は，コロナ禍の影響を受けて，研究討議および研究発表を行うために計上していた旅費を使用することができなかった．2021年度も旅費で計上していた予算を使用できなことが予想される．昨年度および今年度で計上していた旅費の予算を，並列計算の実験を行うための計算機整備にあてる予定である．
|
Research Products
(2 results)
