Вопросы по теме 'model-checking'
Как получить текущее значение часов в UPPAAL и сохранить его в целочисленной переменной?
Может ли кто-нибудь сказать мне, как получить текущее значение переменной часов и сохранить в целочисленной переменной. Я пробовал k = t (где k - целое число, а t - часы), но он выдает «ошибку несовместимого типа». Я также пробовал k=(int)t, но он...
2336 просмотров
schedule
26.09.2022
Каков размер формулы LTL?
Что обычно подразумевается под размером формулы LTL, |p|, с точки зрения сложности? Количество атомарных предложений, глубина или что-то еще?
Заранее спасибо!!
247 просмотров
schedule
12.05.2023
Нестандартные обозначения, используемые для точечного языка
Я изучал исследовательскую работу по Graph. Моделирование грамматики (проверка модели). Чтобы лучше понять, я начал исследование экспериментов , проведенных исследователи.
Они использовали точечную нотацию для указания структур графа и...
315 просмотров
schedule
25.06.2022
Недостигнутая ошибка в Promela
Для следующего кода
proctype A()
{
byte cond1;
time = time + 1;
time = time + 2;
t[0] = 3;
a[0] = 2;
do
:: (a[0] == 0)->break;
:: else -> a[0] = a[0] - 1;
do
:: (t[0] <= t[1])->break;
od;
if
:: (cond1 != 0)...
536 просмотров
schedule
11.12.2023
LTL, CTL или TLA для моделирования моей модели (подробное описание внутри)?
В настоящее время я пишу магистерскую диссертацию и столкнулся с уточнением и проверкой моего подхода в темпоральной логике.
Какую темпоральную логику лучше всего использовать в моих обстоятельствах? Мне бы очень хотелось получить отзывы о моем...
1124 просмотров
schedule
21.04.2023
Атомарные предложения Promela для нескольких экземпляров proctype
Мне было интересно, как написать никогда утверждения, которые обозначают все экземпляры proctype. Например, если у меня есть следующее предложение:
#define c (camera_node[SomePid]:start_publishing == 0)
Теперь, если я создам 5 экземпляров...
97 просмотров
schedule
11.07.2023
LTL о Fp=TUp, действительно ли T необходим для перезаписи F?
Я только что пришел с этим вопросом. Как написано в книге «Логика в компьютерных науках», одним из важных эквивалентов LTL является следующее: Fp=TUp. И Т означает отсутствие ограничений.
Но что, если я заменю T на (не p)? Выполняется ли Fp=(не...
125 просмотров
schedule
18.03.2023
Как сравнить два LTL?
Как я могу сравнить два LTL, чтобы увидеть, могут ли они противоречить друг другу? Я спрашиваю об этом, потому что у меня есть иерархический конечный автомат и LTL, описывающие поведение в каждом состоянии. Мне нужно знать, может ли локальный LTL...
173 просмотров
schedule
19.07.2022
Вопросы линейной временной логики (LTL)
[] = всегда
О = следующий
! = отрицание
‹> = в конце концов
Интересно, это []‹> эквивалентно просто []?
Также трудно понять, как распределять временную логику.
[][] (a OR !b)
!‹>(!а И б)
[]([] a ==> <> b)
547 просмотров
schedule
30.11.2023
Запуск NuSMV на Mac
Я скачал исходный код NuSMV для Mac и начал установку с помощью README. Тем не менее, есть шаг, который просит меня выполнить сборку с использованием «cmake..», когда я запускаю эту проблему. Исходный каталог не содержит CMakeLists.txt.
Любая...
1265 просмотров
schedule
21.08.2022
Проверка алгоритма взаимного исключения Dekker с помощью NuSMV
Я использую NuSMV для проверки алгоритма Деккера, и мой код выглядит следующим образом:
MODULE main
VAR
b1 : {true, false};
b2 : {true, false};
k : {1, 2};
pr1 : process proc(k, b1, b2, 1);
pr2 : process proc(k, b2, b1, 2);
ASSIGN
init(b1) :=...
367 просмотров
schedule
16.01.2023
Могу ли я сказать, что пространство состояний — это формальная спецификация поведения некоторой системы?
Учитывая систему и ее полное пространство состояний, могу ли я сказать, что это пространство состояний является формальной спецификацией поведения этой системы?
90 просмотров
schedule
25.08.2022
Проверка ограниченной модели с помощью Z3 — построение выражений
мы используем Z3 для проверки ограниченной модели. Для этого приведем целую кучу выражений следующего вида:
state_A_1 && !state_B_1 && sometrigger => !state_A_2 & state_B_2
Другими словами, мы кодируем течение времени...
407 просмотров
schedule
29.03.2023
реализовать символьное выполнение без проверки модели
Как я могу реализовать symbolic execution для particular language без использования model checking и Finite State Machine (FSM) , например not , таких как Java Path Finder ? Мне нужны подробности об этом. например, на каком языке я могу...
201 просмотров
schedule
21.05.2022
Преобразование утверждения SystemVerilog с задержкой в invarspec
Я хочу преобразовать утверждение SystemVerilog с задержкой в invarspec формального верификатора. Синтезатор выдает синтаксическую ошибку для ##1 в строке кода ниже.
assert property ( ( req1 == 0 ) ##1( req1 == 1 ) ##1 !( req2 == 1 ) || ( gnt1...
187 просмотров
schedule
09.02.2023
преобразовать программу fifo systemC на язык PROMELA со свойствами безопасности и живучести
пожалуйста, я большой специалист в области tihs, как я могу преобразовать классический пример FIFO, написанный в коде systemC, в язык PROMELA со свойствами в LTL, удовлетворяющими следующим трем свойствам:
Взаимное исключение: процессы...
288 просмотров
schedule
22.06.2022
Как определить глобальные константы в NuSMV?
Я не знаю, как объявить глобальные константы в NuSMV таким же образом, как
#define n 5
in C .
Как я могу сделать это в NuSMV?
665 просмотров
schedule
03.10.2023
Причина разницы в количестве достижимых состояний
Я проверяю 8-битный сумматор с помощью этого кода. Когда я печатаю, число доступных состояний равно 1, если основной модуль пуст, и 2^32, если включен весь основной модуль. Что делает эту разницу в сообщаемом количестве достижимых состояний? Для...
95 просмотров
schedule
02.07.2023
SMT/SAT Solver и средство проверки моделей
Недавно я начал изучать методы формальной проверки. В литературе модуль проверки и решатель используются как взаимозаменяемые. Но как связаны друг с другом средство проверки моделей и решатель?
p.s. Я был бы признателен, если бы некоторые...
1207 просмотров
schedule
26.03.2023
Моделирование NuSMV с использованием случайных трасс
Я пытаюсь запустить «случайное» или недетерминированное моделирование модели NuSMV, которую я создал. Однако между последующими запусками трассировка, которая создается, точно такая же.
Вот модель:
MODULE main
VAR x : 0..4;
VAR clk : 0..10;...
371 просмотров
schedule
02.03.2023
