電気ショック付きシャッターの論理構造をSPINで検査してみた

# 環境
 Ubuntu20.04
Spin 6.5.1

# 背景
さて、店舗セキュリティ事業会社のシステム設計担当である貴方は以下のような、遠隔キーからの指令でシャッターの制御、表口と裏口の施錠を行えるようなシステムの設計を任されました。なおシャッターには高電圧が掛けられ、触れると電気ショックが流される機能があり、むだのない通電や安全性についても考慮する必要があります。例えば、シャッターが上がっている間は通電しないなど。

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/485117/0c3ee25d-8a98-e3b0-9b92-a5b73c5be168.png)

必要なハードウェア要素を以下とし、
要素技術的に以下の割り振りでA,B,Cの各社にお願いしたほうが良いと判断しました。つぎにシステム全体として要求を満たすために各社に対し、要求を分解して伝える必要があります。A社にはキー操作関連、B社にはドア関連と言った具合に。この分解後の論理構造に誤りがあった場合、各社が完璧に仕事をしたにもかかわらず、全体としての要求を満たすことが出来ない結果となります。例えば、シャッター通電中にドア解錠が可能であったため中に居た子供がドアを開けてシャッターに触り感電してしまうなど。

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/485117/4f7d3596-fcf1-6379-aded-645ec52fab2e.png)

そのためこの要求分解はシステムを動かす上で非常に重要な作業となるのですが、その責任の重大さにも関わらずこの正しさを保証するには、人間が脳みそを使って論理的試行を巡らせるしか方法は無いように思えます。プログラミングという作業だったらその場でフィードバックがありますが、この作業の場合はフィードバックとなるものが思考実験か各社が作業完了したあとにのみ得られます。**いえ、そう思えます**。

# SPINによる論理の保証
人間の思考実験においては、”シャッターが閉じているときに通電要求があった場合、シャッターに通電させる”と言った、IF-THEN論理構造の集合を用いてシステムの挙動をシミュレーションしていると考えられます。言うは易いですが、最終的にはすべての状態に対し、思考(試行)を終わらせる必要が在るので、考慮漏れの不安が付き纏います。これを計算機にやらせようという試みがモデル検査という分野であり、その一つのツールが今回紹介する[SPIN](https://spinroot.com/)です。SPINはPromelaという記述言語を使用してユーザが対象システムの論理モデルを記述し、それを処理して網羅的にその挙動の検査を行います。背景に上げた例を用いて、その利用法を示してみます。
細かなSPIN仕様の説明は省略します。適宜別記事を参照してください。
私は以下の教科書で学習しました。
https://www.amazon.co.jp/gp/product/B01MD13BNP/ref=kinw_myk_ro_title

# 要求分解
各社への要求分解時点に話を戻します。あなたは以下のように要求を分解しました。
なお、変数空間はKey,Door,ShutterController間で共有していると仮定します。例えばドアの開閉状態はShutterControllerからでも見れます。背景で貼った図を別タブを開いて隣り合わせで確認してみてください。

```
A社： Key & Key Controller
以下の要求を出せる
REQ_A_01 : 表口ドア 施錠/解錠
REQ_A_02 : 裏口ドア 施錠/解錠
REQ_A_03 : シャッター　上げ/下げ
REQ_A_04 : シャッター通電(電気ショック)　ON/OFF
```
```
B社：Door Controller
※ドア閉はドアが閉じている状態のこと。
REQ_B_01 : IF 表口ドア閉 THEN　IF 表口ドアロック解錠要求　THEN　表口ドアロック解錠
REQ_B_02 : IF 表口ドア閉 THEN　IF 表口ドアロック施錠要求　THEN　表口ドアロック施錠
REQ_B_03 : IF 裏口ドア閉 THEN　IF 裏口ドアロック解錠要求　THEN　裏口ドアロック解錠
REQ_B_04 : IF 裏口ドア閉 THEN　IF 裏口ドアロック施錠要求　THEN　裏口ドアロック施錠
```

```
C社： Shutter Controller
REQ_C_01 : IF シャッター上げ要求　THEN シャッター上げ
REQ_C_02 : IF シャッター下げ要求　THEN シャッター下げ
REQ_C_03 : IF シャッター通電ON要求　AND シャッター下げ状態 AND 裏口表口すべてドア閉かつロック施錠
　　　　　　　　　　THEN シャッター通電ON
REQ_C_04 : IF シャッター通電OFF要求　THEN シャッター通電OFF
```

さて、上記の分解後の各社への要求には安全面、エネルギ消費面で穴があります。どこかわかりますか？

# SPINで検査
上記の各社への要求をSPINで処理するためにPromela言語で記述してゆきます。最終的なコードは以下にあげています。
[github](https://github.com/yosukeueda33/SPIN_shutter/blob/f475e7ec790d7f3a8aab8cbd9b07a11c58986d6c/shutter.pml)
A社のKey&KeyControllerへの要求ですが、これは要求を素通しして変数格納するだけですので省略し、遠隔キー操作ユーザの振る舞いモデルとして表現します。この振る舞いモデルは可能な操作を羅列しておくことで、SPINではシステム全体が網羅的に状態遷移するように逐次選択して実行検査します。

<details><summary>振る舞いモデルUserコード</summary>
<div>

```
active proctype User()
{
    printf("User started.\n")
    do
    ::  printf("select door action\n");
        // 解錠されたドアのみ開閉できる振る舞い
        if
        :: door_lock_front_state == DOOR_UNLOCKED ->
            if
            :: door_front_state = DOOR_OPENED;
                printf("door front opened\n");
            :: door_front_state = DOOR_CLOSED;
                printf("door front closed\n");
            :: else
            fi;
        :: door_lock_back_state == DOOR_UNLOCKED ->
            if
            :: door_back_state = DOOR_OPENED;
                printf("door back opened\n");
            :: door_back_state = DOOR_CLOSED;
                printf("door back closed\n");
            :: else
            fi;
        :: else
        fi;
        printf("select action\n");
        if 
        :: door_lock_front_req = DOOR_LOCK_REQ;   // REQ_A_01
        :: door_lock_front_req = DOOR_UNLOCK_REQ; 
        :: door_lock_back_req = DOOR_LOCK_REQ;    // REQ_A_02
        :: door_lock_back_req = DOOR_UNLOCK_REQ; 
        :: shutter_req = SHUTTER_UP_REQ;          // REQ_A_03
        :: shutter_req = SHUTTER_DOWN_REQ;
        :: es_req = ES_ON_REQ;                    // REQ_A_04
        :: es_req = ES_OFF_REQ; 
        :: else 
        fi;
        printf("down reqs\n");
        door_lock_front_req = NO_REQ;
        door_lock_back_req = NO_REQ;
        shutter_req = NO_REQ;
        es_req = NO_REQ;
    od;
}
```
</div>
</details>

B社のDoorControllerのコードは以下です。
<details><summary>DoorControllerコード</summary>
<div>

```
active proctype DoorController()
{
    do
    ::  if 
        :: atomic{
                // REQ_B_01, REQ_B_02
                door_front_state == DOOR_CLOSED->
                if
                :: atomic{
                        door_lock_front_req == DOOR_LOCK_REQ ->
                        door_lock_front_state = DOOR_LOCKED;
                        printf("front door locked\n");
                    }
                :: atomic{
                        (door_lock_front_req == DOOR_UNLOCK_REQ) ->
                            door_lock_front_state = DOOR_UNLOCKED;
                            printf("front door unlocked\n");
                    }
                :: else
                fi;
            }
        :: else
        fi;
        if 
        :: atomic{
                // REQ_B_03, REQ_B_04
                door_back_state == DOOR_CLOSED->
                if
                :: atomic{
                        door_lock_back_req == DOOR_LOCK_REQ ->
                        door_lock_back_state = DOOR_LOCKED;
                        printf("back door locked\n");
                    }
                :: atomic{
                        (door_lock_back_req == DOOR_UNLOCK_REQ) ->
                            door_lock_back_state = DOOR_UNLOCKED;
                            printf("back door unlocked\n");
                    }
                :: else
                fi;
            }
        :: else
        fi;
    od
}

```
</div>
</details>

C社のShutterControllerのコードは以下です。
<details><summary>ShutterControllerコード</summary>
<div>

```
active proctype ShutterController()
{
    do
    :: atomic{
            shutter_req == SHUTTER_UP_REQ ->
            shutter_state = SHUTTER_UPPED;
            printf("shutter upped\n");
        }
    :: atomic{
            shutter_req == SHUTTER_DOWN_REQ ->
            shutter_state = SHUTTER_DOWNED;
            printf("shutter downed\n");
        }
    :: atomic{
            (es_req == ES_ON_REQ) && (shutter_state == SHUTTER_DOWNED) &&
            (door_front_state == DOOR_CLOSED) && (door_lock_front_state == DOOR_LOCKED) &&
            (door_back_state == DOOR_CLOSED) && (door_lock_back_state == DOOR_LOCKED) ->
                es_state = ES_ON;
                printf("electronic shock ON!!!!!!!!!!!!!!\n");
        }
    :: atomic{
            es_req == ES_OFF_REQ ->
            es_state = ES_OFF;
            printf("electronic shock OFF\n");
        }
    :: else;
    od;
}

```
</div>
</details>

また、安全と省エネルギーに関する以下の条件も[LTL](https://ja.wikipedia.org/wiki/%E7%B7%9A%E5%BD%A2%E6%99%82%E7%9B%B8%E8%AB%96%E7%90%86)で記述します。
w1は、”いずれのドアが解錠され、且つシャッターに通電されている状態は、常にあってはならない”
w2は、”シャッターが上がっていて、且つシャッターに通電されている状態は、常にあってはならない”
という意味です。

```
#define C_ES_ON (es_state == ES_ON)
#define C_ANY_UNLOCKED ((door_lock_front_state == DOOR_UNLOCKED) ||\
    (door_lock_back_state == DOOR_UNLOCKED))
#define C_SHUTTER_UPPED (shutter_state == SHUTTER_UPPED)

// For inner person safety.
ltl w1{always !((C_ES_ON) && (C_ANY_UNLOCKED))}

// For energy saving. 
ltl w2{always !((C_ES_ON) && (C_SHUTTER_UPPED))}
```

まとめたコードは[github](https://github.com/yosukeueda33/SPIN_shutter/blob/f475e7ec790d7f3a8aab8cbd9b07a11c58986d6c/shutter.pml)にshutter.pmlとしてあげています。

上記を試しに以下コマンドでシミュレーション実行します。シミュレーション実行はシステム全体の振る舞いをランダムに決定して遷移させていくモードです。

```
spin -u1000 shutter.pml
```
以下のような出力となります。シャッターを何度も下げたり、ドアを解錠したりをしています。(2回おなじ操作が来た場合はエラーとしていないので大丈夫です。)ここでは軽く動いているか確認する程度で見てください。また、文法に間違いが在る場合はこの時点でわかります。

```
...
        shutter downed
              shutter downed
              shutter downed
              shutter downed
      select door action
      door front opened
      select action
      down reqs
              shutter downed
      select door action
      door back closed
      select action
      down reqs
          back door unlocked
          es_state:          ES_OFF   
...
```

次に、網羅的に全体の振る舞いを見てみます。
LTL記述したw1について検証します。

```
spin -a shutter.pml
gcc pan.c
./a.out -m100000 -N w1
spin -t -c shutter.pml
```

以下の出力が得られました。
シャッター通電状態で表口ドアロックが解錠される状態が検出されたためにエラーとなっています。

```
              electronic shock ON!!!!!!!!!!!!!!
              door_lock_front_state:              DOOR_LOCKED              
              door_lock_back_state:              DOOR_LOCKED              
      select door action
      select action
      down reqs
          front door unlocked
          es_state:          ES_ON          
spin: _spin_nvr.tmp:3, Error: assertion violated
spin: text of failed assertion: assert(!(!(!(((es_state==ES_ON)&&((door_lock_front_state==DOOR_UNLOCKED)||(door_lock_back_state==DOOR_UNLOCKED)))))))
```




次に、LTL記述したw2について検証します。

```
./a.out -m100000 -N w2
spin -t -c shutter.pml
```
以下の結果となりました。
シャッター通電状態でシャッターが上がった状態が検出されたためにエラーとなっています。

```
...
      down reqs
              electronic shock ON!!!!!!!!!!!!!!
...
         shutter upped
spin: _spin_nvr.tmp:12, Error: assertion violated
spin: text of failed assertion: assert(!(!(!(((es_state==ES_ON)&&(shutter_state==SHUTTER_UPPED))))))
```

# 各社への要求の修正
SPINの出力結果から、w1,w2を満たしていないことがわかりました。
これに基づき要求を修正しましょう。

<details><summary>修正前：</summary>
<div>

```
B社：Door Controller
※ドア閉はドアが閉じている状態のこと。
REQ_B_01 : IF 表口ドア閉 THEN　IF 表口ドアロック解錠要求　THEN　表口ドアロック解錠
REQ_B_02 : IF 表口ドア閉 THEN　IF 表口ドアロック施錠要求　THEN　表口ドアロック施錠
REQ_B_03 : IF 裏口ドア閉 THEN　IF 裏口ドアロック解錠要求　THEN　裏口ドアロック解錠
REQ_B_04 : IF 裏口ドア閉 THEN　IF 裏口ドアロック施錠要求　THEN　裏口ドアロック施錠
```

```
C社： Shutter Controller
REQ_C_01 : IF シャッター上げ要求　THEN シャッター上げ
REQ_C_02 : IF シャッター下げ要求　THEN シャッター下げ
REQ_C_03 : IF シャッター通電ON要求　AND シャッター下げ状態 AND 裏口表口すべてドア閉かつロック施錠
　　　　　　　　　　THEN シャッター通電ON
REQ_C_04 : IF シャッター通電OFF要求　THEN シャッター通電OFF
```
</div>
</details>

修正後：

```
B社：Door Controller
※ドア閉はドアが閉じている状態のこと。
REQ_B_01 : IF 表口ドア閉 THEN　
             IF 表口ドアロック解錠要求　AND　シャッター通電OFF     // Added!
                THEN　表口ドアロック解錠
REQ_B_02 : IF 表口ドア閉 THEN　IF 表口ドアロック施錠要求　THEN　表口ドアロック施錠
REQ_B_03 : IF 裏口ドア閉 THEN
　　　　　　　　IF 裏口ドアロック解錠要求　AND　シャッター通電OFF     // Added!
　　　　　　　　　　THEN　裏口ドアロック解錠
REQ_B_04 : IF 裏口ドア閉 THEN　IF 裏口ドアロック施錠要求　THEN　裏口ドアロック施錠
```

```
C社： Shutter Controller
REQ_C_01 : IF シャッター上げ要求
               THEN シャッター上げ, シャッター通電OFF    // Added!
REQ_C_02 : IF シャッター下げ要求　THEN シャッター下げ
REQ_C_03 : IF シャッター通電ON要求　AND シャッター下げ状態 AND 裏口表口すべてドア閉かつロック施錠
　　　　　　　　　　THEN シャッター通電ON
REQ_C_04 : IF シャッター通電OFF要求　THEN シャッター通電OFF
```

Promelaにも変更を適用しましょう。変更はこの[github変更履歴](https://github.com/yosukeueda33/SPIN_shutter/commit/3e93cc70fcf10fb45e0761bdc57a3b8b284484e3)をご覧ください。

これで、w1,w2のエラーは消えたはずです。以下で確認してみましょう。

```
spin -a shutter.pml
gcc pan.c
./a.out -m100000 -N w1
```

```
./a.out -m100000 -N w2
```

w1, w2の実行ともに、以下のようにerrors:0と表示されます。
すなわち、修正により求めていた安全性、無駄な電力消費が解決出来たということです。

```
...
State-vector 52 byte, depth reached 787, errors: 0
...
```

これで、論理の保証付きで各社に分解後の要求を出せます。

# 注意点
今回はかなりモデルを省略して書いています。例えば、シャッターを上げる要求を受けたら直ぐにシャッターが上がった状態に成るようにモデルを記述しているため中間状態がありません。実務では中間状態にこそ論理の抜け漏れが多く潜んでいると考えられるため、"上がりきった状態" "下がる途中"など細かくモデルを組むべきと思います。また、通常のプログラミング言語同様、intなどの連続値も使えるので、0%~100%の昇降位置で表現しても容易かも知れません。

# 感想
通常のプログラミング言語と書き方は似ていますが、背景に在る考え方が異なるので少々苦労しました。また、解説サイトが少ないので、トラブルシュートも大変です。Google検索句を活用し"[word] site:spinroot.com"と検索すると良いです。

大規模な論理構造、構成要素数であり、初期の構築後に機能が追加されるようなシステムであれば、このツールの効果は絶大なものと成ると思いました。これまで思考実験を繰り返しながら論理を修正していったシステムに対し、機能を追加したいとなった場合、その思考をトレースする労力が必要ですし、設計担当者が変わった場合、はしばらく前担当者にレクチャーを受ける必要があります。そのような属人化を回避できるのは大きな利点です。
しかし言語として難解であるために、誤った論理表現をしてしまう可能性があります。実務に際してはケーススタディを繰り返して慎重に利用すべきと思います。

# 今後
組み込みの用途においては　"ボタンON後10sec後に動作開始"　などの時相表現がよく利用されますので、そのPromela上での表現方法を調査します。

# 参考文献
[spinroot.com](https://spinroot.com/spin/whatispin.html)
[教科書：SPINモデル検査](https://www.amazon.co.jp/gp/product/B01MD13BNP/ref=kinw_myk_ro_title)