|
JAIST Repository >
School of Information Science >
Grants-in-aid for Scientific Research Papers >
FY 2008 >
Please use this identifier to cite or link to this item:
https://hdl.handle.net/10119/8459
|
| Title: | 証明支援系とモデル検査器を効果的に利用できる環境と方法論 |
| Other Titles: | Methodology and Environment for Effectively Using Theorem Provers and Model Checkers |
| Authors: | 緒方, 和博 |
| Authors(alternative): | OGATA, KAZUHIRO |
| Keywords: | 仕様記述
仕様検証
モデル検査
仕様変換
観測遷移システム
CafeOBJ
Maude
メタプログラミング |
| Issue Date: | 10-Apr-2009 |
| Abstract: | 証明支援系とモデル検査器を効果的に利用できるよう、定理証明向きのシステム仕様をモデル検査向きのシステム仕様に自動変換する方法を考案した。変換により、モデル検査向きのシステム仕様が大きくなりすぎて効果的にモデル検査ができなくなることを防ぐための工夫を行った。提案した変換方法の有効性を確認するため、電子商取引プロトコルiKPとMondexの検証実験に適用した。また、変換を支援する変換ツールの拡張性の高い実装方法も提案した。この実装方法では、複数の変換規則をモジュラーに組み入れることを可能にする。 |
| Description: | 研究種目：基盤研究（Ｃ）
研究期間：2006～2008
課題番号：18500019
研究者番号：30272991
研究分野：形式手法
科研費の分科・細目：情報学・ソフトウエア |
| Language: | jpn |
| URI: | https://hdl.handle.net/10119/8459 |
| Appears in Collections: | 2008年度 (FY 2008)
|
Files in This Item:
| File |
Description |
Size | Format |
|---|
| 18500019seika.pdf | | 185Kb | Adobe PDF | View/Open |
|
All items in DSpace are protected by copyright, with all rights reserved.
|
