実現不能な仕様の欠陥情報を用いて部分プログラムを合成する方法に関する研究

2000 Fiscal Year Annual Research Report

• Project/Area Number: 12780194
• Research Institution: Tokyo Institute of Technology
• Principal Investigator: 友石 正彦 東京工業大学, 大学院・情報理工学研究科, 助手 (60262284)
• Keywords: リアクティブシステム / 実現可能性 / プログラム化可能性 / 時間論理 / プログラム合成

Research Abstract

本年度は、実現不能な仕様の欠陥情報を用いて部分プログラムを合成するための基礎として、欠陥情報の検出方式の形式化を行なった。
●仕様の充足不能性を効率的に検証する手続きとして、前段階での検証時に生成したタブローを用いて現段階での検証を行なう発展型のタブロー法の構成を行なった。充足不能性は実現可能な仕様が満たすべき性質の中でも基本的なものである。
●有限フレームを意味とする様相論理に特化した分解証明法の構成を行なった。ここでの様相論理はシステムが止ることをフレームの制約として持つものである。この論理と通常の時間論理の証明システムにおいては、無限状態列をどのように標準化して検証を行なうかという共通の問題がある。本研究においては、無限列に対する無矛盾性の判定を、(標準化された)有限列の繰り返しに対する無矛盾性判定で行なえることの正当性が示され、その標準化モデルに基づく証明法が示された。
●メールの中継のためのリアクティブシステムの実装を実際に行なった。これは、ファイアーウォールを導入したネットワークにおいて、出先でのユーザに対して安全かつ利便なメール送信のためのシステムを提供するものである。
ここで取り扱われる中継のためのプロトコルは単純なので、本研究での仕様と検証における実例として使いたいと考えている。

Research Products

• [Publications] M.Tomoishi,N.Yonezaki: "Evolutional Tableau Method for Temporal Logic Specifications"International Symposium on Principles of Software Evolution. 176-183 (2000)
• [Publications] 萩原茂樹,友石正彦,米崎直樹: "有限フレームを意味的基礎として持つ様相論理に対する分解証明法"日本ソフトウェア科学会論文誌別冊「ソフトウェア発展」. 78-91 (2000)
• [Publications] 増井健司,友石正彦,米崎直樹: "リレーサーバを用いたpop before smtpのセキュアな実現法とその解析"日本ソフトウェア科学会第17回大会論文集(online). (2000)