時間を加味したモデリング

こんにちは、SWETの鈴木穂高（@hoddy3190）です。

現在SWETチームにて仕様の欠陥をなるべく早くみつける取り組みにチャレンジしています。 欠陥をみつけるタイミングが早ければ早いほど、開発中の手戻りに伴うコストを抑えられます。 たとえば、仕様作成フェーズ、実装フェーズ、QAフェーズの順で開発が進んでいくときに、仕様の欠陥が実装フェーズやQAフェーズでみつかると実装やQAのやり直しを引き起こしかねません。 そうした大きな手戻りを抑えるために仕様の欠陥をなるべく仕様作成フェーズでみつけることを目指します。

対象領域に出てくる要素をモデリングすることは、仕様に潜む欠陥を開発の早い段階でみつけるための、有効な手段のひとつです。 要素には、開発者がこれから作るシステムや、そのシステムのユーザー、そのシステムと直接的または間接的に相互作用する外部のシステムが含まれます。 単に図を書くというモデリングの他に、プログラムのように動くモデルを作るという方法もあります。動くモデルを作るとモデリングする過程での気づきや、モデルを動かしてみた時の気づきが後工程での手戻りを減らすことにつながります。

以前私が書いた「仕様記述テクニック『Promotion』の紹介」ではAlloyを使っていましたが、 本記事ではプログラミング言語OCamlをモデリング言語として使って時間を加味したモデルを記述する方法を紹介します。 多くのモデリング対象の振る舞いは時間が関係するため、モデルの記述で時間を扱えると表現の幅が広がります。 なお、OCamlの説明はしません。

OCamlでのモデリング

今回はプロセスをモデリングします。プロセスは対象領域の要素の振る舞いを指す用語として用います。 モデリングのやり方はさまざまあります。今回は対象のプロセスをプロセスが取りうる状態と遷移で表現します。 プロセスの型は次のようにします：

type ('ev, 'ch, 'state) process =
  'state -> (('ev, 'ch, 'state) trans) list

process型で求められる状態の型は次のようにします：

type state =
  | State_A
  | State_B of int

状態変数はコンストラクタの引数を使って表現します。

遷移ラベルには、イベント同期、受信、τを用意します。ここでτという遷移ラベルのついた遷移は、プロセス内部で自動的に遷移します。 遷移の型は次のようにします：

type ('ev, 'ch, 'state) trans =
  | Tau of 'state
  | Ev of ('ev * 'state)
  | Recv of ('ch * ('state, 'ev) guard * ('ev -> 'state))

コンストラクタTauはτを表します。 コンストラクタEvはイベント同期を表します。イベント同期は、チャネルを通じて値をやりとりします。 コンストラクタRecvは受信を表します。受信は、チャネルを通じて値を受け取ります。受信の場合、事後状態は受信した値によって決まります。ガードを満たすかどうかも受信した値によって決まります。 受信によって起きるイベントは、受信した値を使ってイベント同期で表します。

trans型で求められるイベントの型は次のようにします：

type ev =
  | Event_A
  | Ch1 of int

イベント型に呼応してチャネル型を定義します。イベントが属するコンストラクタを表すための型です。 OCamlでは引数をとるコンストラクタそのものを値として使うことができないので、このような構成にしています。 trans型で求められるチャネルの型は次のようにします：

type ch =
  | Ch_Ch1
  | Ch_Ch2

ここまでを踏まえて次の状態遷移図で表されるATMをモデリングしてみましょう。

ATMの振る舞いは、カードを受け取り（in）、PINナンバーを受け取り（pin）、PINナンバーをチェックし（check）、引き出す額を受け取り（req）、額分のお金を出し（dispense）、カードを出します（out）。

これをモデリングすると次のようになります：

let atm_process : (ev, ch, atm_state) process = fun s ->
  match s with
  | A_S1 vals ->
      [
        (* in?c *)
        Recv
          ( Ch_In,
            (fun _ _ -> true),
            fun ev ->
              let vals' = make_vals'_1 vals ev in
              A_S2 vals' );
      ]
  | A_S2 vals ->
      [
        (* pin?p *)
        Recv
          ( Ch_Pin,
            (fun _ _ -> true),
            fun ev ->
              let vals' = make_vals'_2 vals ev in
              A_S3 vals' );
      ]
  | A_S3 vals ->
      let vals' = make_vals'_3 vals in
      [ (* check *) Ev (Check, A_S4 vals') ]
  | A_S4 vals ->
      [
        (* req?n *)
        Recv
          ( Ch_Req,
            (fun _ _ -> true),
            fun ev ->
              let vals' = make_vals'_4 vals ev in
              A_S5 vals' );
      ]
  | A_S5 vals ->
      let vals' = make_vals'_5 vals in
      [ (* dispense!n *) Ev (Dispense vals.req, A_S6 vals') ]
  | A_S6 vals ->
      let vals' = make_vals'_6 vals in
      [ (* out!c *) Ev (Out (get_card vals), A_S1 vals') ]

時間遷移の追加

次に、物理的な時間経過を表現できるように表現の枠組みを拡大します。ここでは時間オートマトンという理論にある考え方を使います。 時間オートマトンにおける状態は、ロケーションと時間代入関数の組で表現します。 ロケーションは、今まで「状態」と呼んでいたものです。時間代入関数はクロック変数と時間をマッピングしたものです。クロックは経過した時間を表します。 遷移には2種類あり、あるロケーションから別のロケーションに遷移する離散遷移と、時間経過による時間遷移があります。

時間を表す型を用意します：

type datetime = int

クロック変数の型を用意します：

type clock = T

時間制約式は、時間に関する条件を表した式です。ある時刻までに遷移するといった遷移の条件や、ある時刻を越えてこの状態に留まることはできないといった状態が満たすべき条件を表すのに用いられます。時間制約式は次のようにします：

type ('clock) cons =
  | True
  | Eq of 'clock * datetime
  | Le of 'clock * datetime
  | Ge of 'clock * datetime
  | Lt of 'clock * datetime
  | Gt of 'clock * datetime
  | Not of 'clock cons
  | Or of 'clock cons * 'clock cons
  | And of 'clock cons * 'clock cons

時間代入関数は次のようにします：

type 'clock v = ('clock, datetime) Hashtbl.t

時間代入関数は時間遷移や、クロック変数のリセットを伴う離散遷移で更新されます。

不変述語は状態が満たす時間制約です。不変述語は次のようにします：

type ('state, 'clock) inv = 'state -> ('clock cons)

遷移に時間制約を与えられるようにしたいので、遷移する際に満たすべき時間制約とリセット対象のクロック変数を指定できるようプロセスの型を次のように変更します：

type ('ev, 'ch, 'state, 'clock) process =
  'state ->
  'clock v ->
  ( 'clock cons * (* 遷移する際に満たすべき時間制約式 *)
    'clock list * (* リセットするクロック変数 *)
    ('ev, 'ch, 'state, 'clock) trans ) list

遷移も合わせて変更します：

type ('ev, 'ch, 'state, 'clock) trans =
  | Tau of 'state
  | Ev of ('ev * 'state)
  | Recv of ('ch * ('state, 'clock, 'ev) guard * ('ev -> 'state))

ATMの例（モデリング）

ここまでを踏まえてさきほどのATMの振る舞いに変更を加えたものをモデリングしてみましょう。

pinの受け取りに時間が30かかる場合はカードを出す振る舞いを加えました。 これをモデリングすると次のようになります：

let atm_process (ev, ch, atm_state, clock) process = fun s v ->
  match s with
  | A_S1 vals ->
      [
        ( True,
          [ T ],
          (* in?c *)
          Recv
            ( Ch_In,
              (fun _ _ _ -> true),
              fun ev ->
                let vals' = make_vals'_1 vals ev in
                A_S2 vals' ) );
      ]
  | A_S2 vals ->
      [
        ( Lt (T, 30),
          [],
          (* pin?p *)
          Recv
            ( Ch_Pin,
              (fun _ _ _ -> true),
              fun ev ->
                let vals' = make_vals'_2 vals ev in
                A_S3 vals' ) );
        (Eq (T, 30), [], Ev (Out (get_card vals), A_S1 vals));
      ]
  | A_S3 vals ->
      let vals' = make_vals'_3 vals in
      [ (True, [], (* check *) Ev (Check, A_S4 vals')) ]
  | A_S4 vals ->
      [
        ( True,
          [],
          (* req?n *)
          Recv
            ( Ch_Req,
              (fun _ _ _ -> true),
              fun ev ->
                let vals' = make_vals'_4 vals ev in
                A_S5 vals' ) );
      ]
  | A_S5 vals ->
      let vals' = make_vals'_5 vals in
      [ (True, [], (* dispense!n *) Ev (Dispense vals.req, A_S6 vals')) ]
  | A_S6 vals ->
      let vals' = make_vals'_6 vals in
      [ (True, [], (* out!c *) Ev (Out (get_card vals), A_S1 vals')) ]

モデリングしたプロセスをエンジンを使ってREPL上で動かしてみます。 エンジンは、どのイベントが起こるとどの状態になるのかを可視化します。 ひとつ前の状態に戻ったり、遷移の履歴をダンプしたりもできます。 不変述語を満たしているかのチェックもエンジン側で行っています。

メニュー[0]を選ぶと時間遷移をします。 メニュー[1]を選ぶとたどってきた状態とイベントをダンプします。 メニュー[2]を選ぶとひとつ前の状態に戻ります（undo）。 メニュー[3]を選ぶとundoで戻った操作をやり直します（redo）。 メニュー[4]以降を選ぶと離散遷移をします。

状態遷移図を見ながら意図どおりに動いているかチェックします。 上の図では、初期状態A_S1から、メニュー[4]を選択していき、A_S2、A_S3、A_S4、A_S5、A_S6、A_S1と遷移することを確認しています。 その後、A_S1からA_S2に遷移し、メニュー[0]を選択して時間を30進めた後、A_S1に遷移することを確認しています。

並行合成

一般にシステムはユーザーや外部ソフトウェアなどと相互作用をもちます。 しかし、相互作用をもつ複数の要素から構成されるシステムを欠陥なく設計し実装することは難しいものです。 複数の要素から構成されるシステムをモデリングして開発の早い段階で先のように動かしてみることは、手戻りを減らすことに寄与することが期待されます。

システムを動かすためには、まず相互作用する複数のプロセスをそれぞれモデリングします。そしてそれらを合成します。合成は、複数の振る舞いを組み合わせてできたシステムの振る舞いを決定します。 並行合成は、合成する2つのプロセスそれぞれで発生する遷移のうち、同期させたい遷移を指定して合成します。指定された遷移以外の遷移は独立して起こります。

2つのプロセスを受け取り、並行合成したプロセスを返す関数の型を次のように決めます：

val composit:
  ?sync_set_by_ch:('ch -> bool) ->
  ?eq_ev:('ev -> 'ev -> bool) ->
  ('ev, 'ch, 'p_state, 'clock) process (* プロセスP *) ->
  ('ev, 'ch, 'q_state, 'clock) process (* プロセスQ *) ->
  ('ev -> 'ch) (* 対応チャネル取得関数 *) -> 
  ('ev, 'ch, 'p_state * 'q_state, 'clock) process

プロセスPとプロセスQは合成対象のプロセスです。合成されたプロセスがとりうる状態は、プロセスPがとりうる状態とプロセスQがとりうる状態の組になります。合成されたプロセスがとりうる状態はp_stateとq_stateのタプルで表現します。 対応チャネル取得関数は、与えられたイベントが属するチャネルを返します。 sync_set_by_chで同期イベント集合を表現します。同期イベント集合には、合成する2つのプロセスの相互作用に関係するイベントを指定します。たとえば2つのプロセス間でチャネルを通じて値を送受信する場合、値のやりとりをするイベントを指定します。チャネルを受け取ってtrueを返す場合、そのチャネルに属するイベントはすべて同期イベント集合に含まれることを意味します。 eq_evは受け取った2つのイベント同期を比較し等しいかどうかを判定する関数です。2つのイベント同期が同期イベント集合に含まれているとき同期するのかどうかを判定するのに使います。

ATMの例（並行合成）

さきほどのATMのモデルは変えずに、新たにユーザーの振る舞いをモデリングして、ATMと並行合成します。

ユーザーの振る舞いを次のように定めます：

さきほどのcomposit関数を用いてATMの振る舞いとユーザーの振る舞いを並行合成したものを動かしてみます。 同期イベント集合は次のようにします：

let sync_set_by_ch ch =
match ch with
| Ch_In -> true
| Ch_Pin -> true
| Ch_Req -> true
| Ch_Dispense -> true
| Ch_Out -> true
| _ -> false

ユーザーとATMを合成した振る舞いの状態遷移図は次のようになります：

初期状態を(U_S1, A_S1)にして動かしてみます。

まとめ

調べたい部分に限定したモデリングは実システムの実装よりもずっと小さなコストでできますから、実装が終わって調べていた振る舞いを、仕様作成の段階で調べることができます。 ここで誤りをみつけることができれば手戻り避けることができるので、開発時間を大きく短縮できます。 動くモデルを作って動かせば、仕様書を読んだだけだと気づけなかった仕様の欠陥にも気づくことが期待できます。 また設計上の選択についてさまざまな可能性を実験的に調べるといったことも可能になります。そうすることでよりよいプロダクトやサービスを開発できる可能性が高まると考えています。

参考

• 磯部祥尚、並行システムの検証と実装、近代科学社、2012
• 磯部祥尚、粂野文洋、ソフトウェア科学基礎、近代科学社、2008
• Communicating Sequential Processes
• The Theory and Practice of Concurrency
• Timed Automata Patterns