| 研究課題/領域番号 |
07680341
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
米崎 直樹 東京工業大学, 大学院・情報理工学研究科, 教授 (00126286)
|
|---|
| 研究分担者 |
友石 正彦 東京工業大学, 大学院・情報理工学研究科, 助手 (60262284)
|
|---|
| キーワード | 実時間ソフトウェア / 仕様記述 / 検証方式 / 時間論理 / 実時間論理 / 線形論理 / 適切さの論理 |
|---|
| 研究概要 |
以下の各項目につき研究成果を得た。
1.時間領域の違いによる証明体系の研究
離散性を持つ体系に対する、結合法をベースとした様相記号列の統一化による証明方法を考案した。この方法では、統一化に自己代入を許すとともに、式の無限個の複製を表す記号を導入した。また、すでに提案した実時間システムの検証を目的する実時間を記述可能な論理RTLを基にし、RTLの意味論を保存して有理数時間に制限したRTL^Qについて公理系を提案し、その弱完全性の証明方法について研究を行った。
2.線型論理の意味論に関する研究
様相演算子まで含む命題線形論理CLL_eに対し、モデルを基にした、直感的にわかりやすい意味論を与えた。式を命題の要求と供給と見ることで原始命題の収支に着目し、この収支をモデルで表現した。このモデルでは、様相演算子はその式が無限にあることを表現している。そしてモデルと式との間の命題の収支を計算することで、式に真偽値を割り当てている。
3.発展的検証方法に関する研究
新たな構造を持ったタブローグラフとその構成方法を導入することで、部分仕様について検証済みの情報を全体仕様の検証に再利用可能なタブロ-法を提案した。特に、線形離散時間フレームにおけるモデルチェッキングの手続きにおいてグラフ生成とは別に必要な「イベンチャリティを確認する手続き」の代わりに、確認した結果の情報も反映したタブローグラフを直接構成可能な構造を与えた。
4.仕様からの適切な情報を推論する論理体系に関する研究
仕様として記述された論理式から、人間にとって意味ある式のみを演繹することは、仕様を検査し過ちを発見しやすくするために重要である。このためにすでに結合子の適切さを考慮した新しい論理ERを構築していたが、本年はこの体系を基に結合子の適切さも考慮した体系LRCを構築し、その性質について論じた。
5.仕様の分類とその判定方法に関する研究
リアクティブシステムの仕様記述について、その実現可能性に至るいくつかのクラスを分類しその性質について論じた。このクラス分けは、欠陥のある仕様を実現可能な仕様に修正してゆく過程において、仕様記述者に対して、より詳細な情報を与える。また、仕様がそのクラスに属するか否かに関する判定アルゴリズムをその正しさの証明とともに与えた。
|
