日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

形式言語 CSP#による SysML ステートマシン図の形
式化
安藤 崇央 †

谷津 弘一 †孔 維強 †

久住 憲嗣 ‡

福田 晃 †

SysML ステートマシン図は，システム開発においてシステム中のあるブロックの振る舞いを記述するのに利用されるモデル図の一つである．ステートマシン図のモデル検査を可能とするため，Zhang らはステートマシン図をモデル
検査器 PAT の入力言語である形式言語 CSP#を用いた表現に変換する手法を提案している [23]．本稿では，Zhang
らによって提案された変換規則に対して，いくつかの規則に対する修正と新しい変換規則の追加を提案する．まず，ステートマシン図の定義にてらして不適切な規則となっている 3 つの規則についての修正規則を与えた．次に，これまで変換規則の与えられていなかった 2 つの擬似状態に対する変換規則を新たに追加した．また，これらの変換規則を含んだ自動変換システムを，Web ベースの MDD ツール上に実装し，より一般的なステートマシン図に対してモデル検査が適用可能な環境を構築したことを報告する．
SysML is a language for systems modeling. State machine diagrams are one type of the SysML diagrams
and are used to describe the behavior of blocks in the system under consideration. In order to reduce development costs, it is desirable that the correctness of the designed models (that capture the block behavior)can be verified in the system design phase. The work in [23] proposed a formalization of SysML statemachine diagrams in which the diagrams were translated into CSP# processes that could be verified by thestate-of-the-art model checker PAT. In this paper, we make several modifications and add new rules to thetranslation described in that work. First, we modify several translation rules, which we think are inappropriately defined according to the SysML definition of state machine diagrams. Next, we add new translation
rules for two components of the diagrams – junction and choice pseudostates – which have not been dealt
with previously. And then, we are implementing the automatic translation system on a web-based model
driven development tool, which reflects on our translation rules. As the contribution of this work, we canachieve more reasonable verification results for more general SysML state machine diagrams.

の図的表現として 9 種の図が用意されており，ステー

1 はじめにトマシン図はその一つである．ステートマシン図は，

Systems Modeling Language (SysML) [18] はモシステムのあるブロックのライフサイクルにおける振デリング言語の一つで，システム全体のモデル化をる舞いを状態遷移系として表現した図である．ステー

サポートするため，ソフトウェアのモデリング言語

トマシン図を含む SysML の各図に対しては，厳密なのデファクトスタンダードである Uniﬁed Modeling

意味論が定義されておらず，記述の正しさの確認の障

Language (UML) [17] から派生したモデリング言語

害となっており，とくに，形式的な手法を用いた検証である．SysML には，システムのモデル記述のための妨げとなっている．
一方，状態遷移系の形式的な検証手法として，モデ

Formalization and Model Checking of SysML State
Machine Diagrams by CSP#
Takahiro Ando† , Hirokazu Yatsu† , Weiqiang Kong† ,Kenji Hisazumi‡ , Akira Fukuda† , † 九州大学 大学院
システム情報科学研究院，‡ 九州大学 システム LSI 研
究センター, † Graduate School of Information Science and Electrical Engineering, Kyushu University,‡ System LSI Research Center, Kyushu University.

ル検査技術 [6] がよく知られている．モデル検査は，状態遷移系を形式的な言語でモデル化し，そのモデルが望まれる性質を満足するかどうかを形式的かつ網羅的に確認する技術である．モデル検査ツールには，よく知られたものとして SPIN [11], NuSMV [3]，PAT[21] などがある．これらのツールを利用する際には，

状態遷移系は，それぞれのツールに対応した形式言語

サーベイは [2] に詳しい．ステートマシン図に対するでモデル化され，モデルが満たすべき性質も，線形時モデル検査器としては，SPIN [11]，SMV [14], FDR

相論理 (Linear Temporal Logic, LTL) や，計算木論[22] などをベースにしたものがある．

理 (Computation Tree Logic, CTL) などの形式的な言語を用いて記述される．

ステートマシンを Promela 言語に変換して SPIN
でモデル検査を行う手法が， [12] で提案されている．

PAT は SPIN に 匹 敵 す る モ デ ル 検 査 ツ ー ル で ，

この研究では，ステートマシン図の基本の要素しか取モデルの記述には CSP#という形式言語を用いる．

り扱われていない．そのほかに SPIN をベースとし

CSP#は Hoare の Communicating Sequential Pro-

たツールに vUML [13] があるが，詳しい形式化手法

cesses (CSP) [10] に共有変数の記述や条件選択などについては述べられていない．

の記述を追加し拡張した形式言語である．CSP#のステートマシンを SMV の入力言語に変換し形式ベースとなる CSP は，プロセス代数の一種で並行シ化するものに [4] がある．そこでは，シンボリックモ

ステムの形式化などに用いられる言語である．CSP

デル検査のために，各状態やイベントに変数を割りや CSP#は，並列実行されるプロセスの記述や割り当てている．そのため，小さな図であっても，変数の込みの処理などの記述に適する．

増加によってシンボリックモデル検査中の状態爆発

本稿では，SysML ステートマシン図を CSP#を用問題が顕在化しやすい． [5] は，UML ステートマシ

いた記述に変換し形式化する手法について述べる．こン図の意味論とシンボリックなエンコード法を示し，の形式化により，ステートマシン図に対してモデル検

NuSMV で検証を行っている．ステートマシンのシ査ツール PAT を用いたモデル検査が可能となる．ス

ンボリックエンコード法は [16] でも与えられており，

テートマシン図についての CSP#への変換について

この研究では SAT ソルバベースの有界モデル検査には，先に [23] で提案されているが，本稿では [23] にて検証を行う手法が提案されている．

おいてステートマシン図の定義に照らして妥当ではステートマシンをプロセス代数に形式化するものないと思われる変換規則について修正した変換規則

としては， [8], [20], [15], [23] などがある． [8] では，と，取り上げられていなかったステートマシン図の 2

ステートマシンをプロセス代数 Algebra of Commu-

つの要素についての変換規則を与える．また，本稿でnicating Process (ACP) ベースの言語 mCRL2 [7] で与えた変換規則について，簡単なユーザ認証システム

形式化し，そのモデルを mCRL2 ツールセットを用のステートマシン図に適用したケーススタディを交えいて検証する方法について紹介している． [20], [15],

説明と評価を行う．

[23] は，本稿と同じくプロセス代数 CSP に変換する

本稿の構成は以下の通りである．2 節では，関連研ことでステートマシンを形式化している． [15] は，状究について述べる．3 節では，ステートマシン図から態のもつ振る舞い entry, exit について取り扱ってい

CSP#記述への変換規則について述べる．4 節では，る．しかし，擬似状態を扱うような複雑な遷移につい

簡単なユーザ認証システムを例題としてステートマては対応していない． [15] では形式化されたモデル

シン図から CSP#記述への変換について説明およびの検証に，モデル検査器 FDR2 を用いている．

評価を行う．5 節では，現在開発中のステートマシン[23] は本稿の直接的な先行研究になる．この研究

図から CSP#記述への自動変換システムについて述

では，ステートマシンを CSP ベースの言語 CSP#にべる．最後に，6 節にて本稿のまとめと今後の展望に変換し形式化する手法を与えている．本稿では， [23]ついて述べる．

にて提案されている変換規則について，不適切な箇所に対する修正と新たな変換規則の追加を行う．

2 関連研究ステートマシン図に対して，形式的な検証技術や形式的解析を適用しようという研究は多くありその3. 2 CSP#

3 ステートマシン図の形式化

Communicating Sequential Processes (CSP) [10]本節では，まずステートマシン図の各要素と形式

はプロセス代数の 1 種で，並行システムの相互作用パ

言語 CSP#について簡単な説明を行い，その後にスターンを記述する形式仕様記述言語である．CSP#はテートマシン図を CSP#を用いた記述に変換する変CSP に条件分岐や共有変数を追加して拡張された言

換規則について述べる．

語で，モデル検査器 PAT のモデル記述用言語である．
以下に，本稿で用いる CSP#のサブセットとそれ

3. 1 SysML ステートマシン図
SysML を用いたモデル記述では，あるブロックの状態に依存する振る舞いを記述するため，ステートマ
シン図が用いられる．ステートマシン図は，状態と状態間の遷移からなる．ステートマシン図の構文や表記法は [18] に定義されている．
状態は，ブロックのライフサイクルにおける状況を表し，その状況は一般的に，ある不変条件が成立することとして表される．各状態は，入状時振る舞

ぞれの直観的な意味を簡単に説明する．
定義 3.1

CSP#におけるプロセス P は，以下のように定義される．

P ::=Stop | Skip | e{prog} → P | P1 ; P2 | P1 □P2| P1 ∥ P2 | P1 |||P2 | [b]P | P1 △P2
ただし，P1 , P2 はプロセス，e はオプションとしてシーケンシャルプログラム prog をもつイベントの名
前，b, b1 , b2 はブール式とする．

い (entry)，退状時振る舞い (exit)，在状時振る舞い(do) を持つことができる．entry は，ブロックがそのStop はデッドロックプロセスを表し，Skip はプロ状態に入ったときに，exit は，ブロックがその状態かセスの正常終了を表す．e → P は，イベント e が起きら出たときに実行される．また，do は entry の後にた後にプロセス P として振る舞うプロセスを表す．e

実行され，その振る舞いが完了するか，ブロックがそがシーケンシャルプログラムを持つ場合は，そのプロの状態から出るまで実行を続ける．

グラムをアトミックに実行した後にプロセス P としステートマシン図の状態には，アトミックな状態とて振る舞う．P1 ; P2 は，プロセス P1 として振る舞っ

合成状態などがある．アトミックな状態は単純な状態

た後に，続けて P2 として振る舞うプロセスを表す．

で，内部にサブ状態を一つも持たない．合成状態は，

P1 □P2 は非決定的選択をもつプロセスを表し，その一つまたは複数の領域を持ち，それぞれの領域にサブ振る舞いは，イベントによりプロセス P1 , P2 のどち状態を持つ．

らとして振る舞うかが決定される．P1 ∥ P2 は並行合状態間の遷移は，トリガ，ガード，効果の三つの要成プロセスで，どちらのプロセスにも現れるイベント

素を持つ．イベントは遷移をアクティブにするトリガで同期する．P1 |||P2 は並行プロセスのインターリー

として働く．遷移は，イベントが生起し，ガード条件

ビング合成を表す．[b]P は，ガード条件付きプロセが成立する場合にのみ発火可能となる．遷移が発火すスを表し，ブール式 b が成立するとき P として振る

ると，遷移の効果が実行され，状態が遷移先の状態に舞う．P1 △P2 は割り込みを表すプロセスで，P2 の最変化する．

初のイベントが生起するまで P1 として振る舞い，そまた，ステートマシン図は，様々な擬似状態も持のイベントが起きた後は P2 として振る舞う．

つ．代表的なものとしては，ステートマシンの開始や終了を表す初期擬似状態，終了状態や，複数の遷移を

3. 3 変換規則

まとめるための表現として連結擬似状態，選択擬似状

本節では，ステートマシン図から CSP#記述への態などがある．

変換規則について述べる．ステートマシン図中の各状
態，遷移，擬似状態は CSP#におけるプロセスとして表現され，ステートマシン全体も一つのプロセスとして表現される．また，ステートマシン図中の各イベとは，ステートマシンが終了状態ではない状態で正常

ントは，CSP#のイベントとして表現する．

終了をすることを許容していることになり不適切であステートマシン図の各要素についての変換規則を表る．また，CSP#では，等式 Stop△P = P という事

1 にまとめた．表中では，簡単のためステートマシン

実から，tr (do) を，tr (do); Stop に修正することで出図から CSP#への変換規則を関数 tr として表し，各力遷移を無視する振る舞いを禁止することができる．

要素 e について変換規則を適用した結果の CSP#表

続いて，複数の遷移をまとめるための表現としてス

現を tr(e) としている．
表 1 は，先行研究 [23] で提案されたものをベースにテートマシン図中で用いられる連結擬似状態と選択
擬似状態についての変換規則を新たに与える．

しているが，いくつか異なる点がある．先行研究では，

連結擬似状態

状態の entry, exit と遷移の効果の表現に CSP#の連結擬似状態は，複数の遷移の共通部分をまとめて

atomic 演算子を用いていたが，本稿ではこれを用い記述するために用いられる．したがって連結擬似状態ていない．これは，これらの振る舞いについてアトの CSP#記述への変換は，入出力遷移の情報からまミックとすると危険な振る舞いを見逃がしてしまう

とめられた遷移をほどき，元々の遷移それぞれについ可能性があると考えるためである．実際のシステムての変換を行えばよい．

では，これらの振る舞いがアトミックな振る舞いとして定義されているとは限らない．アトミックとしてし
まうと，インターリービング合成による振る舞いのS1

パターンが減ってしまい，モデル検査時に，問題となるアクションの実行順序を無視してしまう可能性が
ある．

S2

e1

[g1]/a1e2[g2]/a2

S3
S4

図 1: 連結擬似状態

また，状態の変換規則にも変更点が 2 つある．1 つは，出力遷移の割り込みを受ける対象から entry を表す tr (entry) プロセスを除外したことである．これある連結擬似状態によりまとめられた遷移をほど

は，状態の entry が，そのほかの振る舞いや出力遷移いた時に得られる遷移の集合 Transunwound は，連結の発火前に完了していなくてはならないとのステー

擬似状態の入力遷移の集合を Transin ，出力遷移の集トマシン図の規定を反映するためである．

合を Transout として，次のように与えられる．

もう一つは，状態の do を表す tr (do) プロセスとデッドロックを表す Stop プロセスを “;” で連結したことである．従来の変換規則で変換した CSP#のプ

Transunwound= {t | ∃t′ ∈ Transin . ∃t′′ ∈ Transout .
(source(t) = source(t′ ) ∧ event(t) = event(t′ )遷移も発火しなくとも，プロセスは正常終了する” こ∧ guard(t) = guard(t′′ ) ∧ eﬀect(t) = eﬀect(t′′ ))∧ target(t) = target(t′′ ) }とを許す記述が含まれてしまう．これは以下の 2 つのここで，5 つの関数 source, event, guard, eﬀect, tar-

事実から導かれる．

get はそれぞれ，引数に遷移をとり，その遷移の遷移

ロセスには，“do の振る舞いが終了した後，どの出力• do の変換規則から明らかな様に，CSP#において tr (do) プロセスが完了すると Skip プロセスとして振る舞う．

元の状態，トリガとなるイベント，ガード，効果，遷移先の状態を返す関数とする．
連結擬似状態とそれに関わる遷移の CSP#記述へ• CSP#の意味論では，Skip△P というプロセスの変換は，Transunwound の各要素に独立に変換を施の振る舞いとして，プロセス P を実行せずに正したものとなる．たとえば，図 1 中の連結擬似状態

常終了することが許される．

とその入出力遷移は，以下の 4 つのプロセスに変換

このような記述を変換後の CSP#の記述に含めるこ

表 1: ステートマシン図から CSP#記述への変換規則
要素

CSP#

コメント

ステートマシン smtr (sm) = tr (i), ただし i は sm 中の最上位レベ
ルの初期擬似状態とする．
tr (i) = tr (s), ただし s は，i を遷移元とする遷移の遷移先の状態とする．
tr (f ) = Skip;tr (s) = tr (entry); ( (tr (do); Stop) △ (tr (t1 )□ tr (t2 ) □ · · · □ tr (tn )) ), ただし，t1 , t2 , . . . ,tn は，s を遷移元の状態とする遷移とする．
tr (entry) = e1 → e2 → · · · → en → Skip;, ただし e1 , e2 , . . ., en は，入状振る舞い中のアクション列を表す．
tr (t) = [guard](event → tr (exit); tr (eﬀect);tr (st ) ), ここで，exit は，遷移元の状態の退状時
振る舞い，st は遷移先の状態を表す．
tr (cs) = tr (entry); ( ((tr (do); Stop) ||| tr (r1 )||| tr (r2 ) ||| · · · ||| tr (rm )) △ (tr (t1 ) □ tr (t2 )□ · · · □ tr (tn )) ), ただし r1 , r2 , . . . rm は，cs
中の領域を表し，t1 , t2 , . . . , tn は，合成状態を遷移元とする遷移を表す．

合成状態中の領域もほぼ同様．

初期擬似状態 i
終了状態 f
アトミックな状態 s

入状時振る舞い entry

遷移 t

合成状態 cs

される．

S1

(
)
P13 = [g1 ] e1 → tr(exit(S1 )); tr(a1 ); tr(S3 )()
P14 = [g2 ] e1 → tr(exit(S1 )); tr(a2 ); tr(S4 )()
P23 = [g1 ] e2 → tr(exit(S2 )); tr(a1 ); tr(S3 )()
P24 = [g2 ] e2 → tr(exit(S2 )); tr(a2 ); tr(S4 )S2どの領域の初期擬似状態についても同様．
ステートマシンの正常終了を表す．
tr (do) に続くプロセスが Skip では
なく Stop であることに注意する．
状態の退状時振る舞い (exit)，在状時振る舞い (do)， 遷移の効果についても同様．

e1/a1[g3]/a3e2/a2[g4]/a4

S3
S4

図 2: 選択擬似状態

ここで，関数 exit は，引数に状態をとり，その状態のexit を返す関数とする．また，プロセス P13 , P14 は，

選択擬似状態への入力遷移は，状態間の遷移とほぼ

状態 S1 の出力遷移を変換したものとして，tr(S1 ) 中

同様に変換を行う．ただし，遷移先状態を表すプロセで次のように参照される．

スの代わりに，出力遷移の集まりを表す CSP#のプ

tr(S1 ) =tr(entry(S1 ));()(tr(do(S1 )); Stop) △ (P13 □ P14 )プロセス P23 , P24 も同様に tr(S2 ) 中で参照される．

ロセス Pchoice を用いる．
選択擬似状態からの各出力遷移もまた，状態間の遷移とほぼ同様に変換を行う．ただし，遷移元状態のの選択擬似状態

exit についてのプロセスは省略する．これは，これら選択擬似状態は，連結擬似状態と同様，入出力遷移の出力遷移の遷移元状態は選択擬似状態であると見を複数持つ擬似状態である．連結擬似状態とは，出なすためである．出力遷移の集まりを表す Pchoice プ

力遷移のガード条件を評価するタイミングが異なる．

ロセスを次のように定める．

選択擬似状態では，出力遷移のガード条件は，選択擬

Pchoice = tr(t1 ) □ tr(t2 ) □ · · · □ tr(tn )似状態に到達するまで評価されない．つまり，選択擬

ただし，t1 , t2 , . . . , tn は選択擬似状態の出力遷移と似状態への入力遷移の効果の結果が出力遷移のガー

する．

ド条件の評価に影響を与える．以上をふまえ，選択擬
似状態とそれに関わる遷移は，入力遷移と出力遷移に分けて CSP#記述に変換する．

図 2 中の選択擬似状態とそれに関わる入出力遷移

を CSP#に変換すると次のようになる．

P1 = e1 → tr(exit(S1 )); tr(a1 ); Pchoice
P2 = e2 → tr(exit(S2 )); tr(a2 ); Pchoice()
P3 = [g3 ] tr(a3 ); tr(S3 )()
P4 = [g4 ] tr(a4 ); tr(S4 )

略化され次のように表すことができる．

idle() = (StartUp → initializing())□ (TurnOﬀ → TopLevelFinal());
diagnosing() = (SystemOK → operating())□ (SystemNG → idle());

Pchoice = P3 □ P4
ここで，P1 , P2 はそれぞれ，状態 S1 , S2 から選択擬

一方，状態 initializing は，変数 passed の値を変更す

似状態に向かう遷移を表すプロセスで，tr(S1 ) およる振る舞い entry, do を持つ．本稿の変換規則では，こび tr(S2 ) 中で参照される．また，P3 , P4 はそれぞれ，

れらの振る舞いをアクション列ととらえ，CSP#におけ

選択擬似状態から状態 S3 , S4 に向かう遷移を表すプるイベント列へと変換する．CSP#では，イベントにはロセスである．

シーケンシャルプログラム付加することが可能であり，状態 initializing の entry は {passed = false} → Skip,

4 ケーススタディ

do は {passed = true} → Skip と変換される．また，

本節では，図 3 に示す簡単なユーザ認証システムのCSP#記述への変換では，振る舞いで用いられる変数

ステートマシン図を例題として，前節までに述べた変passed の宣言が必要となる．以上により，これらの換規則を用いてステートマシン図から CSP#記述へプロセスを用いて状態 initializing は，次のように変の変換について説明する．以下の説明では，図 3 中の換される．

状態名 “name” をもつ状態について変換規則を適用し得られた CSP#のプロセスを name() と表記する．

var passed = false; /* 共有変数の宣言 */はじめに，ステートマシンの全振る舞いを表すプロ
セスを System() とする．ステートマシンの振る舞い
は，最上位レベルの初期擬似状態から続く振る舞いのことであるから次のように表される．

System() = TopLevelInit();
ただし，TopLevelInit() はトップレベルの初期擬似状態を CSP#記述に変換したプロセスとする．

initializing()= {passed = false} → ( ({passed = true} → Stop)△ ( (TimeOut → idle())□ ([passed == true] operating())□ ([passed == false] diagnosing()) ) );比較のため，先行研究 [23] の変換規則を，状態 ini-

tializing に適用した例を以下に示す．

また，図 1 にも記したとおり，初期擬似状態はその出力遷移が指す状態を，終了状態は正常終了をそれ

initializing()

ぞれ表すため，最上位レベルの初期擬似状態および，= ( {passed = false} → {passed = true} → Skip)

終了状態は次のように変換される．

TopLevelInit() = idle();TopLevelFinal() = Skip;
次にアトミックな状態 idle, initializing, diagnosing
に対する変換について説明する．状態 idle, diagnosing
は，entry, do, exit を持たないため，これらの振る舞
いの変換を表す tr (entry) などはプロセス Skip となる．さらに，CSP#では等式 Skip; P = P が成り立
つため，状態 idle, diagnosing の CSP#への変換は簡△ ( (TimeOut → idle())□ ([passed == true] operating())□ ([passed == false] diagnosing()) );先行研究 [23] での規則による変換において，状態

initializing の entry プロセス {passed = true} は，出力遷移プロセスの割り込みを受ける領域に含まれている．また，本稿で与えた規則を用いた変換では Stopとなる箇所が Skip となっている．以前の変換規則を適用すると，システムの振る舞い全体を表すプロセス

System() は以下の 2 つのイベント列を受理でき，正operating

TurnOff

entry/logged_in = 0
exit/logged_in = 0

ShutDown

idle
StartUp
TimeOut

logged_off

initializing
entry/passed=false
do/passed=true[passed == true][logged_in == 0]

LogIn

LogIn

[passed == false][logged_in<MAX]/ logged_in = logged_in +1

logged_on[logged_in != 0]

SystemNG

diagnosing SystemOK

LogOut/ logged_in = logged _in - 1

図 3: 簡単なユーザ認証システムのステートマシン図
常終了してしまう．

StartUp → TimeOut → TurnOﬀ → Skip
StartUp → {passed = false}→ {passed = true} → Skip
1 つ目のイベント列は，ユーザ認証システムが状態
initializing の entry を実行する前にイベント TimeOut を受理可能であることを意味している．一方，2つ目のイベント列は，システムが状態 initializing に期擬似状態を CSP#記述に変換したプロセスとする．

var logged in = 0; /* 共有変数宣言 */operating()= {logged in = 0}
→ ( (operatingSubInit() ||| Stop)△ (ShutDown → {logged in = 0} → idle()) );あるときにどの出力遷移も発火しないままで正常終合成状態内部のサブ状態 logged oﬀ, logged on は了できることを意味している．しかし，これらの振るどちらも連結擬似状態，選択擬似状態に関係する遷舞いは，SysML ステートマシン図の定義に照らすと移と接続しているため，CSP#記述への変換は注意が

不適切な振る舞いとなっている．したがって，システ必要である．先行研究では，これらの擬似状態に関連

ムはこれらのイベント列を受理すべきではない．本稿した状態や遷移に関する変換規則は与えられておらで提案した変換では，これらのイベント列が受理されず，本稿で提案した新しい変換規則を用いることで，ることはない．

CSP#記述に変換可能となった．

次に，内部に連結擬似状態，選択擬似状態を持つ合合成状態内部の連結擬似状態は，サブ状態 logged oﬀ

成状態 operating の変換について述べる．合成状態

からサブ状態 logged on の遷移と，サブ状態 logged on

operating は振る舞い entry を持ち，この振る舞いはからサブ状態 logged on への自己遷移の 2 本の遷移

内部の状態遷移が開始する前に処理される．その後，をまとめている．どちらの遷移も，トリガが LogIn

合成状態内部の領域の初期擬似状態から始まる状態遷

イベント，ガード条件として [logged in < MAX]，効移が実行される．また，合成状態 operating は，振る果として logged in = logged in + 1 を持つ．連結擬似舞い exit を持ち，この振る舞いは，ShutDown イベ

状態によりまとめられた，これら 2 つの遷移はどちントにより idle 状態へ遷移する際に実行される．このらも次のように変換される．

合成状態を CSP#記述に変換すると，次のようになる．ただし operatingSubInit() プロセスは，内部の初[logged in < MAX]
(LogIn → {logged in = logged in + 1}
→ logged on());
選択擬似状態は変数 logged in の値を 1 減らす効果

た CSP#記述のモデルを利用したステートマシン図のモデル検査について例題を用いて説明する．
たとえば，図 3 のユーザ認証システムのステートマシンが満たすべき要求として次の 3 つの性質を考える．

を持つ入力遷移と，変数 logged in の値を 0 と比較す

1. ステートマシンはデッドロックフリーである．

るガード条件を持つ 2 つの出力遷移を持つ．先に述

2. ステートマシンは logged in > 0 を満たす状態

べたとおり，選択擬似状態では出力遷移のガード条件
は入力遷移の効果の処理後に評価される．そのため，
選択擬似状態の入力，出力遷移はそれぞれ，次のように変換される．

/* 選択擬似状態の入力遷移 */LogOut → {logged in = logged in − 1} → Choice();/* 選択擬似状態の出力遷移 */
Choice() = ([logged in == 0] logged oﬀ())□ ([logged in != 0] logged on());に到達可能である．

3. 変数 logged in は常に 0 ≤ logged in ≤ MAX を満たす．

PAT には組み込みの機能として，CSP#のプロセスに対するデッドロックフリーの検査や，到達可能性検査の機能が備わっている．上記の性質 1, 2 については次のように簡単なアサーションとして記述でき，これを評価することで性質の判定が可能となる．

#assert System() deadlockfree; /* 性質 1 *//* 性質 2*/#deﬁne logged on prop (logged in > 0);以上より，合成状態 operating 内部の状態遷移は次#assert System() reaches logged on prop;のように変換される．
また，性質 3) は，LTL 論理式を用いて次のように

operatingSubInit() = logged oﬀ();表される．

□((logged in ≥ 0) ∧ (logged in ≤ MAX))
logged oﬀ()

ステートマシンがこの LTL で表された性質を満足す= [logged in < MAX]

るかの確認は，PAT の入力として次のようなアサー(LogIn → {logged in = logged in + 1}

ションを定義しこれを評価することで行える．

→ logged on());#deﬁne user num prop((logged in >= 0) && (logged in <= MAX));logged on()= ( [logged in < MAX]
(LogIn → {logged in = logged in + 1}
→ logged on()) )□ (LogOut → {logged in = logged in − 1}
→ Choice());#assert System() | = []user num prop;
上記の 3 つのアサーションを実際に PAT を用いて評価すると，結果はいずれも “valid” となる．
最後に，システムが次の性質 4 を満足するかを確認することについて考える．

4. イベント LogIn が受信される場合は必ず，変数
Choice() = ([logged in == 0] logged oﬀ())□ ([logged in != 0] logged on());
以上のようにして得られた CSP#の記述は，モデル検査ツール PAT の入力として LTL モデル検査に利用できる．ここからは，上記の変換により得られpassed の値は true である．
この性質 4 は，以下のアサーションとして定義される．

#deﬁne passed prop (passed == true);#assert System() | = []( LogIn → passed prop );このアサーションを PAT を用いて評価すると “NOT

ディタのスクリーンショットであり，図 5 はグラフィ

valid” と評価され，反例として次のイベント列が出

カルモデルエディタのスクリーンショットである．さ力される．

らに，clooca はグラフィカルなモデルを，あらかじStartUp → τ → SystemOK→ {logged in = 0} → LogIn

め用意したテンプレートに沿ったドキュメントに変換するテンプレートエンジンと，テンプレートスクリプ

ただし，τ はラベルなしイベントを表す．このイトを編集するためのエディタ機能もあわせもつ．図 6

ベント列は，状態 initializing から状態 diagnosing を

は clooca のテンプレートスクリプトエディタのスク

通ってサブ状態 logged oﬀ に到達し，そのサブ状態

リーンショットである．

でイベント LogIn を受信することを表している．シ

clooca 上でステートマシン図のメタモデルと，本稿

ステムがこの経路をたどって振る舞った場合，イベン

で提案した CSP#記述への変換規則をベースとする

ト LogIn を受信するまで変数 passed の値は false のテンプレートスクリプトを用意することで，グラフィままである．したがって，システムは性質 4 は満たさ

カルなステートマシン図から CSP#記述への変換をないということを，反例によっても確認できる．

自動で行うウェブベースのツールが得られる．clooca

PAT を用いてモデル検査できるプロセスは，ス

上では，メタモデルは JavaScript Object Notation

テートマシン全体を表すプロセス System() のみに限

(JSON) 形式のリストで表現され，テンプレートス

定されることはない．たとえば，これまでの例題でクリプトは，Phython で記述されたテンプレートラ

System() の部分を operatingSubInit() プロセスに代イブラリ Mako [1] のテンプレート形式で記述される．

えると，合成状態 operating の内部状態遷移にのみ

現在，ステートマシン図を含む SysML モデル図の一焦点を当てたモデル検査が可能となる．本稿で与えた部のメタモデルを作成し，clooca 上のアドオンとし変換規則では，各領域の初期擬似状態を CSP#のプて本稿で提案した変換規則をテンプレートスクリプ

ロセスに変換しているためこのような操作が簡単にトとして開発中である．まだ，いくつかの制限はある

行える．システム全体を通して常に成り立つべき条件

ものの，開発中のツールを用いる事で SysML ブロッなどの確認では，入れ子の深い状態遷移系から確認す

ク図中のあるブロックに関連するステートマシン図をることで不具合箇所の早期発見につながる．本稿で与自動的に CSP#の記述に変換することが可能となっえた変換規則はそういった，階層的な検査にも柔軟にた．自動生成された CSP#記述に，システムの要求対応できる優位性を持つ．

をアサーションとして追加することで，変換元のス
テートマシン図に PAT を用いたモデル検査が適用可

5 CSP#記述への自動変換システムの実装能である．

本節では，現在開発中のステートマシン図から本 シ ス テ ム が 完 成 す る こ と で ，1) clooca 上 で

CSP#記述への自動変換システムについて述べる．本SysML モデル図をグラフィカルに記述，2) モデル図

システムは，おもに教育の現場にて利用されているから自動的に CSP#記述を生成，3) モデル図へのモ

ウェブベースのモデル駆動開発 (MDD) ツール clooca

デル検査の適用，までの一連の作業を Web 上で実行

[9] 上にアドオンとして実装中である．clooca はシスできる環境が構築される．本稿で提案した変換規則

テムのモデル記述に利用できるだけでなく，Meta-

を clooca 上に実現することで，より質の高いモデル

Object Facility (MOF) [19] をベースとしたメタモデ

駆動開発およびモデル検査技術の教育が期待できる．

ルの開発にも利用可能なツールである．一度 clooca
上でメタモデルを開発しておくことで，ウェブブラウ

6 結論と今後の展望

ザのみでそのメタモデル上のモデルをグラフィカル

本稿では，SysML のステートマシン図を CSP#のに記述することが可能となる．図 4 は実際にウェブ

プロセスに変換する変換規則を与えることで，ステー

ブラウザ上で実行されている clooca のメタモデルエ

トマシン図の形式的な意味を与えた．この変換規則

図 4: clooca のメタモデルエディタ

図 5: clooca のモデルエディタ

により，ステートマシン図に対するより正確なモデル

図 6: clooca のスクリプトエディタ[ 4 ] Clarke, E. M. and Heinle, W.: Modular Translation of Statecharts to SMV, Technical report, 2000.
検査が可能となった．本稿では，先行研究 [23] にて与[ 5 ] Dubrovin, J., Junttila, T., Högskolan, T.,
えられた既存の変換規則について，妥当性を欠いた
Dubrovin, J., Junttila, T., Dubrovin, C. J., andJunttila, T.: SYMBOLIC MODEL CHECKING
部分に対して修正を施した変換規則を与えた．さら
OF HIERARCHICAL UML STATE MACHINES,に，ステートマシン図の構成要素として先行研究でTechnical report, Helsinki University of Technology
Laboratory, 2007.
は扱われていなかった連結擬似状態，選択擬似状態の[ 6 ] Edmund M. Clarke, J., Grumberg, O., and2 つの擬似状態に対する変換規則を新たに提案した．
Peled, D. A.: Model Checking, The MIT Press,
1999.
また，ケーススタディによりステートマシン図の実際[ 7 ] Groote, J. F., Mathijssen, A., Reniers, M.,の変換例とモデル検査器 PAT を用いたモデル検査例
Usenko, Y., and Weerdenburg, M. V.: The Formal
Specification Language mCRL2, In Proceedings ofを示し有用性の確認を行った．
the Dagstuhl Seminar, MIT Press, 2007.
今後の展望としては，より複雑な振る舞いに対応す[ 8 ] Hansen, H. H., Ketema, J., Luttik, B., Mousavi,
M. R., and van de Pol, J. C.: Towards Model Checkるため，複数の状態機械図をまたぐメッセージ通信のing Executable UML Specifications In MCRL2, Inある振る舞いへの対応や，ブロック図やシーケンス図
novations in Systems and Software Engineering,Vol. 6(2010), pp. 83 – 90.
などと連携し CSP#への変換やモデル検査に有用な[ 9 ] Hiya, S., Hisazumi, K., Fukuda, A., and Nakan情報を取り出す方法について開発することがあげら
ishi, T.: clooca : Web based tool for Domain Specific Modeling, Demos / Posters / StudentResearch
れる．
@MoDELS, 2013, pp. 31–35.
[10] Hoare, C. A. R.: Communicating Sequential
Processes, Commun. ACM, Vol. 21, No. 8(1978),参 考 文 献pp. 666–677.
[ 1 ] Bayer, M.: Mako 1.0.0, http://www.makotemplates. [11] Holzmann, G.: The Model Checker Spin, IEEE
org, 2014.
Trans, Vol. 23, No. 5(1997), pp. 279–295.
[ 2 ] Bhaduri, P. and Ramesh, S.: Model Checking[12] Latella, D., Majzik, I., and Massink, M.: Auof Statechart Models: Survey and Research Directomatic Verification of a Behavioural Subset oftions, CoRR, Vol. cs.SE/0407038(2004).
UML Statechart Diagrams Using the SPIN Model[ 3 ] Cimatti, A., Clarke, E., Giunchiglia, F.,checker, Formal Asp. Comput., Vol. 11, No. 6(1999),
and Roveri, M.:
NuSMV: a new Symbolic
pp. 637–664.
Model Verifier, Proceedings Eleventh Conference on[13] Lilius, J. and Paltor, I. P.: vUML: a Tool for
Computer-Aided Veriﬁcation (CAV’99), N. HalbVerifying UML Models, 1999, pp. 255–258.
wachs and D. Peled(eds.), Lecture Notes in Com[14] McMillan, K. L.: Symbolic Model Checking: An
puter Science, No. 1633, Trento, Italy, Springer,
approach to the state explosion problem, PhD TheJuly 1999, pp. 495–499.
sis, Pittsburgh, PA, USA, 1992.

[15] Ng, M. Y. and Butler, M.: Towards Formalizing UML State Diagrams in CSP, 1st International
Conference on Software Engineering and Formal
Methods, IEEE Computer Society, 2003, pp. 138–
147.
[16] Niewiadomski, A., Penczek, W., and Szreter, M.:
A New Approach to Model Checking of UML State
Machines, Fundam. Inf., Vol. 93, No. 1-3(2009),
pp. 289–303.
[17] OMG: OMG Unified Modeling Language Superstructure Version 2.4.1, http://www.omg.org/spec/
UML/2.4.1/Superstructure/PDF, August 2011.
[18] OMG: OMG Systems Modeling Language Version 1.3, http://www.omg.org/spec/SysML/1.3/
PDF, June 2012.
[19] OMG: OMG Meta Object Facility (MOF)
Core Version 2.4.1, http://www.omg.org/spec/MOF/
2.4.1/PDF, June 2013.

[20] Rasch, H. and Wehrheim, H.: Checking Consistency in UML Diagrams: Classes and State Machines, Formal Methods for Open Object-Based Distributed Sysems, Vol. 2884, 2003, pp. 229–243.
[21] Sun, J., Liu, Y., and Dong, J. S.: Model Checking CSP Revisited: Introducing a Process Analysis Toolkit, Proceedings of the Third International
Symposium on Leveraging Applications of Formal Methods, Veriﬁcation and Validation (ISoLA
2008), Communications in Computer and Information Science, Vol. 17, Springer, 2008, pp. 307–322.
[22] The Formal Systems website: FDR2.91, http://www.fsel.com/, November 2010.
[23] Zhang, S. J. and Liu, Y.: An Automatic Approach to Model Checking UML State Machines,
Secure Software Integration and Reliability Improvement Companion, IEEE International Conference on, (2010), pp. 1–6.