Публикации по теме 'model-checking'
Введение в проверку моделей с помощью TLA+
В этом месяце я ставлю перед собой задачу завершить серию онлайн-лекций в университете Введение в проверку моделей . Курс ведет Йост-Питер Катоен, один из авторов книги Принципы проверки моделей . Катоен отмечает, что курс больше сосредоточен на теории, чем на применении. Однако, поскольку у меня есть небольшой опыт в этой области, я использую курс и упражнения в качестве предлога для практики использования TLA+ и связанных с ним инструментов, языка алгоритмов Pluscal и TLC Model..
Вопросы по теме 'model-checking'
проблемы со спецификацией сплава
Ниже приведена так себе спецификация сплава, которую я недавно закончил для текстовых сообщений с мобильного телефона. Это всего лишь основные требования к текстовым сообщениям, и, поскольку это практика, у меня нет строгих требований, которые нужно...
226 просмотров
schedule
15.08.2022
Оператор Select в Promela намного медленнее, чем эквивалентный оператор if?
Поэтому я использовал следующую строку в своем коде Promela.
select( cycles: 26..31 );
Однако это вызывало взрыв государства. Я заменил его следующим оператором if , и внезапно проблема взрыва состояния исчезла. Разве оператор select ,...
350 просмотров
schedule
21.08.2023
Проверка взаимоблокировки и поиск вне диапазона массива Uppaal
Когда я запускаю запрос A[] not deadlock в Verifier на моей модели, проверка останавливается с ошибкой:
Проверка была прервана из-за ошибки. Скорее всего, это вызвано присваиванием вне диапазона или поиском в массиве вне диапазона....
1239 просмотров
schedule
06.02.2023
Доступ к членам составных сортировок (типов данных) в SMT-LIBv2
Согласно разд. 3.9.3 из Язык и инструменты SMT-LIBv2: учебное пособие возможно чтобы объявить составную сортировку, подобную этой, в SMT-LIBv2:
(set-logic QF_UF)
(declare-sort Triple 3)
(declare-fun state () (Triple Bool Bool Bool))
Я...
139 просмотров
schedule
10.04.2022
Проверить эквивалентные формулы CTL
Я делаю упражнение CTL, я пытаюсь проверить, эквивалентны ли следующие формулы. Но я не уверен, правильно ли я поступаю.
EF (p or q) = EF(p) or EF(q) ?
AF(p or q) = AF(p) or AF(q) ?
A(p U ( A(q U r) )) = A(A(p U q) U r) ?
Первая формула:...
969 просмотров
schedule
12.09.2022
Запуск NuSMV на OSX
Я установил NuSMV с помощью предоставленного файла readme, однако, когда я пытаюсь использовать команду NuSMV, я получаю следующее сообщение: -bash: NuSMV: команда не найдена
В интернете мало информации по этому поводу, буду признателен за любую...
1309 просмотров
schedule
05.07.2023
Найдите минимальное значение переменной для всех возможных исполнений с помощью формулы LTL.
Рассмотрим следующую Promela модель двух процессов, которые управляют общей переменной N :
byte N = 0;
active [2] proctype P(){
byte temp, i;
i = 1;
do
:: i < 10 ->
temp = N;
temp++;...
164 просмотров
schedule
07.04.2023
Построить формальную модель UART в NuSMV?
Я изучаю проверку моделей и NuSMV для своего образования. Я могу редактировать и запускать код NuSMV, и у меня есть четкое представление о том, что такое UART и что он делает.
Моя задача — формально смоделировать UART с помощью NuSMV, но пока я не...
143 просмотров
schedule
03.11.2022
Как SPIN определяет порядок выполнения процессов в атомарных процессах?
Я пытаюсь понять, как SPIN выбирает порядок выполнения и завершения процессов в следующем примере. Я понимаю, что основное внимание в SPIN уделяется анализу параллельных процессов, но для моих целей меня интересует простое линейное выполнение. В...
392 просмотров
schedule
17.06.2022
как смоделировать очередь в промеле?
Итак, я пытаюсь смоделировать блокировку CLH-RW. в Промеле.
Принцип работы замка на самом деле прост:
Очередь состоит из узла tail , в котором и читатели, и писатели ставят в очередь узел, содержащий один узел bool succ_must_wait . Они...
465 просмотров
schedule
14.04.2022
Преобразование системы переходов состояний в формулы свойств LTL
В контексте проверки ограниченной модели система описывается как система переходов состояний и свойства, которые необходимо проверить. Когда нужно предоставить несколько системных описаний и свойств инструменту проверки модели, может стать...
205 просмотров
schedule
22.06.2023
UPPAAL: проверка члена массива
Можно ли проверить, является ли объект элементом массива в UPPAAL?
Если у меня есть целочисленный массив
int ap[1,2];
Я хочу сделать запрос в верификаторе, где у меня есть что-то вроде:
E<> 1 \in Process.ap[1]
Кроме того,...
469 просмотров
schedule
02.09.2022
Как вычислить достижимое символьное пространство состояний для бинарной диаграммы решений
Этот вопрос касается того, как сгенерировать символическое пространство состояний для средства проверки символьной модели. Сначала я вхожу в предысторию, которая заставляет меня хотеть сделать это для MDD, затем я объясняю вопрос более подробно....
215 просмотров
schedule
30.03.2023
синтаксическая ошибка вложенного оператора NEXT в NuSMV
Я пытаюсь использовать NuSMV для проверки своей модели, и вот код.
Однако, когда я ввожу NuSMV kernel.smv в оболочку, возникает ошибка
file kernel.smv: line 16: nested NEXT operators: next(_b)
in definition of next(_cond)
in definition...
298 просмотров
schedule
21.04.2023
NuSMV: как исключить возможное следующее состояние
Я хочу исключить возможный следующий случай при определенных условиях. Например, у меня есть:
token : array 1..2 of {0, 1, 2, 3, 4, 5, 6};
next(token[1]) := case
x : {1, 2, 3, 4, 5, 6};
TRUE : 0;...
128 просмотров
schedule
11.08.2022
Могут ли структуры Крипке иметь охрану?
У меня есть простая структура крипке, где у меня есть 3 состояния со следующими переходами:
s1 --> s2
s2 --> s1
s1 --> s3
s3 --> s3
s1 — единственное начальное состояние. Я не хочу, чтобы цикл от s1 до s2 повторялся более...
87 просмотров
schedule
22.11.2022
Проверка модели: неверные префиксы с использованием NFA
Мы используем NFA для моделирования BadPrefixes для свойства безопасности. Я хочу понять для данного свойства безопасности, как моделировать NFA.
Следующие изображения приведены для справки.
Например, для свойства безопасности...
232 просмотров
schedule
29.06.2022
Как мне правильно установить NuSMV, поскольку при загрузке bin-файл не содержит .exe-файла?
Я следую руководству по установке NuSMV в Windows 10. Он загружается нормально, но после извлечения файлов из заархивированной (.tar) папки я не нахожу файл .exe в папке «bin», которая должна быть там (конечно). Я загружаю его с веб-сайта NuSMV....
82 просмотров
schedule
04.09.2022
