@techreport{oai:ipsj.ixsq.nii.ac.jp:00082100,
 author = {山田, 豊 and 和﨑, 克己 and Yutaka, Yamada and Katsumi, Wasaki},
 issue = {10},
 month = {May},
 note = {筆者らが，以前に試作したUMLアクティビティ図からPROMELAで記述された検証用モデルに自動変換する変換器において，UMLアクティビティ図のフォークノード・マージノード等の並列処理記述を扱えるように拡張し，非同期通信により並列処理を伴うAjaxアプリケーションのモデルも扱うことができるようにした．提案手法の評価のため，Ajaxを用いた業務アプリケーションの画面遷移設計に適用実験を行った．, 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.},
 title = {UMLアクティビティ図からSPINモデル検査用コードの自動生成における並列処理拡張とAjaxアプリケーション設計への適用},
 year = {2012}
}