• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

分散システムのための代数仕様記述と検証に関する研究

Research Project

Project/Area Number 11780207
Research Category

Grant-in-Aid for Encouragement of Young Scientists (A)

Allocation TypeSingle-year Grants
Research Field 計算機科学
Research InstitutionJapan Advanced Institute of Science and Technology

Principal Investigator

森 彰  北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30311682)

Project Period (FY) 1999 – 2000
Project Status Completed (Fiscal Year 2000)
Budget Amount *help
¥2,100,000 (Direct Cost: ¥2,100,000)
Fiscal Year 2000: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 1999: ¥1,300,000 (Direct Cost: ¥1,300,000)
Keywords分散システム / 振舞仕様 / 隠蔽代数 / 安全性 / モデル検査 / 無限状態 / 定理証明 / 形式仕様
Research Abstract

今年度の研究の目的は,前年度の研究で発見された安全性モデル検査手続きに厳密な定式化を与え,これをセキュリティや実時間システムの問題に適用できるよう,新たな仕様記述の仕組みを明らかにすることであった.安全性モデル検査については,隠蔽代数を用いて記述された分散システムの振舞仕様を(無限)状態遷移機械の定義とみなし,システムの状態を隠蔽ソート上の述語として表現する述語抽象の考え方を定式化するに至った.これによって,プログラム検証において扱われて来た述語変換の手法が利用できるようになり,モデル検査とプログラム検証の関係が明らかになった点が意義深いものであった.この述語変換を用いた最小不動点の繰り返し計算として安全性モデル検査を定式化し,定理証明を用いた述語間の含意証明による収束判定を用いた繰り返し手続きとして簡潔な定義を与えることができた.そして,代数仕様システムCafeOBJ上で新たに自動定理証明器PigNoseを開発し,このモデル検査手続きを利用できるようにした.ユーザーはCafeOBJによる仕様と検査したい安全性述語を定義するだけでよく,他の類似システムにあるような構文変換や時相論理式による検証条件の記述が不要であることから,無限状態システムを対象としたモデル検査器として他に類をみないものとなった.さらに移動コードの仕様を,コード実行の操作的意味と安全性検査機構をまとめた抽象機械として定義することで,どのようなコード体系であっても安全性検査が可能であるとの知見を得た.実時間システムにおいては,大域時間を示す属性と時間進行のための操作を定義し,状態変化に伴い最大遅延や最小遅延といった時間制約の属性をセットすることで,安全性が検査できることが確認できた.また本研究では,仕様記述とその検証に同一の論理体系が用いられていることから,対話的検証に対する有効性も確認することができた.

Report

(2 results)
  • 2000 Annual Research Report
  • 1999 Annual Research Report
  • Research Products

    (4 results)

All Other

All Publications (4 results)

  • [Publications] 森彰: "開放型分散環境でのソフトウェア部品検証システムの研究開発"第19回IPA技術発表会論文集. 27-35 (2000)

    • Related Report
      2000 Annual Research Report
  • [Publications] Joseph Goguen: "An Overview of Tatami Project"CAFE : An Industiral-Strength Algebraic Formal Method. 61-78 (2000)

    • Related Report
      2000 Annual Research Report
  • [Publications] Akira Mori: "Verifying Behavioural Specifications in CafeOBJ Environment"Lecture Notes in Computer Science. 1709. 1625-1643 (1999)

    • Related Report
      1999 Annual Research Report
  • [Publications] 海野 浩: "振舞仕様による通信処理システムの記述法について"レクチャーノート/ソフトウェア学 ソフトウェア工学の基礎VI. 22. 172-179 (1999)

    • Related Report
      1999 Annual Research Report

URL: 

Published: 1999-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi