検証を考慮した仕様記述の指針に関する研究
スポンサーリンク
概要
- 論文の詳細を見る
代数仕様言語は,仕様が実行可能であるという特徴を利用して,仕様をプロトタイプと見倣せたり,検証の半自動化を実現できる.しかし,代数仕様言語が実用に供するには,モジュールを効率よく扱え書換え速度が高速な処理系が必要である.本研究では,実行効率のよい代数仕様言語CafeOBJの処理系を作成し,その処理系が正しく動くことを示すために,以下のことを行った.CafeOBJのモジュールシステムの要求と設計をCafeOBJを用いて記述し,設計が要求を満たしていることを振舞等価の概念を用いて示した.そしてこの仕様記述および検証で得られた仕様記述の際に得られた知見をまとめた.
- 社団法人電子情報通信学会の論文
- 1999-11-12
著者
-
五百蔵 重典
神奈川工科大学情報学部
-
緒方 和博
北陸先端科学技術大学院大学情報科学研究科
-
二木 厚吉
北陸先端科学技術大学院大学情報科学研究科
-
五百蔵 重典
北陸先端科学技術大学院大学情報科学研究科 : (現)神奈川工科大学
-
五百蔵 重典
神奈川工科大学 情報工学科
-
緒方 和博
北陸先端科学技術大学院大学
-
五百蔵 重典
神奈川工科大学 情報学部 情報工学科
-
五百蔵 重典
神奈川工科大
関連論文
- アクティブタグを用いた群衆の嗜好に応じた広告情報提示法に関する一検討 (ユビキタス・センサネットワーク)
- GPS携帯を用いた場所にリンクした情報共有システムの設計と基本評価(セッション携帯端末/センターネット)
- F-013 AIBOによる室内確認システムの検討(F分野:人工知能・ゲーム)
- ソフトウェア科学会第3回大会
- 代数仕様に基づく実時間システムの検証
- B-2 代数仕様言語CafeOBJにおけるモデル検査(プログラムの理論,B.ソフトウェア)
- B-20-27 ウェアラブル加速度センサを用いた操作動作の開始判断手法(B-20.ユビキタス・センサネットワーク,一般セッション)
- D-12-54 加速度センサを用いたローマ字による日本語文字入力方法の提案(D-12.パターン認識・メディア理解,一般セッション)
- B-20-55 超音波測位システムにおける同期誤差の測定と評価(B-20.ユビキタス・センサネットワーク,一般セッション)
- B-20-54 超音波を用いた位置検出における同期誤差シミュレーション(B-20.ユビキタス・センサネットワーク,一般セッション)
- B-20-26 加速度センサを用いた動作認識における認識前処理の効果の検討(B-20.ユビキタス・センサネットワーク,一般セッション)
- B-3-1 逆GPS法を用いた屋内測位システムの基本実験(B-3.衛星通信,一般セッション)
- B-20-10 曖昧さを持つ動作の認識率向上に関する一検討 : 動作認識による周辺機器の操作性向上を目的として(B-20.ユビキタス・センサネットワーク,一般セッション)
- B-7-97 超音波を用いた広域屋内位置特定法に関する基本検討(B-7.情報ネットワーク,一般セッション)
- B-20-44 ウェアラブル加速度センサを用いた周辺機器操作の基本検討(B-20.ユビキタス・センサネットワーク,一般セッション)
- B-20-45 3軸加速度センサを用いた動作認識に関する基本検討(B-20.ユビキタス・センサネットワーク,一般セッション)
- GPS情報を利用した知的環境構成の一実証 : モバイルネットワークと家電ネットワークを統合したエアコン制御を例として(無線分散ネットワーク(WDN)特集セッション及び一般講演)
- AS-3-3 代数仕様に基づく実時間システムの検証(AS-3.コンカレントシステム理論の最近の発展とその応用,シンポジウムセッション)
- B-20-36 遮蔽によるアクティブRFIDの受信強度変化を利用した状態検知方式(B-20. ユビキタス・センサネットワーク,一般セッション)
- 電子社会と法令工学(法情報学最前線)
- パネル討論会 : 理輪は実践を導けるか,実践は理論を生かせるか? : 第1回プログラミング : 言語・基礎・実践 研究会報告
- ET2009-119 携帯電話を用いたリアルタイム授業支援システムの開発(障害者教育・特別支援教育/一般)
- 地上網と衛星システムを用いた情報収集・共有システムの提案と基本実験(衛星応用技術及び一般)
- アクティブタグを用いた群衆の嗜好に応じた広告情報提示法に関する一検討(モバイル P2P,ユビキタスネットワーク,アドホックネットワーク,センサネットワーク,一般)
- 超音波を用いた屋内測位システムにおける広域化と複数対象識別法の検討と実証
- ウェアラブル加速度センサを用いた動作認識による周辺機器操作のアーキテクチャの提案と実証(ユビキタス・センサネットワークの要素技術,コンテクストの抽出,スマートスペース,ユビキタス生活支援,一般)
- B-20-33 Android端末を用いた遠隔操作アーキテクチャの提案(B-20.ユビキタス・センサネットワーク,一般セッション)
- 項書換えコンパイラに関する一考察
- 項書換え系に基づく定理証明支援環境の構築
- 項書換え抽象機械における組み込み演算の処理
- 実行可能な形式仕様言語CafeOBJ(4) : CafeOBJによるZ仕様のアニメーションの枠組み
- 実行可能な形式仕様言語cafeOBJ(3) : CafeOBJによるオブジェクト指向システムの仕様記述ライブラリの記述
- 実行可能な形式仕様言語CafeOBJ(2) : Cafeシステムの核アーキテクチャ
- 実行可能な形式仕様言語CafeOBJ(1) : CafeOBJの宣言的意味論
- 振舞仕様に基づくシステムの記述方法
- 代数仕様言語OBJによる並行分散システムの形式仕様作成法
- RB-003 An algebraic specification of message passing programming languages
- CafeOBJ入門(6) : 通信プロトコルの検証
- CafeOBJ入門(5) : 認証プロトコルの検証
- CafeOBJ入門(4) : 証明譜による検証法(エージェント)
- CafeOBJ入門(3) : 等式推論と項書換システム
- Maude : 書換え論理に基づく計算機言語および処理系(ソフトウェア紹介)
- CafeOBJ入門(2) : 構文と意味
- CafeOBJ入門(1) : 形式手法とCafeOBJ
- LA-008 実行可能な代数仕様の停止性証明について(モデル・アルゴリズム・プログラミング)
- モジュラーな代数仕様言語のための項書き換えシステム(システム検証の科学技術)
- OTS/CafeOBJからOTS/Maudeへの仕様変換の研究
- 項書き換えシステムにおける可簡約演算子とその応用
- 項書き換えシステムにおける可簡約演算子とその応用
- STSプロトコルの形式化と検証によるCafeOBJとCoqの比較
- B-036 代数仕様言語CafeOBJと証明支援系CoqによるSTSプロトコルの形式化と検証(B.ソフトウェア)
- B-034 隠蔽代数に基づく命令型プログラム言語の意味論の記述と検証(B.ソフトウェア)
- LA-005 項書換えシステムにおける可簡約演算子とその応用(A. モデル・アルゴリズム・プログラミング)
- B-1 代数仕様言語CafeOBJのための拡張可能な前処理系(プログラムの理論,B.ソフトウェア)
- 項書換え抽象機械TRAMの設計と実装
- 検証を考慮した仕様記述の指針に関する研究
- 検証を考慮した仕様記述の指針に関する研究
- モジュールシステムの要求仕様と設計仕様
- モジュールシステムを備える書換え抽象機械の提案
- 超並列項書換えシステムの実装と評価
- 超並列項書換えシステムの実装と評価
- 超並列項書換えシステムの実装と評価(並列・分散)
- 代数仕様によるZ仕様の検証支援
- CafeOBJによるプロセス記述ライブラリの作成
- CafeOBJによるODPトレーダ仕様の記述
- B-20-1 超音波を用いた屋内測位システムにおける複数対象測位法の検討(B-20.ユビキタス・センサネットワーク,一般セッション)
- M-054 超音波を用いた屋内測位システムにおける測位誤差要因とその評価(M分野:ユビキタス・モバイルコンピューティング,一般論文)
- M-026 超音波測位システム開発のための測位誤差シミュレーション(ユビキタス・モバイルコンピューティング,一般論文)
- B-035 Provably Correct Translation from OTS/CafeOBJ Specifications to Java Programs
- 項書換えを用いた安全性検証の組織化(ソフトウェア工学の基礎)
- 代数仕様言語CafeOBJによる実時間システムの仕様記述と検証の一例 : timed two-process raceの仕様記述と検証
- 代数仕様言語CafeOBJにおける高信頼システムの記述に関する一考察
- Java仮想機械の形式仕様
- テスト集合余帰納法を用いた振舞等式の検証
- 高信頼コンポーネントソフトウェアの開発支援ツール
- コンポーネントソフトウェア開発用軽量フォーマルメソッド
- 振舞意味論を用いた詳細化検証 : オブジェクト合成と非観測射影演算を用いた新しいアプローチ
- 振舞意味論に基づく仕様の検証法
- 並列分散システムへの振舞意味論の適用について
- 振舞意味論と投影演算に基づく並行システムのノンインターリーブ性の記述および詳細化検証
- 項書換えシステムのための抽象機械の設計について
- B-7-98 キャッシュするデータをファイル種別で選別するキャッシュ方式の提案(B-7. 情報ネットワーク,一般セッション)
- B-20-7 FPGAを用いた超音波測位システムの広域化に関する検討(B-20.ユビキタス・センサネットワーク,一般セッション)
- B-20-6 超音波測位システムの屋内歩行者向けナビゲーションへの適用に関する検討(B-20.ユビキタス・センサネットワーク,一般セッション)
- IC旅券等のIC身分証明書を利用した仮想会員証運用システムの提案(セッション5: グループウェアアプリケーション)
- IC旅券等のIC身分証明書を利用した仮想会員証運用システムの提案(セッション5: グループウェアアプリケーション)
- D-9-17 ケータイを利用した防犯情報共有システムの検討 : 厚木市森の里四丁目/地域の目・防犯ネットワークの構成(D-9.ライフインテリジェンスとオフィス情報システム,一般セッション)
- 携帯電話を用いたリアルタイム授業支援システムの開発
- 書き換え理論に基づく有機的プログラミング言語GAEAの意味
- A-15-19 まばたきによる筋電位変化を用いた入力インタフェースの検討(A-15.ヒューマン情報処理,一般セッション)
- 文脈依存書き換えの拡張
- 書き換えによるセキュリティプロトコル帰納的検証(セキュアコンピューティング)
- CafeOBJによる分散システムの形式仕様作成法
- 形式仕様言語CafeOBJを用いたテキストエディタの仕様記述
- 順序ソート項書換えの効率のよい実現に関する一考察
- プログラム合成/変換特集の編集にあたって (プログラム合成/変換)
- 特集「非手続き型プログラミングのための計算モデル」の編集にあたって
- 並行項書き換え計算による並行オブジェクト指向言語の実現
- 有限状態機械に基づくプログラミングでのgoto文使用の是非 : Hoare論理の観点から(プログラミングの理論)
- 多重ループからの脱出でのgoto文の是非 : Hoare理論の観点から(プログラミング方法論とパラダイム)