本日はこちら。

先週から続く、要求レベルでのモデル検査関連のお話です。

まとめると、

・ビジネスプロセスモデリングの分野で、シーケンス図を使ってプロセスを記述

・シーケンス図を使うのは時間制約が重要だから

・UPPAALでシーケンス図を状態遷移でモデル化し、モデル検証を実施する。最終状態に到達できればビジネスプロセスが矛盾がないことが言える

という話のようです。

気になった点を引用します。

ビジネスプロセスとは、ある事業目的を達成するために、企業間または企業内で行われる作業およびその作業の順序や条件などを定義して一連の業務の流れを表す言葉

なるほど、UMLは基本ソフトウェアの話をしているとおもっていたのですが、人を含めたシステム（むしろ主に人かな）を対象に使うこともできますね。

標準BPM言語のひとつであるUML

そうなんですね、まったくこの分野に疎いので知りませんでした。

シーケンス図における時間表現は代表的なもので時間制約と持続制約があり

最近astahで書いていて、確かに二つありました。説明を書いてくれていますが正確には理解できていない気がします。勉強します。

シーケンス図でビジネスプロセスを表現する場合、まず何をライフラインとするかを決める必要がある

この論文では二つ挙げられていて、「組織や業務」もしくは「タスクやアクティビティ」とのことです。直感的には前者です。後者はあまりイメージができないですね。ライフラインを何にするかは、どの詳細度で物事を表現するかによる気もしてきました。うーん経験がなくてダメですね。

UPPAALによるBPのモデル化と検証

特に詳しい説明もなく、シーケンス図がUPPAAL（状態遷移モデル）でモデル化できるという話になっています。これ自然なのでしょうか。わからん。シーケンス図がモデル検証できる、という話になるなら個人的には結構うれしいのですが。調べてみる必要がありそうだ。

そもそもの知識を説明してくれている論文だったので、新しいポイントがどこにあるかがわかりにくかったですが、少なくともシーケンス図のモデル検査が非現実的なものではないことがわかったので、収穫です。