UMLアクティビティ図からSPINモデル検査用コードの自動生成における並列処理拡張とAjaxアプリケーション設計への適用

• Item type: SIG Technical Reports(1)
• 公開日: 2012-05-14
• タイトル: UMLアクティビティ図からSPINモデル検査用コードの自動生成における並列処理拡張とAjaxアプリケーション設計への適用
• タイトル / 言語: en
• タイトル: Extension for the Parallel Processing in Automatic Generation from UML Activity Diagram to SPIN Model Checking Code and its Application to Ajax Application Design
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 形式手法
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: (株)プラグマティック・テクノロジーズ
• 著者所属: 信州大学工学部情報工学科
• 著者所属(英): en
• 著者所属(英): Pragmatic Technologies Co. Ltd.
• 著者所属(英): en
• 著者所属(英): Department of Computer Science & Engineering. Faculty of Engineering, Shinshu University.
• 著者名: 山田, 豊; 和﨑, 克己
• 著者名(英): Yutaka, Yamada; Katsumi, Wasaki
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 筆者らが，以前に試作したUMLアクティビティ図からPROMELAで記述された検証用モデルに自動変換する変換器において，UMLアクティビティ図のフォークノード・マージノード等の並列処理記述を扱えるように拡張し，非同期通信により並列処理を伴うAjaxアプリケーションのモデルも扱うことができるようにした．提案手法の評価のため，Ajaxを用いた業務アプリケーションの画面遷移設計に適用実験を行った．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: We extended the converter that converts automatically the UML activity diagram into the SPIN model checking code PROMELA, and enabled it to treat parallel processing description, such as a fork node and merge node of an UML activity diagram. The model of Ajax application with parallel processing by asynchronous communication can also be treated. We modeled the screen transition design of an Ajax application as an evaluation of the proposed method.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10112981
• 書誌情報: 研究報告ソフトウェア工学（SE）; 巻 2012-SE-176, 号 10, p. 1-8, 発行日 2012-05-14
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会