Может ли Coq использоваться (легко) в качестве проверки модели?

Ответ 1

Помощник проверки, такой как Coq, будет проверять, что ваше доказательство является обоснованным и что любые предлагаемые вами теоремы могут (или не могут) быть получены с использованием аксиомами и ранее доказанными результатами. Он также предоставит вам поддержку в предложении доказательных шагов, чтобы уменьшить усилия, которые вы должны предпринять для выполнения доказательств.

Контроллер модели, напротив, символически перечисляет пространство состояний спецификации и определяет, нарушено ли какое-либо из условий проверки. В этом случае он предоставит трассировку ошибок, показывающую, какая последовательность изменений состояния вызовет нарушение.

Обычно они имеют очень разные требования к обработке на заднем плане, но, хотя их можно объединить в один инструмент, средство Coq не похоже на это.

Язык спецификации Temporal Logic of Actions (TLA +) вместе со спутником TLA + Proof System (TLAPS) была разработана Лесли Лампортом, чтобы обосновать большие формальные спецификации. Он был расширен с помощью алгоритма PlusCal, который поддерживает проверку моделей алгоритмов, которые переводятся в представление TLA +.

μ-исчисление - это обозначение, используемое в качестве низкоуровневого подкрепления для многих формальных методов. Вы также должны взглянуть на логическую задачу выполнимости для более грубого подхода. Претенденты теории, как правило, более сложны в своем дизайне и используют традиционные концепции экспертной системы/ИИ, а также библиотеки доказательных правил, определенных экспертами, для обеспечения поддержки, необходимой для выполнения обязательств по доказательству.

В качестве другого примера инструмента доказательства вы можете посмотреть метод Event-B и сопутствующую платформу разработки Rodin. Это будет при уточнении спецификации более конкретно идентифицировать доказательства обязательств и попытаться механически выполнить их, оставив трудные для вас делать.

Для проверки модели вы можете посмотреть:

• Alloy и
• Dafny,

среди свободно доступных вариантов.

Ответ 2

В дополнение к существующему ответу @Pekka, μ-calculus является обозначением для разговоров о фиксированных точках, которые представляют собой решения проблем достижимости.

• Примером наименее фиксированной точки (μ) является наибольшее множество состояний, которые могут быть достигнуты, начиная с где-то (например, из первой строки программы). Это "наименее" фиксированная точка из-за того, что она является наименьшей среди возможных других фиксированных точек. Он получается, начиная с пустого набора и добавляя состояния до достижения фиксированной точки. При определенных условиях существование фиксированной точки обеспечивается теоремой Кнастера-Тарского.

• Примером наибольшей фиксированной точки (ν) является наибольшее множество, которое мы можем оставаться внутри без нарушения некоторых требований безопасности. Это "наибольшая" фиксированная точка, потому что она получается, начиная с совокупности всех состояний (так, сверху в частичном порядке множеств, определенных отношением подмножества), и итеративно ограничивая ее, пока мы не достигнем фиксированной точки. Наибольшие фиксированные точки являются двойственными по наименьшим фиксированным точкам, поэтому одна и та же теорема применяется для существования и единственности. Подумайте о графическом поиске в качестве другого примера.

Перемещая тип фиксированных точек в формуле μ-исчисления, мы можем выразить временное поведение, подобное: "Я хочу, чтобы вы продолжали идти туда и обратно между двумя местоположениями" или "Я хочу, чтобы сервер в конечном итоге отвечал на каждый попросите его получить".

Затем мы можем моделировать проверку (с помощью счетной или символической проверки модели), подразумевается ли указанное нами свойство системой, которую мы разработали.

• SPIN - это перечисляющая проверка модели: она хранит каждое состояние, которое она исследует в хеш-таблице, и включает некоторые алгоритмы для признавая, что ему не нужно перечислять все государства, но может относиться к некоторым из них как к представителям других государств (с точки зрения проверяемого имущества эти состояния эквивалентны, поэтому достаточно рассуждать об одном из них). Эти методы называются частичное сокращение порядка.

• NuSMV - это средство проверки символической модели. Он по-прежнему ищет состояния системы, но не представляет их один за другим в памяти. Вместо этого он сохраняет следы наборов состояний, представляя эти множества как двоичные диаграммы решений. Это структуры данных, которые могут оставаться небольшими, даже если они представляют собой множества с состояниями 10**24. Там гарантия для этого. К сожалению, они все еще могут взорваться по размеру, и, к сожалению, это происходит почти для всех булевых функций (поэтому почти все множества, которые мы можем представить), как Клод Шеннон доказал.

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

Разница между верификацией и синтезом заключается в чередовании quantifiers:

• проверка имеет единую количественную оценку (все универсальные, обычно)
• синтез имеет переменную количественную оценку: он включает вложенные экзистенциальные и универсальные кванторы.

Конечно, можно также проверить количественную формулу, например \forall x: \exists y: f(x, y). Разве это не просто проверка? Ну, это, демонстрируя, что нет никакой математической разницы в основе дела, между синтезом и проверкой. Традиционно встречаются в основном вышеупомянутые случаи того, как квантификация появляется в том, какие проблемы рассматриваются как синтез, и какие проблемы рассматриваются как проверка.

Основная реальная разница между синтезом и проверкой заключается в том, как мы используем результат проверки правильности формулы:

• При проверке мы уже имеем реализацию системы, которую хотим, и проверяем, что она удовлетворяет некоторым желаемым свойствам. Если нет, мы собираемся (вручную) попытаться исправить реализацию, а затем снова проверить.

• В синтезе есть некоторые части окончательной системы, которые мы еще не полностью детализировали. Мы позволяем выбирать эту деталь инструментом, который мы используем. Другими словами, инструмент устраняет экзистенциальные квантификаторы таким образом, чтобы сделать формулу истиной и сообщает нам, что она сделала, чтобы мы завершили систему таким образом, гарантируя, что формула истинна.

Примером инструмента синтеза в C является gr1c, еще один пример в Python - omega. Есть несколько других инструментов.

Однако вы подходите к проблеме, по крайней мере, убедитесь, что вы пишете, что такое план, вы пишете спецификацию.

Одна из лучших книг по этим темам - Лесли Лампорт Задание систем. И убедить, что разные представления - это лица одного и того же, подумайте о том, чтобы читать Информатика и государственные машины.

Ответ 3

Существует некоторая работа по использованию Coq в качестве проверки модели, например, см. https://github.com/coq-contribs/smc. Тем не менее, я не знаю людей, которые использовали это в серьезных приложениях.