ソフトウェアモデル作成支援ツール
実現のための状態遷移分析手法
アーク・システム・ソリューションズ株式会社
発表者：福井 雅彦
共著者：島津 仁晶
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
1
概要
要求仕様とソフトウェアの齟齬を無くしたい
形式手法（Bメソッド）の利用
適切なモデル化が困難
提案
モデル作成の自動化
ツール化可能な状態遷移分析手法考案
作成しやすいモデルの導入
要求
仕様
ツールによる
入力支援
仕様
モデル
自動で導出
仕様を素直に反映できるモデル
実装
モデル
実装可能な状態遷移モデル
※今回はツールではなく手法を中心に解説
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
2
背景
高信頼なシステムを構築するために、形式手法の一つであるB
メソッドを制御系分野で活用する方法を模索してきた。
Bメソッドは開発の下流までカバー
ソースコード
Bメソッドの形式モデル
適合性を証明
仕様
自動生成
実装
他の手法で扱うのは概ね仕様のみ
欧州では鉄道インフラ構築への実績あり
にもかかわらず、日本では普及が進んでいない。
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
3
課題(1/2)
制御系分野ではBメソッドの活用が困難
理由
データ構造よりも振る舞いのモデル化が重要だが、
要求仕様 → 状態遷移の
導出手法が属人的で未確立
国内で入手可能なBメソッドの
技術情報に偏り
データ構造のモデル化が主
実践的なサンプルが少ない
13th WOCS2
1/20/2016
＋
ステートやイベントを
明確な根拠に基づいて
導出できない
要求との対応が
一意ではない
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
4
課題(2/2)
状態遷移モデルを「えいや！」で作ると．．．
状態遷移モデル
S2
S1
・仕様との適合を保証できない。
・仕様の追跡が困難。
形式モデル
(B, Z, VDM)
実装
信用できない形式モデルは
信用できないソフトウェア
しか生まない
解決できれば形式手法を活用できる
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
5
提案
ツール化可能な
経験や勘に依存しない
制御分野向け状態遷移分析手法
状態遷移モデル
作成しやすい
モデルの導入
S1
SS22
S2
必要な要件
明確な分割ルールを持ち
適切な規模のモジュール
の集まりで表現
ステートを意識せずに書ける
状態遷移モデルを機械的に導出
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
6
本提案手法の内容
本手法の開発の流れ
実装モデル
仕様モデル
S2
S1
ステートを意識しないモデル作成
実装可能な状態遷移モデル導出
ツール化するプロセス
入力支援
イベント
定義
13th WOCS2
1/20/2016
分割ルールに該当
モジュール追加
分割
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
自動生成
仕様モデル
から導出
7
本手法で扱うモデル
仕様モデル
実装モデル
S1
S2
• ステートを意識しない
• 一般的な状態遷移モデル
• イベント定義はガード必須
• 実装に近い形式
• 要求仕様と原則一意対応
• 非決定性を持たないス
テートマシンの集まり
• 明確なモジュール分割ルール
導出
作成が容易
機械的な導出
作成に要する属人スキルの軽減
要求仕様→モデル 変換時の誤り防止
メンテナンス及び可読性の向上
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
8
仕様モデルの定義 (1/2)
仕様モデル
変数定義
名称
イベント定義
イベント
イベント
トリガ
型、
ガード
初期値
アクション
等価
イベント
イベント
イベント
．．．
ステートが1個のステートマシン
禁止条件
（発生してはいけない変数値の組み合わせ）
イベント定義 ： トリガ [ガード]／アクション
発火の引き金となる外部状態
13th WOCS2
1/20/2016
発火を許す内部状態
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
9
仕様モデルの定義 (2/2)
要求仕様は仕様モデルの項目と原則一意に対応する。
要求仕様
R1. （外部の状態が）Eになったとき操作Aを行なう。
R2. 状態がG以外のとき入力Eは無視する。
仕様モデル（イベント定義）
イベント定義
E [￢G] / A
R1. トリガとアクション
13th WOCS2
1/20/2016
R2. ガード(※否定表現なので論理が反転)
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
10
仕様モデルの分割(1/3)
仕様モデルはルールに従って適宜モジュール分割を行う。
仕様モデル
分割後の仕様モデル
ルールに
合致したら分割
ステートマシン1個分の記述=1モジュール
イベント評価の監視で連携
分割ルールの適用可能箇所がなくなったら、仕様モデル作成完了。
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
11
仕様モデルの分割(2/3)
分割ルール1：
未定義イベントを詳細化した結果、イベント評価で更新される
変数ができた場合、更新は分割先のアクションに記述。
例えば、イベント評価回数が
イベント判定に使われる場合
++評価回数 > 1024 ／アクション
新モジュールを作りaの更新を
分割先のアクションに記述
評価回数 = 1024 ／アクション
監視
T／++評価回数
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
12
仕様モデルの分割(3/3)
分割ルール2：
相互依存がない変数更新は分割する。
bはaに依存
トリガ2 ／a:=0
トリガ1 [a=0] ／b:=0
監視
新モジュールに
aの更新を分割
トリガ1 & a=0／b:=0
トリガ2 ／a:=0
aはbに非依存
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
13
実装モデルの導出(1/2)
実装モデルは機械的な手順で導出できる。
実装モデル
仕様モデル
T2[G1] / A2
T1[G1] / A1
T3[G1] / A3
導出
T 1 / A1
S2
S1
S3
①ステートSは仕様モデル
のガードGから生成
②ステートSはガードGが
合致する全てのイベントTを持つ
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
③遷移先はステートSと
アクションAで決定される
14
実装モデルの導出(2/2)
モジュール ∈ 仕様モデルの全モジュール
ステートはモジュールの全ガード条件が持つ項gnと
否定￢ gnの直積
{g0, ￢ g0} ×{g1, ￢ g1} × ．．． ×{gmax, ￢ gmax}
（ただし、nは0～max）
から、域値が空になるものと仕様モデルの禁止状態
に該当するものを除いた全ての条件の集合
ステートの生成
ステート ∈ 生成した全ステート
イベント ∈ モジュール定義内の全イベント
ステートの条件→イベントのガード条件
T
ステートにイベントを追加
遷移可能ステート ∈ 生成した全ステート
遷移可能ステートの条件→
アクション評価後のステート
T
遷移可能ステートをイベントの遷移先に追加
遷移可能ステート
イベント
ステート
モジュール
END
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
15
Bメソッドのモデルへ変換
仕様モデルと実装モデルをBのモデルに変換。
導出
変換
変換
Bの形式モデル
ソースコード
Bの定理証明器で
適合確認が可能
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
自動生成
16
提案法の実証試験・試行(1/7)
本手法の実証サンプルを作ってみた。
機能概要
・計測時間は最大3分まで指定できる
・開始ボタンを押すと計測開始
・完了時にはブザーで知らせる
・計測中カウントの一時中断／再開可能
開発規模
入出力定義 : 5件
機能要求 : 19件
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
17
提案法の実証試験・試行(2/7)
要求仕様
3.1 機能要求
1. 付録 A：タイマの要求仕様
本手法を解説するためのサンプルとして、簡単なタイマアプリの要求仕様を定義する。
3.1 概要
タイマが「できること」の概要は以下の通り。
・計測する時間は最大 3 分まで指定できる
・開始ボタンを押すと計測開始
・完了時にはブザーで知らせる
・計測中にカウントダウンの一時中断と再開が可能
R2_1
: 複数ボタンの同時押し操作は無視する
R2_2
:計測可能な最大は 3 分まで。
R2_3
:開始ボタンを押すと時間の計測を開始する。
R2_4
:但し、待ち時間（=計測開始時にセットする時間）が０ならば開始ボタンを押しても計測開始しない。
R2_5
:待ち時間から 0 になるまでカウントダウンを行う。
R2_6
:カウントダウン終了後、開始ボタンを押すと再度待ち時間からカウントダウンを始める。
R2_7
:計測中に開始ボタンを押すとカウントダウンを一時中断する。
R2_8
:カウントダウンを一時中断しているときに計測ボタンを押すと再開する。
R2_9
:非計測中に加算ボタンを押すと待ち時間に 60 秒加算
R2_10 :クリアボタンを押すと待ち時間をクリア、計測中であれば残り時間もクリアして計測終了。
図 9_1：タイマの物理イメージ
R2_11 :計測中は 1 秒毎に残り時間をカウントダウン。
R2_12 :計測中に残り時間が 0 になったらブザーを 3 秒鳴らす。
R2_13 :計測中は残り時間を表示する。
3.2 入出力
R2_14 :非計測中は待ち時間を表示する。
入出力は簡単なキッチンタイマのインタフェースを想定している。
R2_15 :計測終了のブザー鳴動中の時間表示は０。
R2_16 :計測終了のブザーが鳴り終わったら再び待ち時間を表示する。
R1_1 : 開始ボタン
入力ボタンの一つ。押す(T)/離す(F)状態の状態を参照できる。
R2_17 :計測終了のブザー鳴動中にボタン操作が行われたときは鳴動を停止し、そのボタン操作を行う。
R2_18 :計測中は残り時間の区切り”：”が点滅する。
R1_2 : 加算ボタン
入力ボタンの一つ。押す(T)/離す(F)状態の状態を参照できる。
R2_19 :動作は周期実行（1024 回/秒）とする。
R1_3 : クリアボタン
入力ボタンの一つ。押す(T)/離す(F)状態の状態を参照できる。
R1_4 : 液晶パネル
数字列と区切りの”：”の表示制御ができる簡単なもの。
表示時間は自然数（NAT）で秒数を渡す。
表示点滅は”：”の点滅を論理値で指示する。T ならば点滅。F ならば常時点灯。
表示時間の形式は”mm:ss”とする。但し、mm は先頭空白埋めの分数、ss は先頭 0 埋め２桁の秒数。表示
の形成はドライバないし基本機械で適宜行われるものとする。
R1_5 : ブザー
ブザーの鳴動。
論理値で指示する T ならば鳴動、F ならば停止。
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
18
提案法の実証試験・試行(3/7)
仕様モデルを作成する。以下は、開始時点のモジュール構成。
変数は要求仕様の
入力定義から拾う
イベントは
要求仕様の
入力で発生
する動作から
拾う
変数は要求仕様の
出力定義から拾う
イベント定義
トリガ
ガード
アクション
※左の表はツール化した
際のイベント定義。スぺ
―スが不足しているため
禁止条件と変数定義は
割愛。
要求仕様を元に作る。
この時点でモジュール間の参照は未定義。
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
19
提案法の実証試験・試行(4/7)
仕様モデルの分割とイベント定義を全て終えた状態。
要求仕様の能動的な機能要件の
項目は最上位モジュール群の
イベント定義に対して一意に対応
タイマ制御の下位モジュール
なので要求仕様書のスコープ外。
これを元に実装モデルを導出する。
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
20
提案法の実証試験・試行(5/7)
要求仕様と仕様モデルのトレサビリティ
追跡可能な要件
２２／２４
イベントと対応
２０／２４
イベントと非対応
２／２４
暗黙で仕様を満たして
いたので明示しなかった
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
21
提案法の実証試験・試行(6/7)
仕様モデルと実装モデルから作成したBの形式モデルの構成。
機械的に置き換えたモデルなので、点線で囲った部分の構成
は完全に一致する。
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
22
提案法の実証試験・試行(7/7)
以前作成したキッチンタイマの形式モデルとの比較
最も複雑さが集中するモジュールの証明責務数
前回：最大で442件発生 対して 今回：最大で96件。
前回
13th WOCS2
1/20/2016
今回
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
23
まとめ
要求仕様に近い仕様モデル
で振る舞いを記述できる
仕様モデル→実装モデル
が機械的な手順で導出できる
状態遷移モデル作成の属人
スキル依存を軽減
ソフトウェアツールによる
自動作成支援が可能
項目が一意に対応するので
仕様の追跡が容易
他の形式手法や制御以外の
分野でも応用が可能と思われる
Bメソッドの形式モデルの導出が可能
国内の開発現場でもBメソッドを制御系分野で活用できる可能性が開けた。
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
24
今後の課題
手法のソフトウェアツール化
手順自体は完成
・状態遷移モデル導出のため
の数式処理が必要
・手法の検証
他の形式手法、制御以外への適用
現状の前提
･周期実行
･ポーリング
イベント駆動、割り込み駆動モ
ジュール評価順の検証要
※ ツールは現在開発中
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
25
ご清聴ありがとうございました。
お問い合わせ先
アーク・システム・ソリューションズ株式会社
開発部 研究開発課 福井 雅彦
TEL：011-207-6460 e-mail：[email protected]
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
26
付録A:タイマの要求仕様(1/3)
付録A：タイマの要求仕様
本手法を解説するためのサンプルとして、簡単なタイマアプリの要求仕様を
定義する。
1.1 概要
タイマが「できること」の概要は以下の通り。
・計測する時間は最大3分まで指定できる
・開始ボタンを押すと計測開始
・完了時にはブザーで知らせる
・計測中にカウントダウンの一時中断と再開が可能
図1：タイマの物理イメージ
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
27
付録A:タイマの要求仕様(2/3)
1.2 入出力
入出力は簡単なキッチンタイマのインタフェースを想定。
R1_1 : 開始ボタン
入力ボタンの一つ。押す(T)/離す(F)状態の状態を参照できる。
R1_2 : 加算ボタン
入力ボタンの一つ。押す(T)/離す(F)状態の状態を参照できる。
R1_3 : クリアボタン
入力ボタンの一つ。押す(T)/離す(F)状態の状態を参照できる。
R1_4 : 液晶パネル
数字列と区切りの”：”の表示制御ができる簡単なもの。
表示時間は自然数（NAT）で秒数を渡す。
表示点滅は”：”の点滅を論理値で指示する。Tならば点滅。Fならば常時点灯。
表示時間の形式は”mm:ss”とする。但し、mmは先頭空白埋めの分数、ssは先頭
0埋め２桁の秒数。表示の形成はドライバないし基本機械で適宜行われるものと
する。
R1_5 : ブザー
ブザーの鳴動。論理値で指示するTならば鳴動、Fならば停止。
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
28
付録A:タイマの要求仕様(3/3)
1.3機能要求
R2_1 ：複数ボタンの同時押し操作は無視する
R2_2 ：計測可能な最大は3分まで。
R2_3 ：開始ボタンを押すと時間の計測を開始する。
R2_4 ：待ち時間（=計測開始時にセットする時間）が0ならば開始ボタンを押しても計測開始しない。
R2_5 ：待ち時間から0になるまでカウントダウンを行う。
R2_6 ：カウントダウン終了後、開始ボタンを押すと再度待ち時間からカウントダウンを始める。
R2_7 ：計測中に開始ボタンを押すとカウントダウンを一時中断する。
R2_8 ：カウントダウンを一時中断しているときに計測ボタンを押すと再開する。
R2_9 ：非計測中に加算ボタンを押すと待ち時間に60秒加算
R2_10：クリアボタンを押すと待ち時間をクリア、計測中であれば残り時間もクリアして計測終了。
R2_11：計測中は1秒毎に残り時間をカウントダウン。
R2_12：計測中に残り時間が0になったらブザーを3秒鳴らす。
R2_13：計測中は残り時間を表示する。
R2_14：非計測中は待ち時間を表示する。
R2_15：計測終了のブザー鳴動中の時間表示は０。
R2_16：計測終了のブザーが鳴り終わったら再び待ち時間を表示する。
R2_17：計測終了のブザー鳴動中にボタン操作が行われたときは鳴動停止し、そのボタン操作を行う。
R2_18：計測中は残り時間の区切り”：”が点滅する。
R2_19：動作は周期実行（1024回/秒）とする。
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
29
付録B:実装モデル導出(1/4)
a. ステートの洗い出し
モジュールの全ガード条件から、論理積でつながる全ての項
とその否定の全組み合わせを作成する。
例：モジュールが２つのガード条件
G1 G2を持つ場合
G1=g11 & g12
G2=g21 & g22
トリガ１ [G1]
トリガ2 [G2]
S
ならば全組み合わせは、
{g11,￢g11}×{g12,￢g12}×{g21,￢g21}×{g22,￢g22}
（※{G1,￢G1}×{G2,￢G2}でも良いかもしれない 2016011時点）
ここから、値域が空になる変数を含む要素、仕様モデルの禁
止条件に該当する要素を除いた残りが実装モデルのステート。
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
30
付録B:実装モデル導出(2/4)
b. ステートに属するイベント
仕様モデルのイベント
Ti [Gi] / Ai()
と、洗い出したステートSnに対して
Sn → Gi
が真になるとき、ステートSn はイベントEiを持つ。
このときガード条件は除く。
Sn
Ti / Ai()
Sn → Gi ならばSn はイベントTiを持つ。
13th WOCS2
1/20/2016
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
31
付録B:実装モデル導出(3/4)
d. 実装モデルのガード条件
遷移先が分岐する場合はイベントにガード条件を付ける。
ステートSmへ遷移するイベントのガードはアクションAi()と遷移
先Smから導出できる最弱事前条件
wp(Ai(), Sm)
である。
13th WOCS2
1/20/2016
Sn
Ti [wp(Ai(), Sm)] / Ai()
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
Sm
32
付録B:実装モデル導出(4/4)
d. ステートの整理
どこからも遷移しないステートは破棄。
S1
S3
S3はどこからも遷移
しないので破棄
S2
イベントと遷移先が同じステートはまとめる。
イベント2
イベント1
S3
イベント2
S1
イベント1
13th WOCS2
1/20/2016
S2 、S3はまとめる
（注：イベント2はまとめる
と同じになる）
S2
Copyright © 2016 Arc System Solutions Inc. All Rights Reserved.
33
© Copyright 2024 ExpyDoc
