実時間ソフトウェアの仕様記述とその検証方式の研究

1996 年度 実績報告書

• 研究課題/領域番号: 07680341
• 研究種目: 基盤研究(C)
• 研究機関: 東京工業大学
• 研究代表者: 米崎 直樹 東京工業大学, 大学院・情報理工学研究科, 教授 (00126286)
• 研究分担者: 友石 正彦 東京工業大学, 大学院・情報理工学研究科, 助手 (60262284)
• キーワード: 実時間ソフトウェア / 仕様記述 / 検証方式 / 時間論理 / 実時間論理 / 線形論理 / 適切さの論理

研究概要

平成8年度の成果は以下のようにまとめられる。
・効率的証明体系の研究(米崎、友石)
実時間論理は、その恒真性判定問題が決定可能な場合でも、計算の複雑さが指数関数を越えるオーダーになることがほとんどである。しかし、このことは必ずしも実用性が無いことを意味してはいない。すべての式に対して効率的でなくとも、意味のある式のクラスに対して効率の良い証明方法があれば、実時間論理の表現力をいかした仕様記述、仕様検証が可能となる。そこで、これまでに研究して来た様相記号列の統一化による証明方法を時間論理について拡張し、その証明のヒューリスティクスに対して理論的基礎を与えた。具体的には、タブロ-法などで必要な、ループの検査を代替するような自己代入を用いる統一化の新しいスキーマを与えた。
・仕様記述のための形式言語に関する研究(友石、米崎)
新たな適切さの論理を提案し、仕様記述から有用な情報のみを推論する方法について考察した。具体的には、ラベル付き演繹システムを用いることで、有用な情報が効果的に推論可能となり、含意以外の結合子に関する新たな適切さを導入することが可能となった。
また、並列処理などの記述に有用とされる線形論理について、直観的に理解しやすい新しい意味論を構築した。この意味論は、これまでに提案された代数的意味論と異なり、式が真となるために必要な命題の個数の情報を持つモデルを用いている。
さらに、これらの論理を用いた仕様記述における、不完全な仕様の検査方法、仕様、検証の再利用方法についてのシステム構築のための検討を行なった。

研究成果

• [文献書誌] Noriaki Yoshiura,Naoki Yonezaki: "Relevant Inference and Reliability Dependent on Implication" Information modelling and knowledge bases. VII. 154-172 (1996)
• [文献書誌] Yoshiaki Minamisawa,Masahiko Tomoishi,Naoki Yonezaki: "Semantics for Linear Logic and its Completeness" The 6th European-Japanese Conference on Information Modelling and Knowledge Bases. (1996)
• [文献書誌] 吉浦紀晃、米崎直樹: "知識推論のための適切さの論理" 日本ソフトウェア科学会第13回大会論文集. 437-440 (1996)
• [文献書誌] 南澤吉昭、米崎直樹: "モデルを用いた線形論理の意味論" 日本ソフトウェア科学会第13回大会論文集. 425-428 (1996)
• [文献書誌] 伊藤裕、友石正彦、米崎直樹: "マルチエージェントプランニングにおけるサブゴールの設定" 第5回マルチエージェントと協調計算ワークショップオンライン論文集http://www.csl.sony.co:jp/personal/nagao/Macc95. (1996)
• [文献書誌] 渡辺治、米崎直樹: "計算論入門" 日本評論社, 211 (1996)