拡張時間オートマトン群による実時間システムの記述および検証
スポンサーリンク
概要
- 論文の詳細を見る
この論文では, QoS制御機能をもった動画像再生システムを例に,拡張時問オートマトン群による実時間システムの記述及び検証について述べる.動画像再生システムの記述に検証のための追加や変更を行い,ジッターやフレーム再生間隔といったいくつかの性質をCTLで記述した.そして,チェッカーUppaalを用いて,記述した動画像再生システムが安全性と上記の性質を満たすかの検証を行った.また, QoS制御機能のUppaalによる検証についても触れる.
- 2003-01-23
著者
-
岡野 浩三
岡山大学大学院自然科学研究科
-
山口 弘純
大阪大学大学院情報科学研究科
-
岡野 浩三
大阪大学大学院情報科学研究科
-
谷口 健一
大阪大学大学院情報科学研究科
-
加藤 雄一郎
大阪大学大学院基礎工学研究科情報数理系専攻
関連論文
- 災害現場でセンシングされた生体情報を集約する無線センサーネットワークの構成法(モバイルコンピューティング、モバイルアプリケーション、ユビキタス通信、モバイルマルチメディア通信)
- 詳細度の異なるモデルを用いた無線シミュレーションの高速化手法の提案(Work in Progress,ワイヤレス環境でのアプリケーション品質,P2P/アドホックネットワーク,画像符号化,ストリーム技術,信頼性,一般)
- 車車間通信を利用した信号機制御手法の提案
- 1J-4 センサーネットワークの設計開発を支援するシミュレーション融合型テストベットの検討(情報爆発時代における情報提示・センサネット・P2P,一般セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- 目的地選択の公平性と指定されたノード密度分布を実現する移動モデルの提案(学生特別セッション,移動通信ワークショップ)
- 確率的モデル検査ツールを用いた実時間ネットワークシステムの検証手法の提案およびネットワークシミュレータNS-2との比較
- 外部入力値のみを保持できる整数変数をもつFSMに対する記号モデル検査法(ソフトウェア工学)
- 無線センサーネットワークを利用した電子トリアージシステムの実現(モバイル/放送融合アプリケーション,モバイルコンテンツ,モバイル映像配信,一般)
- 無線センサーネットワークを利用した電子トリアージシステムの実現(学生特別セッション,モバイル/放送融合アプリケーション,モバイルコンテンツ,モバイル映像配信,一般)
- 傷病者の自動監視を実現する電子トリアージシステム(モバイル P2P,ユビキタスネットワーク,アドホックネットワーク,センサネットワーク,一般)
- 在庫管理プログラムの設計に対するJML記述とESC/Java2を用いた検証の事例報告(研究速報)
- ノード群の相対位置関係に基づく位置推定アルゴリズムの評価手法
- 移動無線端末の位置情報と通信情報を用いた災害現場地図の自動生成
- 断続的に移動する無線端末群の位置推定
- 災害時救急救命支援に向けた電子トリアージシステムの設計開発
- 遭遇端末の位置情報と地理情報を併用した高精度な位置推定手法の提案と評価(ユビキタスネットワーク,ITS,センサーネットワーク,アドホックネットワーク)
- 拡張時間オートマトン群による実時間システムの記述および検証
- 計算負荷分散を考慮した近隣端末の分散型移動予測手法の提案
- センサネットワークアプリケーションの実装支援APIの実装と評価
- 確率事象駆動型モデルを利用した無線ネットワークシミュレーション高速化手法の提案
- 確率事象駆動型モデルを利用した無線ネットワークシミュレーション高速化手法の提案
- 確率事象駆動型モデルを利用した無線ネットワークシミュレーション高速化手法の提案
- 確率事象駆動型モデルを利用した無線ネットワークシミュレーション高速化手法の提案
- 時間システムを対象とした到達可能性解析の高速化手法の提案
- 時間抽象を行う洗練手法を用いた確率時間システムの到達可能性解析
- OCLのJMLへの変換ツールの実装と評価
- 傷病者の自動監視を実現する電子トリアージシステム(モバイル P2P,ユビキタスネットワーク,アドホックネットワーク,センサネットワーク,一般)
- OCLのJMLへの変換ツールの実装について
- 実時間システムを対象としたCEGARによる抽象洗練の並列化手法
- 災害現場の被災者や救援者の行動記述とそれを用いたネットワークシミュレーション環境の提案
- Javaに対するループインバリアントを含むDaikon生成アサーションの妥当性評価(研究速報)
- 上位設計におけるシステムの振る舞い検証技術(システム設計のための形式手法の基礎と応用)
- B-001 Javaに対するDaikonを用いたインバリアント自動生成のための汎用基盤ツール(ソフトウェア,一般論文)
- 時間制約を保証するUML/OCLを用いた分散実時間アプリケーション開発手法(ソフトウェア,フォーマルアプローチ論文)
- UML/OCLを用いた分散実時間アプリケーション開発手法の提案
- UML/OCLを用いた分散実時間アプリケーション開発手法の提案
- D-3-6 分散実時間アプリケーションのUML/OCL記述から時間オートマトンネットワークを用いた動作仕様記述への変換手法の提案(D-3. ソフトウェアサイエンス, 情報・システム1)
- 分散環境実時間アプリケーション開発支援のためのTimeliness QoS一貫性検証系および時間制御コード生成系の実装
- 関数型言語ML向け形式的検証支援システムの試作
- 線形制約式を用いた時間QoS一貫性の検証法 (計算機科学基礎理論の新展開)
- 関数型言語MLによるプレスブルガー文真偽判定ルーチンの開発と検証支援システムへの応用
- D-3-8 分散環境における実時間アプリケーション動作仕様記述からのJavaコード自動導出手法の提案(D-3. ソフトウェアサイエンス)
- マルチメディアシステムにおけるTimeliness QoS一貫性検証と時間制御コード導出
- ペトリネットで記述された簡易ブラウザ型の組込みJavaプログラム動作仕様に対する実行方式の提案
- ワークフロー記述向きの時間付きカラーペトリネット
- 時間ペトリネットの拡張モデルを用いたプロトコル合成
- 耐故障性のための多重化リソースを持つ分散システムの導出法
- PeerCastにおける経路の動的変更機能の実装(次世代ネットワーク,SIP・プレゼンス,一般)
- API Hookを用いたWindowsプログラムのモビリティ向上ソフトウェアの作成
- API Hookを用いたWindowsプログラムのモビリティ向上ソフトウェアの作成
- 電子的なホワイトボードのセキュア化に関する研究(信号処理,符号化,知的マルチメディアシステム,一般)
- 電子的なホワイトボードのセキュア化に関する研究(信号処理,符号化,知的マルチメディアシステム,一般)
- 電子的なホワイトボードのセキュア化に関する研究(信号処理,符号化,知的マルチメディアシステム,一般)
- 動画像圧縮技術を応用した透視変換の高効率化に関する研究(信号処理, 符号化とそれらを用いた知的マルチメディアシステム, 一般)
- 動画像圧縮技術を応用した透視変換の高効率化に関する研究(信号処理, 符号化とそれらを用いた知的マルチメディアシステム, 一般)
- 動画像圧縮技術を応用した透視変換の高効率化に関する研究(信号処理, 符号化とそれらを用いた知的マルチメディアシステム, 一般)
- 最適化手法によるパノラマ画像合成法の提案(画像システム,知的マルチメディア処理システム及び一般)
- MANETにおける位置情報マルチキャストルーティングMgCastの提案と性能評価(無線・モバイルネットワーク)
- 無線端末の遭遇履歴情報を用いた移動軌跡推定手法の提案
- 多人数参加型アプリケーションにおける品質要求を考慮した帯域制御の一方式(マルチメディア通信と分散処理)
- 動画の品質劣化の許容度を考慮した帯域制御の一方式
- 帯域割譲交渉による動的帯域制御方式
- 品質要求を考慮した動的な帯域制御を行うプロトコルの提案とその性能評価
- 非同期式パイプライン制御回路の論理合成法(論理合成+高位合成)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会)
- 非同期式パイプライン制御回路の論理合成法(論理合成+高位合成)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会-)
- 非同期式パイプライン制御回路の論理合成法(論理合成+高位合成)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会-)
- 非同期式パイプライン制御回路の論理合成法(論理合成+高位合成)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会-)
- コンポーネント連携によるサービスをオーバレイネットワーク上で実現するためのサービス設計技法の提案(セッション8-B : ミドルウェア)
- コンポーネント連携によるサービスをオーバレイネットワーク上で実現するためのサービス設計技法の提案(セッション8-B : ミドルウェア)
- ノード間の位置関係に基づく推定位置精度の評価手法
- ノード障害に対する自律分散的回復を可能とするオーバレイ遅延最小木の構築アルゴリズム(セッション4:ミドルウェア)
- センサネットワークアプリケーションの実装支援APIの実装と評価
- 並列データパス付き小型DSPを利用したVGA動画像の射影変換 : 高速化のための二つの提案(コンピュータグラフィックス)
- 並列データパス付き小型DSPを利用したVGA動画像の射影変換 : 高速化のための2つの提案(システムLSIの応用と要素技術,専用プロセッサ,プロセッサ,DSP,画像処理技術及び一般)
- 並列データパス付き小型DSPを利用したVGA動画像の射影変換 : 高速化のための2つの提案(システムLSIの応用と要素技術,専用プロセッサ,プロセッサ,DSP,画像処理技術及び一般)
- 並列データパス付き小型DSPを利用したVGA動画像の射影変換 : 高速化のための2つの提案(システムLSIの応用と要素技術,専用プロセッサ,プロセッサ,DSP,画像処理技術及び一般)
- 安定したストリーム配信を実現するオーバレイマルチキャストプロトコルの設計とPlanetLab上での実証実験
- 射影変換における座標計算の高速化手法(画像・映像処理)
- D-11-139 射影変換における座標計算の高速化手法 : 誤差の評価(D-11.画像工学D)
- ワイヤレスデバイスとレーザレンジスキャナを併用した移動体トラッキング(ホームネットワーク,ユビキタスネットワーク,クラウドコンピューティング,コンテキストアウェア,位置情報サービス,eコマース及び一般)
- センサネットワークアプリケーションの実装支援APIの実装と評価
- センサネットワークアプリケーションの実装支援APIの実装と評価
- B-15-20 アドホック通信を用いた歩行者密度の推定法(B-15.モバイルマルチメディア通信,一般セッション)
- 安全な多重帰属制御を実現するVPN分散管理プロトコルの提案(ネットワークプロトコル,シームレスコンピューティングとその応用技術)
- 通信履歴と地理情報を併用した無線端末の移動軌跡推定(モバイルP2P,ユビキタスネットワーク,アドホックネットワーク,センサネットワーク,一般)
- 依存性グラフを利用した非同期式パイプライン合成のための制御回路の構成法(コンピュータ構成要素)
- 制御フローグラフを用いた非同期式パイプライン合成(コンピュータ構成要素)
- 制御フローグラフを用いた非同期式パイプライン合成(プロセッサアーキテクチャ,SWoPP2006)
- 非同期式プロセッサのパイプライン化アルゴリズム : 条件分岐のない場合(プロセス・デバイス・回路シミュレーション及び一般)
- 非同期式プロセッサのパイプライン化アルゴリズム : 条件分岐のない場合(プロセス・デバイス・回路シミュレーション及び一般)
- 複数反例抽出を用いたCEGARによる時間オートマトンの抽象洗練手法
- 集計時の負荷を軽減した重み付き電子投票プロトコル
- OCLからJMLへの変換ツールにおける対応クラスの拡張と教務システムに対する適用実験
- モデル検査器とDaikonを用いた表明動的生成改善手法のシステム開発実プロジェクト教材への適用と評価
- モデル検査器とDaikonを用いた表明動的生成改善手法のシステム開発実プロジェクト教材への適用と評価
- 制約記述言語OCLとJMLのモデル駆動開発技法に基づいた双方向の変換手法の提案
- SMTソルバーとPDG作成ツールを用いたJavaのテストケース自動導出手法の提案
- PDGとSMTソルバを利用した表明自動導出手法の提案と評価(ソフトウェア工学,ソフトウェア基礎・応用論文)
- 契約記述の変更傾向の開発履歴情報を用いた調査
- 契約記述の変更傾向の開発履歴情報を用いた調査