π計算に基づくプログラミング言語NepiのためのGUI機能
スポンサーリンク
概要
- 論文の詳細を見る
本論文では,π計算に基づくプログラミング言語NepiへのGUI機能を設計し,その実装手法を示す.Nepiは,プロセス代数π計算に基づくプログラミング言語で,名前を介したランデブー型通信を実現している.NepiにおけるGUIプログラミングによって,イベントハンドリングをπ計算に基づいて形式的に解析することが可能になり,GUIプログラムの信頼性を向上させることが可能となる.GUIはボタンやフレームなどのグラフィックコンポーネントを単位として構成し,各コンポーネントに1つの名前を割り当て,コンポーネントから生成されるイベントに対する動作を定義することでGUIプログラムの動作をπ計算の動作意昧に基づいて実現する.Nepiにおいて,グラフィックコンポーネントの生成に,?gという新たな構文を定義し,ユニークな名前を割り当てる.この拡張によって各グラフィックコンポーネントに割り当てた名前を介して,コンポーネントが持つ属性値の参照や更新を,名前通信として動作記述する.グラフィックコンポーネントは,イベントの種類ごとに生成されるイベントハンドリングプロセスを生成する.イベントハンドリングプロセスはイベントの発生を指定された名前による通信に変換する.GUIプログラムはグラフィックコンポーネント,イベントハンドリングプロセスおよびそのイベントを受け取って全体の機能を実現するプロセスの並行合成として記述される.以上のようなモデル化に基づいて,GUI機能をAllegro Common Lisp上に実装し,実際のNepiプログラムを用いて,名前通信に基づくGUIプログラムの記述例とその特徴を示す.
- 2004-11-15
著者
-
桑原 寛明
立命館大学情報理工学部
-
結縁 祥治
名古屋大学大学院情報科学研究科
-
真野 健
NTTコミュニケーション科学基礎研究所
-
河辺 義信
日本電信電話株式会社nttコミュニケーション科学基礎研究所
-
阿草 清滋
名古屋大学大学院情報科学研究科
-
阿草 清滋
名古屋大学
-
結縁 祥治
名古屋大 大学院情報科学研究科
-
水野 敦
名古屋大学大学院情報科学研究科
-
河辺 義信
NTTコミュニケーション科学基礎研究所
-
桑原 寛明
名古屋大学大学院情報科学研究科
-
Yuen Shoji
Center For Information Media Studies Nagoya University
-
結縁 祥治
名古屋大学 情報科学研究科
-
河辺 義信
愛知工業大学情報科学部情報科学科
関連論文
- Maudeによる否定を含んだ構造操作意味定義インタプリタと等価性検証器の構築
- Maudeによる否定を含んだ構造操作意味定義インタプリタと等価性検証器の構築
- 3K-5 タスク分割によるCell用の自動並列化コンパイラの開発(チップマルチプロセッサと並列化技術,学生セッション,アーキテクチャ)
- 通信プロセスモデルによるAIBO OPEN-Rプログラムのデッドロックフリー解析手法(検証/テストとデバッグ,組込みシステム工学)
- 確率様相論理による秘匿性の証明 (代数と言語のアルゴリズムと計算理論)
- 4K-2 条件分岐のSIMD化手法のCellへの適用(HPCと高速化,学生セッション,アーキテクチャ)
- 4. ソフトウェアエンジニアリング領域(J07-SE)(情報専門学科カリキュラム標準J07)
- 例外処理付きオブジェクト指向プログラムにおける情報流の安全性解析のための型システム(ディペンダブルコンピューティング)
- Apache Cocoon Flowscriptのモデル検査によるWeb応用プログラムの動作検証
- Haskellのための非同期局所化π計算に基づくネットワークプログラミングフレームワーク
- 5K-8 消費電力の実行時予測を用いた電力最適化(マルチスレッドと省電力,学生セッション,アーキテクチャ)
- 細粒度リポジトリに基づくVHDLツールプラットフォーム(ツール,開発環境)
- 通信プロセスに対する文脈変換手法を用いたモデル検査
- テスト等価性に基づいた視覚的LTSモデル操作によるプロセス代数デバッガ
- プログラムの正規化に基づいた差分抽出法の提案
- 意味を考慮した差分抽出ツール
- On the Job Learning : 産学連携による新しいソフトウェア工学教育手法
- 高精度なデータ依存解析に基づくシーケンス図スライシング手法(モデリング(学生セッション))
- ソフトウェア理解支援のための多粒度ソフトウェアマップ(インタフェース・ナビゲーション(学生セッション))
- ソフトウェアの大局的可視化のための組織化メトリクス
- 確率様相論理による秘匿性の証明
- 動的電圧制御システムにおける評価戦略選択に基づく高効率消費エネルギー関数型プログラミング
- 知識基盤社会を支える情報技術論文特集の発行にあたって
- StrutsLint : Web アプリケーションコーディングチェッカ
- 7.高信頼WebWare生成技術 : WebWareのテスト・解析・作成支援(第1部:高い生産性を持つ高信頼ソフトウェア作成技術の開発,学と産の連携による基盤ソフトウェアの先進的開発)
- 要求定義支援のための要求適合度を用いた事例検索(要求工学(学生セッション))
- 設計工程に合わせたビュー生成を可能にするソフトウェア文書管理手法の提案
- 歴代理事長座談会「日本ソフトウェア科学会の20年とこれから」(20周年記念特集)
- 要求フレームに基づいたソフトウェア要求仕様化技法
- 計算資源へのアクセス能力に基づく競合検査とデッドロック検査のための型解析
- 制御ソフトウェアの固定小数点演算化ツールの設計と実装
- 4M-4 細粒度マークアップに基づくカスタマイズ可能なコーディング規約検査器(リーディングプロジェクト e-society:高信頼ソフトウェア・WebWare開発支援システム,一般セッション,リーディングプロジェクト e-society)
- アマゾンバグ防止フレームワークのためのWebアプリケーション双実行モデル
- NEXCESS : 社会人組込みソフトウェア技術者教育におけるスキル育成
- 社会人に対する組込みソフトウェア技術の再教育の取り組み
- GUI抽象化規則を用いたモデル生成手法(開発支援(2)(学生セッション))
- コンピュータサイエンスシリーズ 15 離散数学, 牛島和夫(編著), 相利民, 朝廣雄一(著), コロナ社(2006-09), A5判, 定価(本体3,000円+税)
- 時間付きデザインパターンに基づく実時間並行ソフトウェアの開発手法
- 5L-8 コード視覚化手法を用いたMPIプログラム開発環境のユーザインタフェース(プログラミング支援環境,学生セッション,ソフトウェア科学・工学)
- 1K-6 静的解析情報を利用したセキュアシステムの侵入検知精度向上(仮想化と言語処理系,学生セッション,アーキテクチャ)
- 1X-2 冗長な検査の削除を行う整数オーバーフロー対策ツールの実装(セキュア設計・実装・フォレンジクス,学生セッション,セキュリティ)
- 時間付き$\pi$計算における有限プロセスの時間動作抽象化(計算機科学の理論とその応用)
- 例外処理付きオブジェクト指向言語における情報流の安全性解析
- 例外処理付きオブジェクト指向言語における情報流の安全性解析
- Javaプログラム理解支援のための不変性解析
- Java プログラム理解支援のための不変性解析
- π計算に対する時間拡張と合同的性質(計算モデル,フォーマルアプローチ論文)
- π計算に基づくプログラミング言語NepiのためのGUI機能
- 時間付きπ計算によるリアルタイムオブジェクト指向言語の形式的記述(オブジェクト指向とWeb技術)
- π計算による優先度継承プロトコルの形式的記述
- 名古屋大学情報メディア教育システムの現状と課題
- 高階書換え系の単一正規形性
- 高階書き換え系の単一正規形性
- Nepi : π計算に基づくネットワーク・プログラミング言語
- 実行履歴にもとづくマルチコア実時間応用プログラムのデバッグモデル
- ゲーム列による安全性証明の形式化と自動化(数理的技法による情報セキュリティ)
- 匿名性とプライバシ保護の数理的技法 (特集 コミュニケーション環境の未来に向けた研究最前線)
- ETAPS 2006参加報告(会議レポート)
- Nepiネットワークプログラミングシステムの形式的検証(ソフトウェア工学の基礎)
- π-計算の名前制限の名前生成による実装の正しさ
- プロセス代数に基づくネットワークプログラム言語 (特集論文1 情報科学研究の最前線--より安全で快適な情報処理技術を目指して) -- (快適にコンピュータを使えるために)
- π-計算に基づくモバイルエージェントの形式化
- アクタモデルのπ計算に基づく意味づけ : エージェントの形式化に向けて
- Webオートマトン : MVCモデルに基づくWebアプリケーションの動作モデル(ディペンダブルソフトウェア)
- FCDGに基づいたコーディングパターン
- 関数部分知識と匿名性検証(理論,数理的技法による情報セキュリティ,平成19年研究部会連合発表会)
- 攻撃者を考慮した匿名性検証法 (第20回 回路とシステム軽井沢ワークショップ論文集) -- (形式的手法)
- セッション型に基づく高信頼ネットワークプログラムの関数型言語による実装手法
- 時間オートマトンによる振舞いモデルに基づく高信頼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によるコンパイラの仕様記述
- ウィンターワークショップ2011・イン・修善寺開催報告
- チャネルに基づく選択付き通信のための分散プロトコル
- Nepi^2: π計算に基づくネットワーク・プログラミングのための2レベル計算体系
- 電子投票プロトコルに対する無証拠性の定理証明
- 計算資源へのアクセス能力に基づく競合検査とデッドロック検査のための型解析
- フォーマルメソッドによるセキュリティ&プライバシ (特集 20周年を迎えたコミュニケーション科学)
- 「情報処理学会論文誌 : プログラミング」の編集について
- 否定前件を含む構造操作意味定義に対するプロセス計算コンパイラ
- 匿名性・プライバシーの工学的定式化とその学際的応用
- CoSyProofs 2009参加報告(会議レポート)
- 認知変数連結論 : 認知心理学を見つめ直す, 中島義明(著), コロナ社(2007-11), B6判, 定価(本体2,600円+税)
- 6. 匿名性とプライバシのためのフォーマルメソッド(Part III:新領域の開拓,フォーマルメソッドの新潮流)
- 分離論理を用いたTOPPERS/ASPの割込み動作に対する検証
- 順序ソート項書換え系における合流性のモジュラ性
- 確率様相論理による秘匿性の証明
- コールスタックの制御データ検査によるスタック偽装攻撃検知
- 電子投票プロトコルに対する無証拠性の定理証明 (特集 人と共存するコンピュータセキュリティ技術)
- コンシェルジュサーバを持つ電話システムの形式的検証
- A-011 既存のプログラミング言語のための量子探索機構(アルゴリズム・コンピュテーション(1),A分野:モデル・アルゴリズム・プログラミング)