UMLアクティビティ図からSPINモデル検査用コードの自動生成とWebアプリケーション設計への適用(次世代経営情報技術,一般)
スポンサーリンク
概要
- 論文の詳細を見る
UMLアクティビティ図は、ワークフローの表現に適しており、分析・設計から実装に至るまでの開発の各段階において振る舞いを表現できる.ソフトウェアの上流設計仕様を形式言語でモデル化し、検査ツールを用いて動作検証あるいは反例を検出するというアプローチが注目を集めている.本報告では、UMLアクティビティ図を、モデル検査ツールSPINが用いるPROMELA言語コードに自動変換する手法を提案する.提案手法の評価のため、筆者の一人が顧客向けに開発しているWebアプリケーションの画面遷移設計に試行適用したところ、モデル検査ツールにより反例の検知とトレースが得られ、一定の条件下での潜在バグが明らかとなった.
- 2011-02-18
著者
-
和崎 克己
信州大学大学院工学系研究科
-
和崎 克己
信州大学工学部
-
和崎 克己
信州大学大学院・情報工学
-
和? 克己
信州大学大学院工学系研究科情報工学専攻
-
山田 豊
信州大学大学院工学系研究科
-
和崎 克己
信州大 工
関連論文
- コンカレントエンジニアリングを目指したロボット設計製作教育
- 工学教育としてのロボットコンテストの意義
- 2V-8 P2Pオーバーレイネットワークにおける仮想接続の永続化プロトコルとその検証(ネットワーク理論・プロトコル,学生セッション,ネットワーク)
- 拡張ペトリネットを用いた情報収集の為の分散アルゴリズムの設計
- IP アドレスを持たない認証ゲートウェイについて
- IPアドレスを持たない認証ゲートウェイについて
- 2L-2 モデル検査に対応する上位ハードウェア記述言語MelasyのVHDLコード生成(上流設計技術,学生セッション,アーキテクチャ)
- 2L-1 モデル検査に対応する上位ハードウェア記述言語MelasyとXML中間表現(上流設計技術,学生セッション,アーキテクチャ)
- A-031 モデル検査系に対応する上位ハードウェア設計言語Melasy(A分野:モデル・アルゴリズム・プログラミング)
- (202)OTC医薬品販売教育における学習者問題作成型e-learning教材の開発(セッション58 コンピュータ援用教育I)
- (22)学社融合によるロボット教室の試み : 親子のロボット工作教室(第6セッション 個性化・活性化(I))
- 広選択度広帯域マイクロストリップラインフィルタによるCATV上り拡張アンプに関する研究(ネットワークプロセッサ,通信のための信号処理,及び一般)
- 広選択度広帯域マイクロストリップラインフィルタによるCATV上り拡張アンプに関する研究(ネットワークプロセッサ,通信のための信号処理,及び一般)
- 広選択度広帯域マイクロストリップラインフィルタによるCATV上り拡張アンプに関する研究(ネットワークプロセッサ,通信のための信号処理,及び一般)
- N-5 プログラミングレポート自動評価における事前処理(教育支援システム(1),N.教育・人文科学)
- 中心多様体と弱非線形系H^∞制御
- 拡張ペトリネットを用いた情報収集の為の分散アルゴリズムの設計
- Moodle用数理演習モジュールを用いたWeb上での数理教育手法(ユビキタス・モバイル学習環境/一般)
- 形式化数学言語システムMizarを用いたCMS/Moodleの数理演習モジュール開発(e-learning/一般)
- GHz帯長距離漏洩同軸ケーブルを用いた高速防災無線情報システムの研究開発
- B-7-80 高速防災無線情報システム向け2.4GHz帯長距離漏洩同軸ケーブル(B-7.情報ネットワーク,一般講演)
- 拡張ペトリネットとJava/PNMLによる並列システムの構成手法(コンカレントシステム,離散事象システム,ハイブリッドシステム,及び一般)
- 7-213 信州大学インターネット大学院・大学の現状(オーガナイズドセッション「バーチャルユニバーシティ」)
- IEEE802.11g 無線 LAN を用いた山間地拠点間接続の長距離化(ネットワークプロセッサ, 通信のための信号処理, 符号理論, 一般)
- IEEE802.11g 無線 LAN を用いた山間地拠点間接続の長距離化(ネットワークプロセッサ, 通信のための信号処理, 符号理論, 一般)
- IEEE802.11g無線LANを用いた山間地拠点間接続の長距離化(ネットワークプロセッサ, 通信のための信号処理, 符号理論, 一般)
- IEEE802.11g無線LANを用いた山間地拠点間接続の長距離化
- IEEE802.11g無線LANを用いた山間地拠点間接続の長距離化
- IEEE802.11g無線LANを用いた山間地拠点間接続の長距離化
- IP アドレスを持たない認証ゲートウェイについて
- IPアドレスを持たない認証ゲートウェイについて
- 信州大学インターネット大学院における学習進捗状況管理システム (eラーニングの実践報告とシステム公開デモセッション)
- 自己組織化マップを用いたニューラルネットワークによる高分子物性予測(OS4b 逆問題解析手法の開発と最新応用)
- 2L-6 時間制約ガード付LOTOS仕様(E-LOTOS)による論理回路ライブラリDILLの拡張(上流設計技術,学生セッション,アーキテクチャ)
- コンピュータウイルスのコード静的解析による特徴抽出と分類について
- (204)情報セキュリティマネジメント向けe-learning教育用コンテンツの作成 : 高校生に対する情報社会に参画する態度の育成(セッション58 コンピュータ援用教育I)
- (73)信州大学インターネット大学院におけるCAIサーバの高信頼性化(セッション21 e-ラーニング(インターネット・マルチメディア利用教育を含む)I)
- (72)個別の学習進捗に対応したe-Learning教材表示制御システム(セッション21 e-ラーニング(インターネット・マルチメディア利用教育を含む)I)
- 拡張ペトリネットによる並列システム設計とエンジンプログラムの試作(コンカレント工学理論と応用一般)
- [特別講演]信州大学インターネット大学院におけるサーバ運用の高信頼化について(リッチメディア,信頼性・セキュリティ,一般)
- 信州大学インターネット大学院におけるマルチメディア教材の利用と履修状況について
- (25)設計製作教育における3次元モデルに関する考察(第7セッション 教育システム(実験・設計製図等)(II))
- (24)ものづくり教育における個人製作とグループ製作(第7セッション 教育システム(実験・設計製図等)(II))
- 2P1-A03 高所レスキューを題材としたロボット製作
- ロボット製作を通したグループ学習の分析
- 2A1-A5 学生の視点から見た21世紀に役立つロボットの製作(78. もの作り教育とメカトロニクスI)
- 大阪府立高専システム制御工学科における福祉技術に関する研究
- Team-Teachingによるロボット製作の実践
- (65)Team-Teachingとグループ学習によるロボット製作 : 阪府高専システム制御工学科における6年間のシステム設計研究(第17セッション 教育研究指導(II))
- 2P2-12-012 指漢点字ロボットの試作
- 1P1-81-134 ロボットによる流鏑馬
- 信州大学インターネット大学院におけるマルチメディア教材の利用と履修状況について
- ネットワークサービスの可視化を主眼に置いた戦略的監視手法の提案 (インターネットアーキテクチャ)
- 量子回路と分岐,量子ニューロ計算の基礎理論
- ものづくり導入実習のための電子情報教材の制作 : e-learning を用いた技術伝達の試み
- 長距離無線LANと広域CATV通信網接続による山岳医療情報ネットワークの構築
- C-011 上位ハードウェア設計言語Melasy+による自己回復機能付きFIFOメモリの記述と検証(ハードウェア・アーキテクチャ,一般論文)
- B-020 UML記述の仕様からSPINモデル検査用PROMELAモデルへの自動変換(B分野:ソフトウェア,一般論文)
- 人道的埋設地雷探知技術
- (71)ストリーミングメディアに連動させるe-Learning向け電子出版物の遠隔制御(第19セッション インターネット・マルチメティアの利用(I))
- M-065 P2P仮想ネットワークにおける移動体接続の永続化プロトコルとモデル検査(ユビキタス・モバイルコンピューティング,一般論文)
- C-038 Time-Petri Netを用いた非同期回路のモデル化と階層化設計(ハードウェア・アーキテクチャ,一般論文)
- C-035 ハードウェア上位設計HDCamlから形式記述言語LOTOSへのコード生成と論理回路ライブラリの構築(ハードウェア・アーキテクチャ,一般論文)
- B-014 VDM-SLの陽仕様記述からLispファミリ言語Schemeへの変換(ソフトウェア,一般論文)
- データ通信に用いるCATV網上り回線の雑音低減について(画像符号化・通信・ストリーム技術および一般)
- データ通信に用いるCATV網上り回線の雑音低減について
- データ通信に用いるCATV網上り回線の雑音低減について
- データ通信に用いるCATV網上り回線の雑音低減について
- 拡張ペトリネットとXMLをベースとしたファイルサーバの設計と実装
- 拡張ペトリネットとXMLをベースとしたファイルサーバの設計と実装
- CATVの上り回線の広帯域化に関する研究
- C-22 拡張ネットモデルによるNFSサーバプロセスの設計と動作の検証(ネットワークシステム,C.アーキテクチャ・ハードウェア)
- A-12-1 色付き論理ペトリネットを用いたNFSサーバプロセスのコンカレント設計
- 拡張ネットモデルによるNFSプロセスのモデル化とXMLを用いた実装
- (72)信州大学インターネット大学院の概要と今後の展望(第19セッション インターネット・マルチメティアの利用(I))
- 学習進捗状況に基づいたe-Learning教材表示制御システム (組織内教育におけるe-Learningの新しい展開)
- 信州大学インターネット大学院の経緯と現状
- ハードウェア化を想定したk-SD数の拡張(リッチメディア,信頼性・セキュリティ,一般)
- 遠隔講義におけるストリーミングメディアと電子出版物の連動手法 (シミュレーション(Virtual Reality、ゲームを含む))
- C-002 上位ハードウェア設計言語Melasy+によるVHDLコード生成と動作検証(C分野:ハードウェア・アーキテクチャ,一般論文)
- 1M-4 上位言語Melasy+による自己テスト機能付バスアービタの設計とNuSMVを用いた検証(モデリング・上流設計,学生セッション,アーキテクチャ,情報処理学会創立50周年記念)
- 1M-3 上位ハードウェア設計言語Melasy+に対する仕様パターン埋め込みと展開(モデリング・上流設計,学生セッション,アーキテクチャ,情報処理学会創立50周年記念)
- IRカメラによる埋設対人地雷の探知技術
- 信州大学インターネット大学院計画について
- 信州大学バーチャル大学院計画について
- 弱非線形系H∞制御における中心多様体と状態フィードバック解
- Mamdani推論法の最適化問題への応用 (情報数理に関連する応用函数解析の研究)
- 時変システムに対する最適ファジィ制御則の存在性
- 時間に依存するファジィ集合族を用いた最適制御に関する一考察 (函数解析学の応用としての情報数理の研究)
- NBV空間のファジィ集合族のコンパクト性とファジィ制御への応用
- 情報リテラシ教育向け大規模エージェントベースシステムの開発と評価--テンプレートマッチング処理を用いた学習結果自動収集の改善 (新しい学習/教育活動を可能にするICT活用とその評価/一般)
- 電子テキストを利用した情報リテラシ教育の実施結果収集を行う大規模エージェントベースシステムの開発と評価
- プルーフチェッカーを用いた論理演算器の設計検証
- トークンを用いたパケット交換システム用バス調停方式
- 画像処理に適した高速リアルタイム復号が可能な2値画像符号とその評価
- 逐次リアルタイム復号処理が可能な2値画像圧縮法
- セルオートマトンの概念を用いた自己回復能力をもつ通信用バッファ
- UMLアクティビティ図からSPINモデル検査用コードの自動生成とWebアプリケーション設計への適用(次世代経営情報技術,一般)
- マルウェアアンパッキングにおけるランタイムライブラリのコード比較によるオリジナルエントリーポイント検出(マルウェア解析,インターネットセキュリティ,一般)
- マルウェアアンパッキングにおけるランタイムライブラリのコード比較によるオリジナルエントリーポイント検出(マルウェア解析,インターネットセキュリティ,一般)