2019 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 |
|---|
| Outline of Annual Research Achievements |
高度に情報化されたネットワーク社会では，異なったシステムを統合して信頼性の高いシステムの構築が求められる．並列事象の同時性を正しく認識できないことはシステム障害（failure）の原因となる．本研究では，並列事象の同時性を区間に局所化した「区間振る舞いモデル」を提案し，並列事象の同時性を並行システムとして実現するさいの振る舞い仕様の記述法とその検証法を体系化することを目指している．本年度は，組み込みシステムを題材として「区間振る舞いモデルの定式化」および「アーキテクチャの振る舞いモデルの定式化」の研究課題について重点的に取り組んだ．
IoTの利便性を向上させるためには，多様な環境においてアプリケーションを稼働させることのできる相互運用性が重要である．IoTにおける柔軟性と相互運用性の確保をソフトウェア構造の問題と捉え，スマートホームでの動的適応を可能とするアプリケーションアーキテクチャを定義して，柔軟で相互運用可能なアプリケーションを保守しやすく構築する基盤としてのアーキテクチャを提案した．
組み込みシステムにおいて，アクチュエータ群の挙動は，センサの検知する値やシステムの状態に応じて変化し，この組み合わせが増えればシステム全体の挙動は複雑になる．複雑な挙動は，それを仕様化する際に誤りの混入を招き，デッドロックなどの問題の原因となる．このような複雑な挙動を持つ組み込みシステムの開発を支援するために，ソフトウェアアーキテクチャに基づく設計法を提案した．組み込みシステムにおける関心事を明確に分離したアーキテクチャに基づいて，形式的に仕様を記述するための手順を示した．また，形式仕様のメタモデルを構築するために，対象に対する視点として「機能」と「振る舞い」に着目し，MVCアーキテクチャに基づいて仕様の構造を整理した．
|
| 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) 仕様記述・検証プロセスおよび検証支援環境の構築，の研究課題に対して(a)および(b)を重点的に取り組んだ．
組み込みソフトウェア開発において，開発文書の品質を向上するために形式仕様の導入は必要不可欠である．形式仕様には形式言語毎にそれぞれ特性があり，記述したい視点に応じて適切な形式言語を選択する必要がある．組み込みシステムでは，タイミング図を用いた記述が利用される．タイミング図を用いて適切な仕様を記述もしくは抽出することができれば，慣れた記述法を用いて仕様を記述することが可能になる．本研究では，ソフトウェア開発技術者に対して，形式仕様の適切な記法を提供するための形式仕様のメタモデルを提案した．形式仕様は，仕様を記述するための自然言語表現，図式表現，表形式表現の代替表現とみなすことができる．形式仕様の表現として，代数仕様，状態規範型仕様，プロセス代数仕様を分析の対象とした．形式仕様のメタモデルにより，研究課題(a)および(b)については概ね目標を達成できたと考えられる．形式仕様のモデルを基盤として，機能および振る舞い仕様に対する検証方法を提示することが今後の重点課題である．
|
| Strategy for Future Research Activity |
今年度の成果を踏まえて，研究課題(c) 振る舞いの正当性検証手法の開発．(d) 仕様記述・検証プロセスおよび検証支援環境の構築，について研究を進める．
「振る舞いの正当性検証手法の開発」では，振る舞い仕様がアーキテクチャで構成された振る舞いを満たすことを検証するための検証式の自動生成を目指す．CSPのモデル検査器FDRでは詳細化関係（Refinement）を用いて検証する．詳細化関係を用いた検証の課題は，着目する事象，並行合成するさいの同期事象，隠蔽する事象の指定を適切に行うことである．安全性と活性の検証および目的に応じた検証を分析して，検証式をパターン化することにより検証式の自動生成を図る．
「仕様記述・検証プロセスおよび検証支援環境の構築」では，仕様記述・検証プロセスを定式化し，仕様記述と検証を支援する環境を開発する．振る舞い仕様記述の課題は，システムの振る舞いを区間に分割する方法である．アーキテクチャの記述から同時に事象が発生する箇所を分析する手法を考案する．区間内を事象の発生を網羅的かつ排他的な場合分けを行う方法を提示する．振る舞い記述の段階的な記述として，抽象的で簡易な非決定的な振る舞い記述とより具体的な決定的な振る舞い記述法を提示する．
また，検証時の課題として，検証失敗時における反例の分析が挙げられる．本研究の事例検証を通して，典型的な誤りを集積して分析することによりフォールトパターンとして提示することによりデバッグの支援を図る．図式表現はUMLの記述を基本として表現の拡張を検討する．ツール支援では，表記法の修正・変更が想定される．これらの変更に柔軟に対応することができるツールのアーキテクチャを検討する．
|
| Causes of Carryover |
今年度予定ていたWindows上で動作する形式検証ツールの利用が次年度に変更となったので，形式検証ツール用のWindowsPCの購入を次年度に繰り越した．
|
Research Products
(3 results)
