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

多値モデル検査法を用いたモデリング・エラーの発見

使用多值模型检查查找建模错误

基本信息

批准号：
20650003
负责人：
亀山幸義
金额：
$ 1.92万
依托单位：
University of Tsukuba
依托单位国家：
日本
项目类别：
Grant-in-Aid for Challenging Exploratory Research
财政年份：
2008
资助国家：
日本
起止时间：
2008 至 2009
项目状态：
已结题

项目摘要

本研究は、モデル検査法を用いたシステム設計検証において、しばしば問題となる「モデル化の誤り(モデリング・エラー)」を発見する手法の研究を行うものである。モデル化に誤りがあるときは、仮にモデル検査器が「検証成功」という結果を出力をしても、システム設計が正しいことは保証されないため、これは深刻な問題である。本研究の中心となるアイディアは、「検証成功」という結果になったときに、モデルの一部を意図的に変更し、「検証失敗」となる限界モデルを探索することにより、モデリング・エラーの原因を探るというものである。今年度の研究では、昨年度の研究で構築した多値モデル検査のアルゴリズムを改良し、Quasi-Boolean Algebraに適用できるようにした。また、多値モデル検査の理論的基礎について、従来手法を一般化した定式化とそれに対するシミュレーション定理を証明し、多値モデル検査の効率化に対して理論的根拠を与えることに成功した。さらに、昨年度のアルゴリズムに対して実装上の改良をおこない、いくつかの具体例に対して、モデリング・エラーの発見を行う実験を行い、一定の条件のもとでは、本研究の手法で効率的なモデリング・エラー発見が可能であることがわかった。これらについては、後日、成果をまとめた論文を発表する予定である。関連研究として、「検証失敗からの情報の取得」という点で類似している型推論アルゴリズムにおける型エラーについての考察を行い、より良い失敗情報の取得を行うためのアルゴリズムの設計、開発を行った。

This study aims to explore the methodology for developing the problem of "error detection" in design and verification by using the model detection method. The test results of the test are correct, and the test results of the test are correct. The center of this study is to explore the reasons for the failure of identification and the failure of identification. This year's research is different from last year's research. It builds a multi-value database to improve the application of Quasi-Boolean. The theoretical basis of multi-value analysis is generalized, formulated and proved. The theoretical basis of multi-value analysis is successfully proved. In addition, the improvement of the equipment in the past year has been carried out under certain conditions, and the method of this study is possible to improve the efficiency of equipment. The results of this study are set out in the following paragraphs. Correlative research: "Failure to verify information acquisition": similar type inference: failure type inference: failure type