- これは
- 7. モデル化技法と UML
— はじめに
— 1. ソフトウェアのモデル
—– (1) モデルとは
—– (2) モデルを作成する目的
—– (3) さまざまなモデル
— 2. モデル記述
—– (1) グラフ表現
—– (2) UML
—– (3) 形式モデル
— 3. モデル分析とモデル変換
—– (1) 模擬実行
—– (2) モデル検査
—– (3) モデル洗練と正しさの証明
—– (4) モデル駆動開発とモデル変換
— 参考
これは
放送大学大学院文化科学研究科の「ソフトウェア工学」という授業で使われる「ソフトウェア工学」という教材書籍を自分なりにまとめたものです.
第 6 章「モデル化技法と UML」では…
- モデル化の目的
- 開発するシステムのイメージをつかむ
- 動作確認と特性の分析
- システム開発のベースとする
- モデル化で重要なのは, 「対象の抽象化」であり, 関心の無い側面は捨象する
- モデル化はグラフや UML, 形式モデルによって行う
- モデルは模擬実行やモデル検査を行う
等, 主にモデル化とその手法 (グラフ, UML, 形式モデル) 及びそれらの検証方法の概要について学んだ.
尚, 本まとめについては, 以下の Github リポジトリで管理しており, 加筆修正はリポジトリのみ行います.
github.com
7. モデル化技法と UML
はじめに
- ソフトウェア工学全般にわたって, モデルという概念とモデル化の技法は重要である
- 6 章ではモデルに共通する特徴とモデル化の基本的な考え方を整理し, ソフトウェアにおけるモデルの役割を明確化する
1. ソフトウェアのモデル
(1) モデルとは
- モデルの目的は大きく二つ
- 工学的なモデル (風洞実験に使って空気特性を確認するため等に作られる)
- 外から見たデザインを検討する為のモデル
- ソフトウェアのモデル
- 現在は存在しないこれから作るソフトウェアについて, 構造や動作をある観点から抽象化したもの
- このモデルに基いて目標となるソフトウェアを開発する
- 共通する特徴
- 本物ではない
- 視覚的である
(2) モデルを作成する目的
モデル作成の目的は以下の通り.
- 開発するシステムのイメージを掴み, その利便性を検討し, また問題点を発見する
- システムの動作確認, システムの持つ特性を分析する
- モデルをシステムの骨組みとみなして, それを詳細化し具体化したシステムを設計し開発する為のベースとする
モデルを作ることは, 対象の抽象化であり, 裏を返すと関心のない側面を捨象 (しゃしょう) するものである.
(3) さまざまなモデル
- モデル化はこれから作るシステムだけを対象するとは限らない
- 現存のソフトウェアを逆に抽象化してモデルとして表現し, 分析の対象とすることもある
- 環境 (問題領域) のモデル化
- システムのモデルと並行して作ることもある
- これらの相互作用も両方のモデル内に組み入れる必要がある
2. モデル記述
(1) グラフ表現
- モデルを記述する言語
- 文字と図が使われる
- 図式表現が好まれる
- グラフ表現 (頂点の集合と頂点間を結ぶ辺の集合からなる位相幾何学的なグラフを意味する)
- グラフ表現は日常的に新聞, 雑誌, テレビや報告書等で利用されている
- 問題, 事件, 事象, 制度, 業務, 仕組み (「もの」や「概念」)といった世界を捉え, それらの関係性を明示することが, 一般性の高い方法である
- 下図は冷害の原因となるオホーツク海高気圧から吹き込む「やませ」の発生要因をグラフ表現したもの
- グラフの頂点は気象現象
- 矢印は因果関係を表している
- 気象現象は頂点が楕円で囲われているのに対して, 「チベット高原」は気象現象ではないので四角で囲って区別している
- グラフ表現の注意点
- 頂点があらわすもの, 辺が表すものが, それぞれ一貫性をもつこと
- 多くの記号・図形を用いて頂点や辺を区別することは問題
- モデル化の失敗を示唆している
- フローチャート
- 制御を表す
- データの流れを表すデータフロー図
- オートマトンの状態遷移図
- 静的なモデル
- 頂点 A と B を結ぶ辺が A と B との関係を表す
- 辺が無向の場合には「A と B が関係がある」, 有向の場合には「A は B とある関係をもつ」ことを示す
- ER モデル, クラス図, 意味ネットワーク
- 動的なモデル
- 頂点 A から B への辺が A から B への何らかの異動を表す
- 辺は有効
- 制御の流れやデータの流れを表現する
(2) UML
- UML (Unified Modeling Language)
- Booch, Rumbaugh, Jacobson らによって 1995 年に提案された
- 統一手法
- 1997 年 11 月に UML 1.1
- 2005 年 7 月に UML 2.0
- 最新版は UML 2.4.1 (2012 年末現在)
- テキストよりも図式を中心とした記法を定めたもの
以下のような 3 つのカテゴリに分類された 13 種類の図表現が定義されている.
1.構成図
1.クラス図
2.複合構造図
3.オブジェクト図
4.コンポーネント図
5.配置図
6.パッケージ図
2.振舞い図
1.ユースケース図
2.状態機械図
3.活動図
3.相互作用図
1.系列図
2.通信図
3.タイミング図
4.相互作用概要図
上記の中から代表的な図の構造をグラフ表現としてみると, 以下のように整理出来る.
| 頂点 | 辺 | |
|---|---|---|
| クラス図 | クラス | 汎化, 集約, 関連 |
| 状態機械図 | 状態 | 遷移 |
| 活動図 | 動作 | 制御の流れ |
| 通信図 | オブジェクト | メッセージの流れ |
| 系列図 | メッセージ受発信の時点 | メッセージの流れ |
- UML を使うための全般的な注意点
- 全ての図を使う必要は無い
- 例えば, クラス図を書く場合に, クラス図で用いることが出来る全ての構成用を使う必要は無い
- 選択の判断は開発組織で統一し標準化すべき
- グラフ構造という共通の形式をもっている為, 各図の差異を十分に認識して使用すべき
- 全ての図を使う必要は無い
(3) 形式モデル
- UML モデルはモデルの意味が曖昧だという批判がある
- この批判に対して, UML 側はメタモデル (モデルのモデル) を定義することによって形式性を与えようとしている
- 最も厳密性の高いモデル記法の方法
- 形式手法によるもの
- 形式論理や形式言語で取られる方法
- 形式使用言語
- VDM
- Z
- RAISE
- Event-B
- Event-B
- モデルは状態と事象で記述される
- 状態: モデルが表す対象の現在の状態を表す (定数と変数の集合)
- 事象: 状態に変化をもたらす (事象がおこある条件と, 事象の事前状態及び事後状態で与えられる)
- 形式手法によるもの
以下, Event-B による「橋の信号制御」のモデル化について.
constant: d axiom0_1: d ∈ N variables: a, b, c inv1_1: a ∈ N inv1_2: b ∈ N inv1_3: c ∈ N inv1_4: a + b + c ≦ d inv1_5: a = 0 V b = 0
「橋の信号制御」問題の状態空間は以下の定数と変数で定められる.
- d は定数
- 橋と島にある車の台数上限
- a, b, c は変数
- a は橋の上にあって本土から島に向かう車の台数
- b は島の上にある車の台数
- c は橋の上にあって島から本土に向かう車の台数
- inv は不変条件
- この状態空間で常に成り立つべき性質を表す
- N は自然数の集合
- inv1_5 で橋が一方通行であることが形式的に定められている
1 台の車が本土を出て橋に入る事象 ML_out は, Event-B では次のように定義出来る.
ML_out
when
a + b < d
c = 0
then
a: = a + 1
end
他の事象も同様に定義出来る.
3. モデル分析とモデル変換
- モデルを作る大きな目的
- モデル上で種々の分析を行い, これから開発するシステムのもつべき性質を確かめ, 信頼性を向上させること
(1) 模擬実行
- 操作的な意味が与えられているモデルでは, それを模擬的に実行して, 実際のシステムの挙動に関する知見を得ることが出来る
- 動画機能
- 状態遷移モデルを扱うツールに備わっている, ユーザーが事象を指定することにより, 模擬的な実行を可能とする機能
(2) モデル検査
- モデルが与えられた性質をみたすかどうかを自動的に検証する方法
- 状態遷移モデルを仮定し, 性質は時相理論 (temporal logic) で表すことが一般的
- 時相理論 (temporal logic)
- 「いつも成立する」ことを意味する時相演算子と「いつかは成立する」ことを意味する時相演算子を含む理論
- 時相理論を用いると以下のような性質を記述することが出来る
- 安全性
- 望ましくない状況がどんな遷移経路をたどっても決しておこらないという性質
- 活性
- 望ましい状況がいつか必ず実現するという性質
- 安全性
- 自動的に実行するアルゴリズムは工夫されており, アルゴリズムを具体化したツールが公開されている
- SPIN
- NuSMV
- Uppaal
- モデル検査の特徴
- モデルと性質を与えれば, 検査は自動的に行われる
- 検査に失敗した時 (モデルが所定の性質を満たさないと判定された場合), その反例が提示される
(3) モデル洗練と正しさの証明
- モデル検査対象となる性質をどう与えるかには任意性があり, ユーザーのセンスに任される…
- 性質は対象となるシステムの仕様から導かれるので, おのずと適切なものが定まる…
- モデルが開発すべきシステムを完全に表現したものであるかどうかについては疑問の余地が残る
- 形式モデルの手法であれば, 仕様とモデルの整合性を満たすことは数学的な手法で証明されているので, より高い信頼性が得られる
定理証明系の問題点- モデル検査系と異なり, 全自動というわけには必ずしもいかない
- 証明プロセスに人が介在して, 対話的に証明を進行させなければならないケースがある
(4) モデル駆動開発とモデル変換
- モデル駆動アーキテクチャ MDA (Model Driven Architecture)
- UML を用いて基盤非依存モデル PIM (Platform Independent Model) を作成
- PIM を PSM (Platform Specific Model) に変換する
- PSM は最終的に Java 等のプログラムに変換される
- メタモデル階層
- MDA で強調される概念の 1 つ
- モデルの集合に対してそれを規定するより抽象化されたモデルのモデルを提供
- モデル層に対して 1 レベル上位層を形成する
- MDE (Model Driven Enginnering)
- MDA は OMG が商標を登録しているので, 学会的に別の名前を付ける必要があった
- 領域特化言語 (DSL: Domain Specific Language) という概念
- ある特定領域のモデルやメタモデルを記述言語
- モデル変換の考え方を PIM → PSM に限定せず, 多用なモデル記述言語間の変換に拡張する
- モデルからメタモデル, メタモデルからメタメタモデルへの変換
- 1 つの領域から別の領域への変換
- データベースの SQL やコンパイラ生成の Yacc
- モデル変換の対象は DSL だけではない
- 汎用言語によるモデルも含まれる
- MDA の MOF/UML
- EMF の ECORE/UML/Java
- EBNF/Java
- XML という 1 つのモデル記述層から, 別のモデル群への変換やその逆の変換も考えられる
- ATL はモデル変換を記述する言語として様々な使用例を持つ
参考
- 位相幾何学的
- やませ
- UML入門 – IT専科
- Event-B – 形式手法 Event-B
- 時相論理 – Wikipedia
- ATL Use Case – DSLs coordination for Telephony | The Eclipse Foundation
- Flowchart Maker & Online Diagram Software
