論文：シーケンス図とステートチャート図の相互変換に着目したソフトウェア分析・設計に関する研究
本日はこちらです。
先日まではユースケースと状態遷移の変換的な話でしたが、今度はシーケンス図から、です。UML、形式検証という文脈としては同じです。
まとめると、
・シーケンス図から状態遷移図を生み出す手法
・既往の研究があるが、状態遷移図の修正をシーケンス図に反映するという機構を入れた点が新しい
・シーケンス図としてはMSC（UMLではなく）を使用
ということです。
気になった点を引用します。
シーケンス図とステートチャート図を相互に変換する方法を提案する
お願いします！興味あります！個人的には、シーケンス図って一方通行だからなんだか元に戻るというイメージがないんですよね。単純に最終状態を初期状態と同じに置くのかな。
シーケンス図と呼ばれるものとして、Message Sequence Charts(MSC)やUMLシーケンス図などがある
MSCというものがあるのを知らなかったです。ある程度有名なのでしょうか。
WikipediaではUMLしか書かれていませんが。まぁ大差ないものだと思っておきます。
MSCでは、bMSCとhMSCと呼ばれる2つの図からなる
なるほど！hMSCが上位で、bMSCを呼ぶ形になっているのですね。これは結構わかりやすいかも。逆にUMLってこれどうやって表現するんでしたっけ…。アクティビティ図とシーケンス図の複合でしょうか。MSCはシーケンス図と言っておきながら純粋なシーケンス図だけではないですからね。
ステートチャート図としてUML Version1.5のステートチャート図を用いた
ステートチャートはUML使うんですね。だったらシーケンスもUML使ってほしい気がしますが。やっぱり何かMSCを使う意図があったのでしょう。できればその理由も書いてほしかったなぁ。
Whittleらは、複数の独立したシーケンス図からステートチャートを生成した
これ読みます。こっちの方が大事かもしれない。2000年ICSEのカンファレンスペーパーのようですね。
MSCの矛盾を検出
まずはMSC単体で矛盾チェックをするようです。データフロー解析を行うとのこと。どんなことをやっているんだろう。気になる。ここら辺単体で諸々論文がありそうですね。
1つのオブジェクトにつき1つのステートチャート図を生成する
てことはライフラインごとってことですかね、UMLで言うと。MSCのメッセージ受信終了から次のメッセージの送信開始までを状態とみなす、ということです。各オブジェクトが実際に状態を持つかどうかに関わらず、シーケンス図の特徴からそうみなしてしまうということですね。ふむふむ。
また知らない話がいろいろ出てきましたが、参考にはなりました。