VDM記述からのPromela記述生成における変換手法の提案
スポンサーリンク
概要
- 論文の詳細を見る
開発早期での検証の手段として形式手法が注目されている.形式仕様記述は開発対象の機能側面に対して厳密な仕様記述を行うことを可能とする.しかし,開発対象の振る舞いの検証において完全性を欠く.一方,形式検証に含まれるモデル検査は開発対象の状態を網羅的に探索することによって振る舞いを検証する.そこで,本論文では形式仕様記述によって得られた厳密な仕様記述をモデル検査が可能な記述へと変換する手法を提案する.
- 2011-03-07
著者
-
大森 洋一
九州大学大学院システム情報科学研究院
-
日下部 茂
九州大学大学院システム情報科学研究院
-
荒木 啓二郎
九州大学大学院システム情報科学研究院
-
日下 部茂
九州大学大学院総合理工学研究科
-
宮下 怜
九州大学大学院システム情報科学府
-
日下部 茂
九州大学大学院システム情報科学府・研究院
-
大森 洋一
九州大学システム情報科学研究院
-
荒木 啓二郎
九州大学システム情報科学研究院
関連論文
- エンタープライズ型プライベートクラウドによる教育環境の性能評価
- 周期性を持つ非同期通信システムのモデリングに関する研究(モデリング(学生セッション))
- 自己タイミング型パイプラインシステムの性能見積りモデル(VLSI設計技術とCAD)
- ATM over IPの実現と性能評価
- ATM over IP の実現と性能評価
- 並列分散オペレーティングシステムCEFOSにおける一括システムコール機構の実装と評価
- 緊密な産学連携に基づく自律的なICT人材育成の実践(情報システム教育コンテスト(3))
- 継続概念による割り込みなし並列I/O処理モデル(継続点)
- スレッドの実動作情報に基づく細粒度マルチスレッド制御法(並行処理(2))
- Zero-Wait方式による多数のI/O要求に対する処理のFuce上での実現と評価(OS-2 : 資源管理,2006年並列/分散/協調処理に関する『高知』サマー・ワークショップ(SWoPP高知2006)-研究会・連続同時開催-)
- 細粒度マルチスレッド環境でのスケジューリングオーバヘッド低減機構の評価(リソース制御)
- Fuceプロセッサ上での継続モデルによる並列I/O処理
- 測定可能な個人プロセスを対象とした形式手法導入に関する提案(形式手法(学生セッション))
- 大規模な産学連携による高度ICT人材育成に向けての取り組み
- アドレス空間を共有するスレッドの空間的な集約を行うスケジューラの評価(カーネル)
- アドレス空間を共有するスレッドの空間的な集約を行うスケジューラの評価
- 継続概念を用いたZero-Wait方式によるOS構成法の提案(OS (1))
- 性能モニタリングカウンタによる一括システムコール機構の評価(OS-2:モニタリング)(2004年並列/分散/協調処理に関する『青森』サマー・ワークショップ(SWoPP青森2004) : 研究会・連続同時開催)
- マルチスレッド実行機構を考慮したプログラム実行制御法(スレッド・プロセス)
- 細粒度マルチスレッド環境でのスケジューリングオーバヘッド低減機構(スレッド・プロセス)
- OSの処理を多く含む並列処理の効率化を指向した一括システムコール機能(システムソフトウェア)
- B-41 並列分散オペレーティングシステムCEFOSにおけるジョブ実行方式と分散共有メモリ機構(リアルタイムと分散共有メモリ,B.ソフトウェア)
- プロトコルスタックをバイパスするMyrinet用ソケット通信機構
- 共有メモリシステム上での細粒度 non-strict データフロー構造データの生産者・消費者間パイプライン実行
- 自然言語による仕様記述の形式モデルへの変換を利用した品質向上に向けて
- コア間時間集約スケジューラ活用のためのAPIの実装と評価
- オブジェクト指向形式仕様記述言語VDM++支援ツールVDMTools(ソフトウェア紹介,先端ソフトウェアツール)
- JUnit向け単体テストを対象としたMapReduce型並列分散実行フレームワークの提案
- 集約制御機構を持つコア間時間集約スケジューラの実装と評価
- Hadoopのマルチコア実行におけるスレッド集約スケジューリングの効果
- ドメイン知識を用いた検証に向けた状態遷移図の抽象化方法に関する考察
- JUnit向け単体テストを対象としたMapReduce型並列分散実行フレームワークの提案
- 状態遷移図の同期モデルへの詳細化および検証手法
- プロジェクトマネジメント学会九州支部活動報告
- プロジェクトマネジメント学会九州支部活動報告(Mail to PM)
- プロジェクトマネジメント学会九州支部活動報告
- Hadoop のマルチコア実行におけるスレッド集約スケジューリングの効果
- データフローモデルに基づく超並列V言語とその商用並列計算機上の実装について
- 超並列V言語とそのマルチスレッド実行方式の概要
- 多重同時最適制御に解放する方式の実装(コンカレント工学一般、及び、CSTソリューションコンペティション2007発表会)
- 変数オリエンティッドなデータ依存関係モデルの提案
- 変数オリエンティッドなデータ依存関係モデルの提案
- 並列化支援視覚化システム NaraViewにおけるビュー間の連携方式について
- 並列化支援のためのデータ依存の3次元視覚化
- Datarolマシンの資源管理方式に関する考察
- 連想記憶と進化過程
- 機能分散・協調によるロボットシステムの構成
- 大規模な産学連携による高度ICT人材育成に向けての取り組み
- モデル規範型形式手法VDMと仕様記述言語VDM++ : 高信頼性システムの開発に向けて(情報システムの信頼性・安全性)
- 大規模な産学連携による高度ICT人材教育におけるインターンシップの役割とその効果
- 1. フォーマルメソッドの過去・現在・未来 : 適用の実践に向けて(Part I:歴史と概要,フォーマルメソッドの新潮流)
- ロボット制御ソフトウェアの形式的モデル検証
- 背表紙画像を用いたネットワーク透過な仮想書架
- エニキャストを用いた自動車のための地域別緊急通報システムの実現(アドホックネットワーク, ユビキタスITSとモバイルアプリケーション)
- 形式仕様記述における階層アーキテクチャ
- エニキャストを用いた位置依存グループウェアの設計と実装
- ユビキタス環境を活用した位置に基づくグループウェア
- ユビキタス環境を活用した位置に基づくグループウェア
- 細粒度マルチスレッド処理向けプロセッサDatarol-IIの構成とその評価
- 並列計算機Datarol-IIのプロセッサエレメントの構成
- スレッド実行機構を導入したDatarolアーキテクチャについて
- Ada並列プログラムのためのグラフィック表示を用いた実行再演ツール
- 並列分散オペレーティングシステムCEFOSにおける準プリエンプション機能
- 並列分散オペレーティングシステムCEFOSにおける準プリエンプション機能
- 並列分散オペレーティングシステムCEFOSにおける一括システムコール機構の実装と評価
- CPSY2000-57 並列分散オペレーティングシステムCEFOSにおける一括システムコールの機構
- CEFOSオペレーティングシステムのスレッド管理機構
- Ｗｅｂサービスを用いた読書録サービスの設計と実装
- 仮想書架における背表紙画像生成の自動化
- 自己タイミング型パイプラインシステムのオンチップ・マクロシミュレーション手法(ARC-8:シミュレーション技法,2006年並列/分散/強調処理に関する『高知』サマー・ワークショップ(SWoPP 高知2006))
- 自己タイミング型パイプラインシステムのマクロシミュレーションモデル
- 自己同期型パイプラインシステムのマクロフローモデル(ARC-3:専用プロセッサと時刻管理)(2003年並列/分散/協調処理に関する『松江』サマー・ワークショップ(SWoPP松江2003))
- 並列分散オペレーティングシステム : CEFOS (Communication-Execution Fusion OS)
- PI-46 行動特性に着目した情報通信分野教育でのProject-Based-Learningの実施(ポスター発表I)
- Web 上における仮想書架の試作と評価 （「ディジタル図書館」ワークショップ 第28回）
- 分散ストレージの安全性検証
- VDM記述からのPromela記述生成における変換手法の提案
- データ型に着目した形式仕様記述からの状態遷移系の抽出(サイバー増大ページ論文概要,新しいソフトウェアの実現,サイバー増大号)
- 非ストリクトデータフロープログラム実行におけるスタックフレームの利用
- 細粒度データフロー言語のWS実装時におけるスレッド結合法の評価
- オブジェクト指向に基づくスカラ拡張の適用条件のクラス化
- オブジェクト指向の枠組によるループ並列化記述
- OMT法による並列化コンパイラ中間言語フレームワークの構築
- データフローに基づくマルチエージェントによる並行プログラミング
- Hadoopを用いた大容量バケット解析システムの設計と実装(トラヒック,NW評価,性能,リソース管理・制御,トラヒックエンジニアリング,NW信頼性・レジリエンシ,一般)
- 分散メモリシステム上での細粒度non-strictデータフロー構造データの生産者・消費者間パイプライン実行
- EARTHアーキテクチャ上でのデータフロー仮想マシンコードDVMCの実行
- 再帰的非ストリクト構造データ生成の効率化
- 分散メモリ実装におけるデータフロー言語の構造データ管理方式
- 分散メモリ実装におけるデータフロー言語の構造データ管理方式
- 分散メモリ型商用並列計算機上でのデータフロー言語の配列参照の効率化
- Dataolマシンの資源管理方式に関する検討 : プロセス状態検出方法と状態変化制御機構
- マルチメディア情報環境を想定したエージェント指向交換システム
- データフロー概念に基づくマルチエージェント指向交換プログラム構成法
- Hadoopを利用したパケット解析システムにおけるパケット入力方法の改善(一般,モバイル,アドホック,ユビキタス,無線,セキュリティ,マルチアクセス,アクセスネットワーク・UserNetworkInterface,Homeネットワーク,一般)
- 規範的チーム開発プロセスTSPiに基づく産学連携PBLの事例報告-OpenFlowコントローラ開発への形式手法導入-
- 関数型言語Validへのオブジェクト指向的記述形式の導入とその実現方式
- 設計時の決定における依存関係の表記法
- 超並列処理記述言語Vによる画像処理アルゴリズムの記述
- 超並列処理記述言語Vによる画像処理アルゴリズムの記述