Как я могу связать данный ввод с другой функцией proctype?
Мне нужна помощь в соответствии с последующей задачей, которую я должен реализовать, используя jSpin а также promela язык.
Домашняя сигнализация может быть активирована и деактивирована с помощью персонального идентификационного ключа или пароля, после активации система вводит период ожидания около 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) на основании проверки?
1 ответ
Поскольку код в примере не соответствует спецификации, по крайней мере, насколько я понимаю, я написал пример с нуля.
Обратите внимание, что следующая модель (исходный код) преднамеренно очень многословна и избыточна по своей структуре, так что ее легче распознать ее логические блоки и - с надеждой - понять ее. На практике можно использовать встроенную функцию для обработки ввода. Я тоже не пользовалась SIGACT, SIGDEACT который появился в исходной модели, так как я не мог понять, кто должен был читать эти сообщения ни из исходной модели (исходного кода), ни из спецификации.
#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 набрав свой собственный пароль, можно использовать для запуска цепочки событий, которые могут привести к срабатыванию тревоги.