Описание тега model-checking

Описание тега Вопросы с тегом
Проверка модели относится к следующей проблеме: данная модель системы автоматически проверяет, соответствует ли эта модель заданной спецификации.
1 ответ

Как исследование символического состояния работает в проверке символьной модели

Следующий алгоритм представляет собой грубый эскиз проверки модели с помощью Computational Tree Logic (CTL): Заявлено, что: Задача проверки модели для CTL состоит в том, чтобы проверить для заданной системы переходов TS и формулы CTL Φ, если TS |= Φ…
30 май '18 в 02:55
1 ответ

Построить формальную модель UART в NuSMV?

Я изучаю проверку моделей и NuSMV для моего образования. Я могу редактировать и запускать код NuSMV, и у меня есть четкое представление о том, что такое UART и что делает. Моя задача - формально смоделировать UART с NuSMV, но в настоящее время я не …
26 фев '17 в 15:27
1 ответ

Spin Verification, проверка переменной достигает определенного значения

Это мой первый вопрос на Stack Exchange, так что если есть что-то, что нарушает правила, пожалуйста, дайте мне знать. У меня есть программа, написанная на Promela для ОС колледжа и класса параллельных систем. Есть два запущенных процесса, которые ув…
08 мар '17 в 11:47
1 ответ

Проблемы со спецификацией сплава

Ниже приведена так называемая спецификация сплава, которую я недавно закончил для текстовых сообщений мобильного телефона. Это просто основные требования к текстовым сообщениям, и, поскольку это практика, у меня нет строгих требований к соблюдению. …
07 янв '13 в 14:15
1 ответ

Как изменить порядок сообщений в канале?

У меня есть этот код необходимо изменить, чтобы каналы могли переупорядочить сообщения, и я должен добавить механизм, чтобы справиться с этим chan linkA = [10] of {byte}; chan linkB = [10] of {byte}; proctype sender () { byte n; do :: n<10 -> …
15 янв '19 в 21:14
1 ответ

Как я могу изменить псевдо-код на код NuSMV?

Мой профессор решил дать нам студент-математик код для преобразования в NuSMV, и я не могу найти помощь где-либо еще, и я читаю учебник, он всего 6 страниц и описывает только то, что делает определенное свойство. Модуль main является примером кода N…
27 май '16 в 18:59
2 ответа

Как создать структуру крипки в NuSMV?

Я должен создать структуру Крипке в NuSMV, и я должен проверить некоторые свойства. Кто-нибудь поможет мне? Структура и свойства (LTL, CTL и CTL*) приведены на рисунках. Здесь есть структура и свойства: http://cl.ly/image/1x0b1v3E0P0D/Screen%20Shot%…
16 окт '14 в 14:58
1 ответ

Как я могу связать данный ввод с другой функцией proctype?

Мне нужна помощь в соответствии с последующей задачей, которую я должен реализовать, используя jSpin а также promela язык. Домашняя сигнализация может быть активирована и деактивирована с помощью персонального идентификационного ключа или пароля, по…
13 ноя '17 в 20:05
0 ответов

Временная логика для моделирования событий в отдельные моменты времени, вызывающие состояния / изменения в течение определенного периода времени

Я ищу подходящий формализм (то есть временную логику) для моделирования ситуации следующего типа Могут быть события, происходящие в отдельные события во времени (при условии, что условия будут подробно описаны ниже). Есть государство. Это состояние …
20 апр '15 в 13:19
2 ответа

Вопросы линейной временной логики (LTL)

[] = всегда O = следующий ! = отрицание <> = в конце концов Интересно, это []<> это эквивалентно просто []? Также трудно понять, как распределить временную логику. [] [] (ИЛИ! b) !<> (! а и б) [] ([] a ==> <> b)
17 мар '16 в 00:48
2 ответа

Существует ли программное обеспечение для проверки моделей (например, Java Path Finder), но для C#?

< EDIT > Об этом вопросе не по теме и слишком основанном на мнении, я постараюсь быть более ясным. Моя цель состояла в том, чтобы понять, существует ли такой инструмент, меня не интересовали мнения о том, что является лучшим. В то время, когда я пис…
03 сен '13 в 19:37
1 ответ

Как смоделировать очередь в промеле?

Итак, я пытаюсь смоделировать замок CLH-RW в Promela. Способ блокировки прост: действительно: Очередь состоит из tail, к которому и читатели и писатели ставят в очередь узел, содержащий единственный bool succ_must_wait они делают это, создавая новый…
03 ноя '17 в 09:28
1 ответ

UPPAAL: что заставило часы перестать работать

В настоящее время я использую симулятор UPPAAL. Мой симулятор перестает запускать код после определенного момента. Этот момент варьируется в зависимости от декларации, которую я предоставляю. Но я хотел бы знать, вообще, когда часы перестают работат…
24 фев '14 в 05:08
2 ответа

Ошибка соглашения о соединении - C

В следующем коде есть ошибка соглашения о вызовах (возможно, ведущая к вечному циклу), и я не могу ее обнаружить. Я пытаюсь подтвердить код, используя "Satabs". Какая модель может вывести ошибку на поверхность. Со следующей моделью я получаю сегфо. …
04 окт '15 в 12:26
1 ответ

Реализовать символическое выполнение без проверки модели

Как я могу реализовать symbolic execution за particular language без использования model checking а также Finite State Machine (FSM) например not такие как Java Path Finder? Мне нужна деталь об этом. например, на каком языке я могу реализовать это с…
14 сен '16 в 12:34
1 ответ

LTL свойства и программа Promela

У меня есть следующая программа, которая моделирует FIFO с процессом в PROMELA: mtype = { PUSH, POP, IS_EMPTY, IS_FULL }; #define PRODUCER_UID 0 #define CONSUMER_UID 1 proctype fifo(chan inputs, outputs) { mtype command; int data, tmp, src_uid; bool…
09 фев '17 в 23:21
1 ответ

Создание автоматического изображения моей модели Promela

Я использую графический интерфейс SPIN - iSPIN. Графический интерфейс поставляется с хорошим генератором представления Automaton, однако, чтобы увидеть полный автомат, мне нужно увеличить / уменьшить масштаб. Также я хотел бы сохранить этот автомат …
23 мар '15 в 21:26
1 ответ

Причина различий в количестве достижимых состояний

Я проверяю 8-битный сумматор с этим кодом. Когда я печатаю, число достижимых состояний равно 1, если основной модуль пуст, и 2^32, если весь основной модуль включен. Что делает эту разницу в сообщаемом количестве достижимых состояний? Для 4-разрядно…
08 май '17 в 05:52
1 ответ

Как SPIN определяет порядок выполнения процессов в атомарных процессах?

Я пытаюсь понять, как SPIN выбирает порядок выполнения и завершения процессов в следующем примере. Я понимаю, что основное внимание в SPIN уделяется анализу параллельных процессов, но для моих целей я просто заинтересован в простом линейном выполнен…
25 июл '17 в 02:50
1 ответ

Пытаясь понять часы и тайм-ауты в UPPAAL

Мне нужно смоделировать систему как синхронизированный автомат с UPPAAL, и я действительно озадачен тем, как UPPAAL управляет часами и стражами в соответствии с прошедшим временем: похоже, UPPAAL просто игнорирует охрану часов! Я предполагаю, что мо…
22 янв '15 в 11:32