EIC 電子情報通信学会 2014 年総合大会のポスターセッションに参加して

特集
学生の研究活動報告−国内学会大会・国際会議参加記 20
EIC 電子情報通信学会 2014 年
総合大会のポスターセッション
に参加して
小
原
正
3．クラス図・ステートマシン図・
シーケンス図間整合性検証
クラスはオブジェクトの雛形であり，その状態を
義
Masayoshi KOHARA
情報メディア学専攻修士課程
規定するインスタンス変数と，それら変数の更新，
参照を行うメソッドを内蔵する．
2年
1．はじめに
今回私は，2014 年 3 月 18 日から 2014 年 3 月 20
図1
クラス図例
日まで新潟大学で開催された，電子情報通信学会の
2014 年 3 月 19 日の部に参加した．この学会で私
ステートマシン図は各オブジェクトのイベントに
は，UML モデルの静的特性と動的特性間整合性評
よる状態遷移を記述したもので，状態遷移はメソッ
価という題目で，ポスターセッションを行った．
ド実行によるインスタンス変数の更新を伴う．
2．研究背景・目的
UML（Unifird Modeling Language）はオブジェク
図2
ステートマシン図例
ト指向開発におけるモデル記述言語として広く普及
している言語である．UML は 13 種類のダイアグ
シーケンス図は複数オブジェクト間の相互作用を
ラムから表記法が定義され，これを用いることで開
表すが，各オブジェクトはメッセージの送受信によ
発の上流工程から下流工程に至るまでの様々な工程
り状態遷移を行うものと考えられる．このことによ
において，システムの構造や振る舞いといった複数
り，同一オブジェクトが前記三種類の図に出現する
の視点から対象をモデリングすることが可能であ
場合，各図における状態が相互に矛盾しないことを
る．しかし優れた表現力をもっている UML には反
整合性の条件とできる．
面，形式性に欠けモデルには曖昧さが残るという欠
点を持っている．この原因として，UML 図自体の
仕様が完全に形式化されていない点が挙げられる．
このため UML 図によって作成されるモデルにも曖
昧さが含まれる可能性が高いと考えられる．本研究
では，この曖昧さが残っている可能性がある UML
間の整合性問題を取り扱う．今回取り扱う UML
は，クラス図，ステートマシン図，シーケンス図と
図3
シーケンス図例
4．VDM＋＋によるクラス記述
する．システムの構造面を表すクラス図を形式仕様
システムはクラスを定義し，クラスを具象化して
記述言語 VDM＋＋に，動作面を表すステートマシ
作成したオブジェクト同士が協調動作を行うことで
ン図，シーケンス図をモデル検査ツールの一つであ
動作する．クラス図はシステムの静的な構造を表す
るカラーペトリネット（CPN）に変換し整合性を検
ダイアグラムであり，分析，設計などシステム開発
証する．
の工程で利用される．クラス図のメソッドを厳密に
記述するために形式仕様記述言語の一つである
― S-93 ―
VDM＋＋を用いる．クラス図で記述される属性や
グメントを使用する場合は，プレースの後のトラン
操作は，システム内の変数・機能として扱われるた
ジションが二つに分岐し，それぞれ if と else を用
め VDM＋＋によってインスタンス変数，関数や操
いて条件分岐させガード条件を記述することで
作になりうるものを抽出し記述する．この手順で
CPN への変換ができる．
VDM＋＋を記述する．
6．CPN による整合性検証
5．ステートマシン図・シーケンス図から
CPN への変換
CPN モデルは CPN tools によりシミュレーショ
ン可能となる．このシミュレーションによりプレー
ステートマシン図から CPN に変換する場合まず
ス内のトークン値が変化するが，この値がオブジェ
開始状態，終了状態，入場点，退場点をプレースで
クトの状態を構成する．これらの状態が 2 節の整合
表す．また遷移において，ガード条件はトランジシ
性条件を満たすかどうかを判定する関数を作成し，
ョンの発火条件に変換し，イベント名は入力プレー
これをガードとするトランジションを必要なプレー
ス名に変換，アクティビティ名は出力プレース名に
スに接続することで，整合性の判定が可能となる．
変換する．
ステートマシン図では各状態に対応するプレース，
シーケンス図では状態不変式と対応するプレースが
この対象となる．
7．まとめ
図4
本研究では，UML の曖昧さから発生する可能性
ステートマシン図から CPN へ変換例
のある不整合問題を解決するために，ソフトウェア
シーケンス図から CPN に変換する場合は，複合
の静的側面を表す UML モデルのクラス図とと動的
フラグメントを用いる場合とそれ以外では変換方法
側面を表す UML モデルのステートマシン図，シー
が異なる．複合フラグメントを使用しない場合は，
ケンス図を対象とした，整合性検証の手法を提案し
メッセージの送受信がライフライン上を上から下へ
た．異なる UML モデルを検証するために，クラス
進んでいくだけなので，メッセージの送受信をアー
図を形式仕様技術言語である VDM＋＋に，ステー
クに変換することで CPN に変換できる．複合フラ
トマシン図，シーケンス図を一度 CPN に変換しこ
れをもとに整合性検証を行うという手順を取った．
CPN を使用する理由としては，比較的構造が簡単
であり，表現力が高く，専用のツールが豊富なため
である．本研究により，UML モデルが CPN に変
換することが可能であると判明した．CPN に変換
された UML モデルは CPN-Tools により自動検証
が可能となる．
8．おわりに
ご指導いただいた新川芳行教授，ご支援いただい
た方々に感謝いたします．
図5
シーケンス図から CPN へ変換例
― S-94 ―

Download Report