Python: Нужен инструмент проверки моделей и результаты конвертации в CNF
Я хотел бы протестировать мой код с помощью средства проверки моделей и сделать из него FSM автоматически. Для этого мне нужна программа проверки моделей и преобразования результатов FSM в CNF.
Любой совет, как я могу сделать это в Python? Я знаю только CBMC, но это ограничено C.
Спасибо Адриан
1 ответ
Python не является языком, подходящим для проверки моделей, например, утка позволяет свободно создавать исключения. Если ваш код по сути процедурный, то вы можете сначала попытаться преобразовать его в C с помощью py2c или какой-то эквивалент.
Тогда используйте modex извлечь promela модель из C код. Этот последний шаг называется абстракцией. Тогда вы можете использовать SPIN Модель проверки для проверки свойств, представляющих интерес.
Если CNF означает "Нормальная конъюнктивная форма", то я не понимаю, как CNF относится к результатам проверки модели. Проверка модели дает либо "да, ваша модель моделирует предоставленную вами логическую формулу", либо "нет, это не так, и вот контрпример, почему бы и нет". CNF является особой синтаксической формой для булевых формул.
Если вы упомянули CNF как актуальную для проверки ограниченной модели с CBMC и SAT решение, участвующее в этом, то, пожалуйста, обратите внимание, что SPIN принимает в качестве входных данных модели Крипке, выраженные с использованием promela язык. Таким образом, вам не нужно ничего преобразовывать в булеву формулу, и, кроме того, вы можете запустить полную проверку живучести.
Чтобы узнать больше об инструментах проверки моделей, взгляните на этот список. В частности, если вы хотите накатить свой собственный конвертер из python в promela Тогда вы можете найти полезные проекты: promela-metamodel - ocaml библиотека для promela - pi2promela - Программа для преобразования Promela.
Также обратите внимание, что "FSM" (конечный автомат) - это преобразователь, а не структура Крипке. Преобразователь имеет как входы, так и выходы. Он реагирует на входы, производя результаты. Это является результатом синтеза в состязательной обстановке, где человек имеет среду (управляющую входами) и систему (управляющую выходами) и хочет синтезировать стратегию, которая удовлетворяет некоторой спецификации, выраженной в форме логической формулы. Существует несколько инструментов для решения этой проблемы. В результате получается машина Мили или машина Мура (они разные и не эквивалентны), оба являются типами преобразователей.
Преобразователь не является структурой Крипке (или системой переходов, хотя последний термин обычно используется неправильно, поэтому лучше обратиться к структуре или модели Крипке, которые могут быть представлены графом с состояниями, помеченными предложениями, на которые вы ссылаетесь в логическая формула, которая является желаемой спецификацией).
Обратите внимание на то, что синтез является противоположностью верификации (проверка модели является формой верификации): синтез в закрытой системе (без среды) берет формулу и синтезирует модель, удовлетворяющую ей, в форме структуры Крипке. Проверка закрытой системы берет модель и требуемую формулу, а затем проверяет, удовлетворяет ли модель спецификации. Синтез замкнутой системы также может быть выполнен с использованием частичной модели (в том смысле, что она определяет, что является допустимым поведением, но включает в себя больше поведений, чем то, что требуется и выражается с помощью логической формулы), вместе с логической формулой и дает подмодель того, что удовлетворяет (или "моделирует") логическая формула.
Синтез открытой системы может быть выполнен с логической формулой в качестве входных данных, а затем, решая игру между системой и средой, мы получаем преобразователь, который реализует стратегию для системы, чтобы удовлетворить логическую формулу, независимо от того, как среда выбирает играть (при условии, что среда соответствует логической формуле).
Обратите внимание на разницу между преобразователем (FSM), имеющую отношение к синтезу открытых систем (и, конечно, к проверке, но контролеры моделей обычно принимают в качестве входных данных закрытые системы, поэтому моделирование среды в настройке закрытой системы должно выполняться путем введения неконтролируемого -детерминизм в структуре Крипке) и структура Крипке или система конечных переходов, которые задаются в качестве входных данных для синтеза в замкнутой системе.