氏名: 加納 康資 (089630661)

論文題目: 振舞仕様記述とその検証法に関する研究


論文概要

ソフトウェアシステムの内部状態は、観測や操作によってアクセスされたり変更され たりする。 従って、ある2つの内部状態に対してあらゆる操作を適用した後に観測した結果が等 しいとき、 その2つの状態は等しいとみなして差し支えない。この意味の等価性をを振舞等価と いう。振 舞仕様記述法は振舞等価の概念に基づいてシステムの振舞を代数的に記述する方法で ある。

本研究では、振舞仕様によって記述されたシステムの性質を検証する方法の1つであ る、余帰 納法(coinduction法)[1]に関する調査研究を行い、大学院博士課程前期進学後の研究 の準備 とする。

振舞等価を証明するためには、すべての観測文脈によるテストをしなければならな い。しかし、 一般的に観測可能文脈は無限に存在するので、等価性証明をするには、何らかの帰納 法が必 要である。そこで振舞等価を一般的にした関係である隠蔽合同を用いるのが、余帰納 法である。 しかしこの余帰納法には、人が自分で隠蔽合同の候補を見つけなければならないとい う欠点が あり、証明の自動化に適していない。そこで、この発見的な部分を解消したものがテ スト集合余 帰納法[4]である。テスト集合余帰納法は、観測文脈全体の集合から必要不可欠な文 脈を選び 出し、それから振舞等価を構成する方法である。 これらの方法は、使える状況が限られており、より一般的な場合にも適用できる方法 としてΔ-coinduction法[2]、Circular-coinduction法[2]が研究されている。これに より、余帰納法に、より 強力な推論規則が追加される。

また、余帰納法が自動的に行える振舞仕様記述の形式に関する研究としてobserver complete definition[3]に関する研究がある。これは仕様の公理がこの形式を満たしていれ ば、証明が簡単 化されるというものである。

以下に挙げる他に10編余の文献を調査している。

(調査文献)

[1] J.Goguen and G.Malcolm : 'A Hidden Agenda',USCD Technical Report CS97- 538,1997.

[2] J.Goguen and G.Malcolm : 'Circular coinduction',Submitted for publication,1999. http://www.cs.ucsd.edu/users/goguen/projs/halg.html

[3] M.Bidoit and R.Hennicker : 'Observer Complete Definitions are Behaviourally Coherent', Reserch Report LSV-99-4,1999.

[4] M.Matsumoto and K.Futatsugi : 'Test Set Coinduction - Toward Automated Verification of Behavioural Properties -',Electronic Notes in Theoretical Computer Science Vol. 15, Elsevier Science, 1998.


目次に戻る


asakura@nuie.nagoya-u.ac.jp