Вопросы по теме 'formal-verification'
Как интерпретировать вывод ошибки SPIN?
Я пытаюсь смоделировать проверку простой модели Promela для следующего свойства LTL:
ltl { M[0] U M[1] }
И я получаю сообщение об ошибке, управляемое моделирование по следу ошибки дает следующий результат:
ltl ltl_0: (M[0]) U (M[1])
spin:...
3722 просмотров
schedule
23.06.2023
Дело Идриса / тактика индукции
Они были реализованы в Idris 0.9.14, и я успешно использовал induction для некоторых доказательств. Однако они работают только для некоторых типов библиотек; в то время как, например, Vect поддерживает их, почти изоморфный All - нет:...
301 просмотров
schedule
01.02.2023
Как мне перевести утверждения / свойства жизнеспособности PSL или SVA в Verilog?
как я могу перевести утверждения жизнеспособности PSL или SVA в Verilog вручную или автоматически с помощью инструмента (с открытым исходным кодом)? Я могу делать простые свойства безопасности, но понятия не имею о свойствах живучести. Я знаю, что в...
624 просмотров
schedule
30.10.2022
Как доказать прекращение длины рекурсивного списка?
Допустим, у нас есть список:
List = nil | Cons(car cdr:List).
Обратите внимание, что я говорю о списках, которые можно изменять! И тривиальная рекурсивная функция длины:
recursive Length(List l) = match l with
| nil => 0
|...
418 просмотров
schedule
19.02.2022
Frama-c не может проанализировать приведенный вручную пример ACSL list_length, включающий конструкцию сопоставления с образцом
В следующем определении функции (list.c):
//@ type list<A> = Nil | Cons(A,list<A>);
/*@ logic integer list_length<A>(list<A> l) =
@ \match l {
@ case Nil : 0
@ case Cons(h,t) : 1 + list_length(tail)
@ };
*/...
107 просмотров
schedule
07.07.2022
как написать формальный тест восстановления сброса, который имеет длительное время
Я использовал для проверки модуля, состоящего из последовательного порта с набором регистров, с помощью динамических тестов. Один из тестов - это тест восстановления и сброса. Последовательность синхронизации: (i) записать случайные данные в регистр...
76 просмотров
schedule
03.06.2023
Действительно ли статический анализ является формальной проверкой?
Я читал о формальной проверке, и основная мысль заключается в том, что для работы с ней требуется формальная спецификация и модель. Однако многие источники классифицируют статический анализ как формальную методику проверки, некоторые упоминают...
1536 просмотров
schedule
19.11.2022
Статическая редукция частичного порядка в заданном пространстве состояний
В большинстве работ о редукции частичного порядка предполагается, что анализируемая система задана как набор процессов с некоторым оператором композиции. Это имеет большой смысл, поскольку вы не хотите сначала вычислять пространство состояний, а...
34 просмотров
schedule
04.06.2023
Есть ли способ узнать, что вызывает «Нет экземпляра» при запуске в Alloy?
Я написал в модели, используя Alloy. Однако для определенных условий выполнение предиката для поиска экземпляра не выполняется, и он говорит, что экземпляр не может быть найден. Я попытался увеличить привязку примерно до 16 экземпляров, но не нашел...
382 просмотров
schedule
28.05.2023
Переписывание простого доказательства теоремы
Я написал определение group в Idris:
data Group: Type -> Type where
Unit: (x: t) -> Group t
(*): Group t -> Group t -> Group t
Inv: Group t -> Group t
postulate
assoc: (a : Group t) -> (b : Group t) -> (c :...
138 просмотров
schedule
25.08.2022
Проверка модели LTL с помощью SPIN
Я смотрю на программное обеспечение SPIN. Я хотел бы использовать его для поиска моделей теорий LTL. Во всех руководствах и туториалах говорится о проверке свойств алгоритмов, но меня это совершенно не интересует. Я просто хочу найти модели формул...
554 просмотров
schedule
07.07.2022
В Dafny, как я могу исправить значение, не удовлетворяющее ограничениям подмножества ошибки 'nat' при делении?
Этот код Дафни :
method Div(n: nat, d: nat) returns (q: nat)
requires d > 1
{
q := n / (d - 1);
}
выдает эту ошибку:
Dafny 2.1.1.10209
stdin.dfy(4,9): Error: value does not satisfy the subset constraints of 'nat'
Dafny program...
359 просмотров
schedule
05.04.2023
Как работает исследование символического состояния в проверке символьной модели
Следующий алгоритм представляет собой грубый набросок проверки модели. с логикой вычислительного дерева (CTL):
Утверждается, что:
Задача проверки модели для CTL состоит в том, чтобы проверить для данной системы переходов TS и...
90 просмотров
schedule
08.10.2023
Ошибка проверки UPPAAL — значение индекса вне допустимого диапазона
Я использую Uppaal для проверки системы. Моделирование работает отлично, но когда я проверяю это свойство A[] not deadlock , оно дает мне следующую ошибку:
_The successors of this state are not well defined.
Index value 3 is out of range....
406 просмотров
schedule
19.11.2022
Почему в Alloy не встречается простой целочисленный контрпример?
Я пытаюсь смоделировать связь между числовой переменной и логической переменной, в которой, если числовая переменная находится в определенном диапазоне, логическая переменная изменит значение. Я новичок в Alloy, и у меня возникли проблемы с...
127 просмотров
schedule
13.01.2023
Могу ли я построить структуру while алгебраически, используя класс и локаль?
Я создаю программные операторы из алгебраических структур, а не использую определения или функции. То есть, чтобы установить их свойства в Isabelle с помощью локали или команд класса. Теперь мне нужно построить оператор while.
Я знаю, что могу...
103 просмотров
schedule
21.05.2022
Функция преобразования типа данных очень долго проверяется
Изабель нужно много времени, чтобы доказать правильность (на мой взгляд) довольно простых функций преобразования типов данных. В качестве примера я создал типы данных для представления математических и логических выражений и функцию, которая упрощает...
56 просмотров
schedule
05.03.2023
Доказуемо правильная сортировка?
Существуют ли схемы сериализации (упорядочения) структур данных, правильность которых может быть формально доказана?
Я не отношусь к конкретному языку программирования, это может быть ocaml/haskell или cpp, java или другой, если можно предположить,...
43 просмотров
schedule
06.06.2023
ACSL-доказательство функции, которая проверяет, отсортирован ли массив в порядке возрастания или убывания
Я пытаюсь доказать правильность функции, которая проверяет, отсортирован ли массив в порядке возрастания/убывания или не отсортирован. Поведение должно возвращать -1, если отсортировано в порядке убывания , 1, если отсортировано в порядке...
247 просмотров
schedule
21.09.2022
Примените лемму к ветви конъюнкции без разделения на coq
У меня есть союз, давайте абстрагируем его как: A /\ B и у меня есть лемма, доказывающая, что C -> A и я хочу получить в результате цель C /\ B . Это возможно?
Если да, то мне было бы интересно, как это сделать. Если я использую разбиение,...
99 просмотров
schedule
03.08.2023
