Alloy Analyzerとの連携について

AlloyおよびAlloy Analyzerについて

Alloy Analyzerは、軽量な形式手法の考え方にもとづいた、形式手法ツールです。仕様として定義した内容を満たすモデルを図として表示することができます。UMLのクラス図で定義された内容に対して適用すると、そのクラス図で定義された条件を満たすインスタンスオブジェクトの例を示してくれます。

使用方法の一例として、クラス図で定義された内容に漏れがないかどうかを確認することができます。意図していない内容のインスタンス図が発見されれば、定義された内容は不十分である(定義に漏れがある)ことがわかります。

参考情報

具体的な例

以下のような例を考えます。

このようにクラス図を作成した場合に、そのクラス図での定義内容に漏れがないか、Alloy Analyzerで確認します。実行時の一例は以下の通りです。

上記の結果では問題がなさそうですが、以下の例では問題があります。書籍を1冊も借りていない貸出記録(一番左の「貸出記録0」)が存在します。

このような問題をに対処するために、以下のようにクラス図に多重度を追加しました。

このようにして、クラス図の改善に役立てることができます。

Alloy Analyzer連携アドインについて

Alloy Analyzer連携アドイン(以下「Alloyアドイン」)を利用すると、作成したクラス図の内容からAlloyの仕様を生成後、自動的にAlloy Analyzerを起動してその仕様を読み込みます。これにより、手間をかけることなくAlloy Analyzerを利用することができます。

Alloyアドインを利用するには、以下のzipファイルをダウンロードしてください。インストール方法はこちらをご覧下さい。なお、Alloyアドインを利用するためには、バージョン9.3 ビルド935以降が必要です。

Alloy.zipのダウンロード (バージョン2.4 : 2012/10/10更新)

使い方

  1. インストール後、「アドイン・拡張」リボン内の「アドインメニュー」パネルに表示される「Alloyアドイン」→「オプション」を実行し、Alloyのjarファイルの位置を指定してください。
  2. 検証対象のクラス図を開いた状態で、「アドイン・拡張」リボン内の「アドインメニュー」パネルに表示される「Alloyアドイン」→「検証」を実行すると、クラス図の内容から仕様が生成され、自動的にAlloy Analyzerが起動されます。
  3. Alloy Analyzerのツールバーにある「Execute」ボタンを押してから「Show」ボタンを押すと、上記のようなインスタンス例が図として表示されます。

変換ルール

UMLのクラス図からAlloyの仕様に変換する際のルールは以下の通りです。このルールに該当しない項目・内容については仕様には反映されません。

  • 要素についてのルール
    • クラス要素は集合(sig)として出力します。
    • ツールボックスの「列挙」要素は、列挙値の定義になります。
      • 列挙値の個々の値は「属性」として追加します。
    • クラスに別名が定義されている場合には、仕様生成時には別名を利用します。名前はコメントとして出力されます。
    • クラスに関する制約は、クラス要素の「制約」タブに入力します。
    • クラスの属性は、集合(sig)のパラメータになります。
      • 属性のプロパティ画面の「多重度」で、oneやsetなどが設定されます。
      • 既定値(最小値1/最大値1)ではoneが設定されます。
    • 制約は、クラスのプロパティ画面にある「制約」タブに入力します。制約の名前として入力した内容はコメントとして出力され、ノートの内容が仕様として利用されます。
    • クラスの「多重度」を指定すると、その数だけインスタンスを生成します。
  • 接続についてのルール
    • 関連端名(役割名)が定義されていない場合には、「クラス名」+s を自動的に設定します。
    • 要素間の関連あるいは集約につきましては、他の要素の保持を示します。多重度によって、oneやsetなどが設定されます。多重度が未定義の場合は「0..*」(set)になります。
      • 集約・コンポジット集約・関連の場合の生成される結果をそれぞれの種類に応じた内容になります。
  • 図や全体についてのルール
    • 出力の対象は、表示されているクラス図に含まれる要素のみです。含まれていないものは出力されません。
    • 全体としての制約(不変条件)については、ステレオタイプ<<system>>を持つクラスを作成し、そのクラスの制約や操作として定義します。
      • ステレオタイプ<<system>>を持つクラスは複数作成できます。
      • <<system>>要素の「制約」はfactとして出力されます。
      • <<system>>要素の「操作」はpredあるいはfunとして出力されます。戻り値の型が他のクラス要素になっている場合はfun、それ以外はpredになります。それぞれの定義の中身は、操作のプロパティ画面の「振る舞い」タブの「振る舞い」の欄に記入してください。
  • その他
    • 最後に「run {}」を追加しています。