Maudeによる否定を含んだ構造操作意味定義インタプリタと等価性検証器の構築
スポンサーリンク
概要
- 論文の詳細を見る
本稿では,プロセス計算の操作意味を定義するときに一般的に用いられる構造操作意味定義(SOS)によって定義されるラベル付き遷移系を実現するインタプリタを書換え論理の処理系であるMaudeによって実装する.SOS規則の前件に否定を含む場合の充足性検査として,Maudeのメタレベルの探索機能を用いることで,一般的なSOSを解釈するインタプリタを構築する.さらに,SOSから導出されるラベル付き遷移系上での項に対する強双模倣等価性検証器をMaudeによって実装し,SOSによって定義される動作仕様上での等価性判定を行うツールを構築し,否定を含むSOSによって定義されるプロセス計算の例として,HennessyのTPLにおける等価性判定を示す.
- 2009-05-14
著者
-
伴 潤
名古屋大学大学院情報科学研究科
-
今井 敬吾
名古屋大学大学院情報科学研究科
-
結縁 祥治
名古屋大学大学院情報科学研究科
-
結縁 祥治
名古屋大 大学院情報科学研究科
-
Yuen Shoji
Center For Information Media Studies Nagoya University
-
結縁 祥治
名古屋大学 情報科学研究科
-
Yuen Shoji
Graduate School Of Information Science Nagoya University:national Institute Of Informatics
-
YUEN Shoji
Nagoya University
-
結縁 祥治
名古屋大学大学院情報科学研究科/科学技術振興機構さきがけ研究
関連論文
- Maudeによる否定を含んだ構造操作意味定義インタプリタと等価性検証器の構築
- Maudeによる否定を含んだ構造操作意味定義インタプリタと等価性検証器の構築
- 通信プロセスモデルによるAIBO OPEN-Rプログラムのデッドロックフリー解析手法(検証/テストとデバッグ,組込みシステム工学)
- ウインターワークショップ2008・イン・道後開催報告
- Apache Cocoon Flowscriptのモデル検査によるWeb応用プログラムの動作検証
- Haskellのための非同期局所化π計算に基づくネットワークプログラミングフレームワーク
- 通信プロセスに対する文脈変換手法を用いたモデル検査
- テスト等価性に基づいた視覚的LTSモデル操作によるプロセス代数デバッガ
- テスト等価性に基づいた視覚的LTSモデル操作によるプロセス代数デバッガ(並列・分散)
- 正則な実時間通信プロセスに対するテスト擬順序の記号的特性化
- 診断テスト生成に基づくラベル付遷移システムのグラフィカル・デバッガ
- 動的電圧制御システムにおける評価戦略選択に基づく高効率消費エネルギー関数型プログラミング
- 計算資源へのアクセス能力に基づく競合検査とデッドロック検査のための型解析
- 4M-4 細粒度マークアップに基づくカスタマイズ可能なコーディング規約検査器(リーディングプロジェクト e-society:高信頼ソフトウェア・WebWare開発支援システム,一般セッション,リーディングプロジェクト e-society)
- アマゾンバグ防止フレームワークのためのWebアプリケーション双実行モデル
- 時間付きデザインパターンに基づく実時間並行ソフトウェアの開発手法
- 時間付き$\pi$計算における有限プロセスの時間動作抽象化(計算機科学の理論とその応用)
- π計算に対する時間拡張と合同的性質(計算モデル,フォーマルアプローチ論文)
- π計算に基づくプログラミング言語NepiのためのGUI機能
- 時間付きπ計算によるリアルタイムオブジェクト指向言語の形式的記述(オブジェクト指向とWeb技術)
- π計算による優先度継承プロトコルの形式的記述
- 名古屋大学情報メディア教育システムの現状と課題
- 実行履歴にもとづくマルチコア実時間応用プログラムのデバッグモデル
- Webオートマトン : MVCモデルに基づくWebアプリケーションの動作モデル(ディペンダブルソフトウェア)
- FCDGに基づいたコーディングパターン
- ラウンドトリップエンジニアリングを目指したWebアプリケーションのための意味モデル(産学連携論文)
- セッション型に基づく高信頼ネットワークプログラムの関数型言語による実装手法
- 時間オートマトンによる振舞いモデルに基づく高信頼Real-Time Javaコード生成手法
- 時間オートマトンによる振舞いモデルに基づく高信頼 Real-Time Java コード生成手法
- An Approach for Debugging Client Dynamic Web Applications(Network Services)
- プログラムスライシングツールのための共通表現
- 実時間プロセス言語に基づく時間ステートチャートの動作シミュレーション
- NATによる準マルチホーム化技法(次世代のインターネット/分散システムの構築・運用技術)
- 文書間の不整合解消に基づくソフトウエアプロセスのモデル化
- NATによるプライベートネットワークの準マルチホーム化技法
- コレオグラフィに基づく高信頼通信指向GUIプログラミング
- 通信プロセス計算とその時間拡張(システム設計のための形式手法の基礎と応用)
- SCCS動作式に対する unfold 変換によるLTSモデルの効率的な構成法
- SCCS動作式に対するunfold変換によるLTSモデルの効率的な構成法
- 命令を並列に実行するCPUに対するSCCSによるコンパイラの仕様記述
- 計算資源へのアクセス能力に基づく競合検査とデッドロック検査のための型解析
- 「情報処理学会論文誌 : プログラミング」の編集について
- Web オートマトン: MVC モデルに基づくWebアプリケーションの動作モデル
- 否定前件を含む構造操作意味定義に対するプロセス計算コンパイラ
- 並行論理型言語の意味領域としてのガード付きストリーム : 意味論的および構文的同値関係について
- Symbolic Alternative Characterizations of Testing Preorder for Regular Timed Processes(Concurrency Theory and Applications '96)
- 実時間通信プロセスの述語的仕様記述に対する検証法(並列・分散)
- 実時間通信プロセスの述語的仕様記述に対する検証法(並列・分散)
- An Extention of DynAlloy with Concurrency
- 分離論理を用いたTOPPERS/ASPの割込み動作に対する検証
- テスト等価性に基づいた視覚的LTSモデル操作によるプロセス代数デバッガ
- 通信プロセスモデルと形式意味論に基づくソフトウェアのモデル化(ディペンダブルソフトウェア)
- FOREWORD
- Alloyを用いたRuby on Railsアプリケーションの開発支援
- 「情報処理学会論文誌 : プログラミング」の編集について
- Nested timed automata
- 時間付きπ計算によるリアルタイムオブジェクト指向言語の形式的記述
- Generating Diagnostic Information for Probabilistic Processes
- A Session Type System with Subject Reduction
- 無限小定数と限量子除去法によるハイブリッドシステムの検証に向けて
- タスクマイグレーション機能を持つマルチコアスケジューリング解析
- タスクマイグレーション機能を持つマルチコアスケジューリング解析
- FOREWORD
- 値付きタスクオートマトンに基づくコストを意識した実時間タスクスケジューリング
- 形式仕様に基づく通信プログラム開発システムONL
- CCSによるモニタの動作の形式的記述