抄録
B-029
Webアプリケーション設計のUMLアクティビティ図に対するセマフォア導入とモデル検査
◎小林　巧（信州大）・山田　豊（プラグマティック・テクノロジーズ）・和﨑克己（信州大）
UMLアクティビティ図は振る舞い図に属するダイアグラムで，処理の実行順序や条件，制御などを表現できる．他方，ソフトウェアの上流設計仕様を形式言語でモデル化し，自動検査ツールを用いて動作検証あるいは反例を検出するというアプローチが注目されている．SPINはモデル検証ツールの一つであり，検証対象の振る舞いの全状態を探査し検証条件を充足するかを検査する．本報告では，同期機構などに対応するように拡張された従来研究で開発中のUML図からのPROMELA自動変換器を用いて，Webアプリケーションに適用した結果について述べる．基本的な同期機構であるセマフォアを導入し複数ユーザが更新対象とするファイルロックの排他制御に利用した．