权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

分布式系统代数规约描述与验证研究

基本信息

批准号：
11780207
负责人：
森彰
金额：
$ 1.34万
依托单位：
Japan Advanced Institute of Science and Technology
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
1999
资助国家：
日本
起止时间：
1999 至 2000
项目状态：
已结题

项目摘要

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

The purpose of this year's research is to formalize the safety monitoring procedures discovered in the previous year's research so that they can be applied to both basic and real-time issues, and to clarify the composition of new official descriptions. Safety test, test The relationship between these two types of documents is clear and meaningful. The minimum fixed point is calculated and the safety is determined. The theorem is proved and the meaning is proved. The bundle is determined and the definition is simplified. In this paper, we introduce a new automatic theorem prover named PigNose on CafeOBJ. The security term is defined by the CafeOBJ, and the security term is defined by the CafeOBJ, and the security term is defined by the CafeOBJ, and the security term is defined by the CafeOBJ, and the security term is defined by the CafeOBJ. The meaning of the operation of the mobile phone and the knowledge of the safety inspection mechanism are obtained. Time is the attribute of time in progress. The operation of time in progress is defined. The state is changed with maximum delay and minimum delay. The attribute of time restriction is checked. The security is confirmed. This paper describes the application of the same logic system to the identification of the problem.