XML文書に対するガイドライン適合性自動検証法の開発

点击翻译按钮获取中文摘要

本研究では,XML文書に関する構文制約(ガイドライン)を記述するための簡明な言語SGSL(Simple Guideline Specification Language)を設計し,与えられたXML文書がSGSLで書かれたガイドラインに適合するかどうか検証するソフトウェアを設計・実装した.SGSLは,XML文書中の要素を特定するための言語であるXPath 1.0に,全称および存在限量子を加えた言語である.本年度は,XPathに関連して昨年度より開始した,XPath式で定義されたアクセス制御ポリシ(XPathで指定した要素に対するアクセスを許可または禁止する)に対し,XPath式で与えられた問い合わせが違反を起こすかどうかを判定する問題(静的解析によるアクセス制御)についてさらに考察した.この問題は,一般の場合は決定性指数時間完全であるが,AND意味論という意味論の下では多項式時間可解である.また,AND意味論で表現可能であるかどうかは決定可能であるが,その判定は一般に決定性指数時間完全であることなどが新たにわかった.また,オートマトン理論に基づくアクセス制御機構の解析に関連して,Abadiらが提案した履歴に基づくアクセス制御機構のモデル化と検証法について研究を行った.その結果,このアクセス制御機構はプッシュダウンシステムによってモデル化できること,従来よく知られていたスタック検査より表現能力が高いこと,モデル検査検証が可能だが決定性指数時間完全であること,などがわかった.