1

根据我必须使用jSpin和promela语言实现的问题，我需要一些帮助。

家庭警报系统可以使用个人 ID 密钥或密码来激活和停用，激活后系统进入大约 30 秒的等待期，该时间允许用户撤离安全区域，之后警报被布防，即使是在入侵时检测到警报有一个内置的等待时间或延迟 15 秒，以允许入侵者输入密码或刷卡钥匙从而识别自己，如果在分配的 15 秒内未进行识别，警报将响起并将一直打开，直到使用身份证或密码将其停用。

这是我尝试过的：

mtype = {sigact, sigdeact};
chan signal = [0] of {mtype};
chan password = [0] of { int }; 
/*chan syntax for declaring and initializing message passing channels*/

int count;
bool alarm_off = true; /*The initial state of the alarm is off*/    
active proctype alarm()    
{
    off:
       if 
         :: count >= 30 -> atomic {signal!sigdeact; count = 0;alarm_off = false; goto on;}
         :: else -> atomic {count++; alarm_off = true; goto off;}
       fi;

    on:
        if
          :: count >=15 -> atomic { signal!sigact; count = 0;
    alarm_off = false; goto off;}
          :: else -> atomic {signal!sigact; alarm_off = true; goto pending;}
        fi;

    pending:

        if
           :: count >= 30 -> atomic {count = 0; alarm_off = false; goto on;}
           :: count < 30 -> atomic {count++; alarm_off = false; goto pending;}
        fi;
}

active proctype user()
{    
   password ! 1234 //1234 is the password I sent. 
   input:  atomic { signal?sigact ->  alarm_off = true; goto off; }   
}

在user proctype中我发送密码

password ! 1234

如何验证密码是否1234正确，如何根据验证使其适应自己的情况（on、、、off）pending？

4

1 回答 1

1

由于示例中的代码似乎没有遵循规范，至少在我理解的方式上，我从头开始编写了一个示例。

请注意，以下模型（源代码）在其结构中故意非常冗长和冗余，以便更容易识别其逻辑块并 - 希望 - 理解它。在实践中，人们会使用一些内联函数来处理输入。我也没有使用SIGACT, SIGDEACT原始模型中出现的 which，因为我无法弄清楚谁应该从原始模型（源代码）和规范中读取这些消息。

#define ALARM_OFF        1
#define ALARM_COUNTDOWN  2
#define ALARM_ARMED      4
#define ALARM_INTRUSION  8
#define ALARM_FIRED     16

#define INPUT_SET_PASSWORD   1
#define INPUT_CHECK_PASSWORD 2
#define INPUT_INTRUDER       4

mtype = { SIGACT, SIGDEACT };

init {
    chan alarm_out = [1] of { mtype };
    chan alarm_in =  [1] of { byte, short };

    run alarm(alarm_in, alarm_out);
    run user(alarm_in);
    run event(alarm_in);
}

proctype alarm(chan input, output)
{
    byte count;
    byte state   = ALARM_OFF;
    short passwd = 1234;
    short tmp    = 0;

off:
    if
        :: nempty(input) ->
            if
                :: input?INPUT_SET_PASSWORD(tmp) ->
                    passwd = tmp;
                :: input?INPUT_CHECK_PASSWORD(tmp) ->
                if
                    :: tmp == passwd ->
                        atomic {
                            state = ALARM_COUNTDOWN;
                            count = 0;
                            goto countdown;
                        }
                    :: else ->
                        skip;
                fi;
                :: input?INPUT_INTRUDER(tmp) ->
                    skip;
            fi;
        :: empty(input) -> skip;
    fi;
    goto off;

countdown:
    if
        :: count < 30 ->
            if
                :: nempty(input) ->
                    if
                        :: input?INPUT_SET_PASSWORD(tmp) ->
                            skip; // error: cannot be done now (?)
                        :: input?INPUT_CHECK_PASSWORD(tmp) ->
                            if
                                :: tmp == passwd ->
                                    atomic {
                                        state = ALARM_OFF;
                                        count = 0;
                                        goto off;
                                    }
                                :: else ->
                                    skip; // error: incorrect password (?)
                            fi;
                        :: input?INPUT_INTRUDER(tmp) ->
                            skip;
                    fi;
                :: empty(input) ->
                    skip;
            fi;
        :: else ->
            atomic {
                state = ALARM_ARMED;
                count = 0;
                goto armed;
            }
    fi;
    count++;
    goto countdown;

armed:
    if
        :: nempty(input) ->
            if
                :: input?INPUT_SET_PASSWORD(tmp) ->
                    skip; // error: cannot be done now (?)
                :: input?INPUT_CHECK_PASSWORD(tmp) ->
                    if
                        :: tmp == passwd ->
                            atomic {
                                state = ALARM_OFF;
                                count = 0;
                                goto off;
                            }
                        :: else ->
                            skip; // error: incorrect password (?)
                                  // maybe it should be handled like
                                  // INPUT_INTRUDER(tmp)
                    fi;
                :: input?INPUT_INTRUDER(tmp) ->
                    atomic {
                        state = ALARM_INTRUSION;
                        count = 0;
                        goto intruder_detected;
                    }
            fi;
        :: empty(input) ->
            skip;
    fi;
    goto armed;

intruder_detected:
    if
        :: count < 15 ->
            if
                :: nempty(input) ->
                    if
                        :: input?INPUT_SET_PASSWORD(tmp) ->
                            skip; // error: cannot be done now (?)
                        :: input?INPUT_CHECK_PASSWORD(tmp);
                            if
                                :: tmp == passwd ->
                                    atomic {
                                        state = ALARM_ARMED;
                                        count = 0;
                                        goto armed;
                                    }
                                :: else ->
                                    skip; // error: incorrect password (?)
                            fi;
                        :: input?INPUT_INTRUDER(tmp) ->
                            skip;
                    fi;
                :: empty(input) ->
                    skip;
            fi;
        :: count >= 15 ->
            atomic {
                state = ALARM_FIRED;
                count = 0;
                goto alarm_fired;
            }
    fi;
    count++;
    goto intruder_detected;

alarm_fired:
    if
        :: nempty(input) ->
            if
                :: input?INPUT_SET_PASSWORD(tmp) ->
                    skip; // error: cannot be done now (?)
                :: input?INPUT_CHECK_PASSWORD(tmp);
                    if
                        :: tmp == passwd ->
                            atomic {
                                state = ALARM_OFF;
                                count = 0;
                                goto off;
                            }
                        :: else ->
                            skip; // error: incorrect password (?)
                                  // warn user but keep alarm on
                    fi;
                :: input?INPUT_INTRUDER(tmp) ->
                    skip;
            fi;
        :: empty(input) ->
            skip;
    fi;
    goto alarm_fired;
};

proctype user(chan output)
{
    output ! INPUT_CHECK_PASSWORD(1234);
};

proctype event(chan output)
{
    output ! INPUT_INTRUDER(0);
};

因此，基本上您必须同时检查（如果input 有的话！）和值，count以便在系统的内部FSM中执行转换。alarm

在示例中，我添加了一个proctype名称event，它将随机向系统发送单个INPUT_INTRUDER输入信号alarm。这与user输入他自己的密码相结合，可用于触发会导致警报触发的事件链。

于 2017-11-13T21:39:15.700 回答