形式手法とモデリング - AlloyAnalyzerを中心に

2010年9月22日(水)
小林 健一

2.3. モデリング・セッション1: 最小限の仕様を作る

今回、実際にモデリングする対象は、以下に示す、簡単なロール・ベース・アクセス制御(Role-Based Access Control: RBAC)の仕様です。

  • 集合
    • ユーザー(User): ユーザー・アカウント
    • ロール(Role): ユーザーに割り当てられる役割。Administrator、Guestなど
    • 権限(Permission): 役割に割り当てられる権限。Read、Write、Read Writeなど
  • ユーザーは、0以上のロールを持つ
  • ロールは、0以上の権限を持つ

図3: RBACのクラス図(クリックで拡大)

Alloy Analyzerでは、最初から一気に仕様を書き上げることは、あまり行ないません。まずは最小限の仕様を作成したうえで、検証を繰り返しながら仕様を追加していきます。

2.3.1. 集合の記述

最初はまず、最低限の仕様を作りましょう。

これだけです。

いくつかAlloy Analyzerのキー・ワードが出てきました。

  • sig: Signatureの略です。集合を表します。sig User {}と記述すると、Userという名前の集合を記述したことになります。{}の中には、ほかの集合との関係を記述します。
  • run: 述語(pred)を実行するコマンドです。{}の中に、例を出力する条件を記述します。

ここで実行(Executeボタン。Ctrl+Eでも可)すると、検証が実行されます(図4)。右側の結果から「Instance」のリンクをクリックすることで、インスタンスを確認できます(図5)。もしアトムが1つも表示されない場合は、次のインスタンスを表示しましょう。「Next」ボタンによって次のインスタンスを表示することができます。

図4: 実行(クリックで拡大)

ここで、Alloy Analyzerの強力な機能である「Evaluator」を試してみましょう。「Evaluator」ボタンを押すことで、Evaluatorを開くことができます(図6)。

Evaluatorでは、任意のAlloy式を記述できます。これにより、インスタンスの内容を詳細に確認できます。

試しに、Userと記述すると、Userのアトムが出力されます。User+Roleと記述すると、UserとRoleの和集合が表示されます。

主な集合演算は、以下の通りです。

  • A + B: 和集合
  • A & B: 積集合
  • A - B: 差集合

具体的に、入力して確認してみましょう。

図5: インスタンスの表示(クリックで拡大)

図6: Evaluator(クリックで拡大)

2.3.2. 関係の記述

先ほどの仕様には関係が記述されていません。このため、各アトム同士にはつながりがありません。以下では、関係を記述して、アトム同士のつながりを表現します。

関係は、上記の仕様のように、シグニチャの{}の中に記述します。

代表的な記述例は、以下の通りです。

  • lone: 0または1
  • one: 1
  • set: 0以上
  • some: 1以上

関係は、集合をつなぎます。これは、以下のように、テーブルとして表現できます(以下は、Alloy Analyzerの仕様ではありません。説明用の記述です)。

先ほどの仕様を実行して、インスタンスを表示してみましょう(図7)。

関係に対し、関係演算を行うことができます。ここでは、いくつかの関係演算を紹介します。

図7: 関係の表示(クリックで拡大)
  • → : アロー。集合同士に対して使い、新しい関係を作り出す
  • . : ドット・ジョイン。2つの集合をジョインする

ドット・ジョインの動作には、注意が必要です。ドット・ジョインは、ジョインの左右で、対応する要素同士を消去するかたちで結び付けます。

上記の場合、roles.permsとすると、rolesの右側の要素Riと、permsの左側の要素Riのそれぞれ対応する要素が消去され、以下の集合ができることになります。

この動作さえ理解してしまえば、Alloy Analyzerの関係演算は、マスターしたも同然です。

2.3.3. 関数の定義

集合同士の関係が記述できたので、関係をたどって「あるユーザーの持つ権限の集合を取得する」関数を記述しましょう。

関数は、以下のように記述します。

  • fun: 関数。「関数名 [引数]:集合 {本体}」の形式で記述する

上記の例では、あるUserのアトムuを引数として受け取り、uが持つロールにヒモ付いた権限の集合を返すことになります。

この関数も、Evaluatorで直接試すことができます。UserのアトムUser$0がインスタンスに存在するとしたとき、以下のようにEvaluatorで実行すると、結果として、権限の集合が得られます。

完成した仕様を、以下に示します。

分からないところは、どんどんEvaluatorに入力して試すことができます。簡単に実行できることが分かると思います。

株式会社豆蔵

連載バックナンバー

Think ITメルマガ会員登録受付中

Think ITでは、技術情報が詰まったメールマガジン「Think IT Weekly」の配信サービスを提供しています。メルマガ会員登録を済ませれば、メルマガだけでなく、さまざまな限定特典を入手できるようになります。

Think ITメルマガ会員のサービス内容を見る

他にもこの記事が読まれています