DRAKON.SU

Ваш разговор касался ли ДРАКОНа? Если да, просьба процитировать.

В первой лекции дано представление о формальной спецификации программ -- базисе формальных методов. Для программ-функций спецификация определяется в виде предусловия и постусловия. Управляющие программы КА относятся к классу реактивных систем. Их спецификация есть спецификация требований; см. другой ликбез.

Глава 2. Верификация программ

Программа является корректной, если она соответствует своей спецификации. Требование соответствия программы и спецификации определим здесь лишь для программ-функций: если перед исполнением программы истинно предусловие, то в случае завершения программы должно быть истинно постусловие. Данное условие принято называть условием частичной корректности. Программа-функция обязана всегда нормально завершаться, поскольку она не взаимодействует с окружением программы, а бесконечное исполнение -- бессмысленно. Это требование есть условие завершения программы. Объединение условий частичной корректности и завершения программы дает условие тотальной корректности программы.

Определим формально условия частичной корректности и завершения программы. Пусть П -- программа-функция со списком аргументов x и списком результатов y, P(x) -- предусловие, Q(x, y) -- постусловие, *П* обозначает предикат (зависящий от x и y), истинный тогда и только тогда, когда программа П нормально завершается. Предикат *П* строится по программе П на базе формальной семантики языка программирования.
Условия частичной корректности и завершения программы определяются, соответственно, формулами корректности:

P(x) and *П* => Q(x, y)

P(x) => exists y. *П*

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

Напомним, что изложение формальных методов на данном Форуме дается в упрощенном виде. Полное детальное описание представленного выше можно найти в статье.

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

- экспертиза
- тестирование
- статический анализ
- проверка на модели
- дедуктивная верификация
- абстрактная интерпретация, суперкомпиляция
- комбинированные методы

Развернутая классификация методов верификации программ дается в обзорной статье нашего классика Виктора Кулямина.

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

Методов тестирования огромное множество. Одним из наиболее эффективных является тестирование на базе формальных спецификаций.

Статический анализ обнаруживает семантические ошибки периода исполнения (деление на ноль, разыменование нулевого указателя и др.) статически на стадии компиляции программы не прибегая к исполнению кода. Статические анализаторы являются полезными для обнаружения ошибок, особенно в больших программных системах. Их недостаток в том, что они выдают большое число сообщений о возможных ошибках, которые на практике не подтверждаются. Следующее поколение статических анализаторов -- статические верификаторы, использующие SMT-решатели. Статические верификаторы (Software model checkers) способны эффективно проверять достижимость любой точки программы, а также истинность любого условия, вставляемого в код в виде оператора assert. Статические верификаторы весьма эффективны и применяются практически во всех крупных софтверных корпорациях. Интересен опыт использования статических верификаторов для верификации драйверов ядра операционной системы Linux.

Метод проверки на модели (model checking) применим для автоматической верификации систем с конечным числом состояний. Для программы строится модель в виде недетерминированного конечного автомата (обычно, модель Крипке). Проверяемые условия записываются на языке темпоральной логики LTL, CTL или др. В реальных приложениях инструмент проверки на модели может работать несколько недель. Ответом инструмента является вердикт об истинности проверяемого условия, либо контрпример, на котором проверяемое условие оказалось ложным.

В процессе дедуктивной верификации реализуется доказательство истинности формул корректности программы, которые предварительно должны быть автоматически сгенерированы по программе и ее спецификации. При доказательстве формул корректности необходимо использовать свойства предметной области, в рамках которой сформулирована исходная решаемая задача. Эти свойства должны быть записаны в виде логических утверждений и представлены в составе дополнительных теорий, все утверждения которых должны быть предварительно доказаны. Доказательства формул корректности проводятся с помощью инструментов автоматического доказательства теорем. Простые утверждения доказываются автоматически применением SMT-решателей. Для доказательства оставшихся утверждений используют инструменты интерактивного доказательства: PVS, Coq, HOL и др.

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

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

Кроме того, что нужно уметь проводить дедуктивную верификацию, необходимо также научится составлять математические модели для различных ситуаций.

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

А вот для того, чтобы верифицировать программы, где встречаются строки, стеки, сокеты, базы данных, графический интерфейс пользователя, web-сервисы и так далее необходимо сначала составить математическую модель и дальше доказывать с использованием этой модели. К сожалению, очень мало где описывается как применить математические модели к объектам, с которыми работает программист.

Поэтому кроме верификации нужно еще и учить составлять математические модели.

Я получил грант Фонда В.Потанина на разработку магистерского курса

Формальные методы в программной инженерии

Грант предусматривает разработку видеолекций и преподавание курса в двух аэрокосмических университетах: Самарском Университете и Сибирском Государственном Аэрокосмическом Университете (г. Красноярск).

Вводная лекция по курсу доступна на сайте:

http://wasp.iis.nsk.su/

Там же будут находиться другие лекции.
В ближайшее время появятся вводные лекции по четырем разделам курса.

Указанные аэрокосмические университеты ограничились частичным использованием материалов курса в своих учебных программах.
Поэтому у меня остались финансовые ресурсы, чтобы в рамках гранта вести преподавание еще в одном университете России.

Видеолекции будут доступны всем.
Выполнение индивидуальных заданий под присмотром лекторов, on-line консультации и прием экзаменов будут проводиться в тех университетах, где мы будем преподавать курс.
Предусмотрены командировки для приема экзаменов.

Таким Университетом может стать Ваш, если Вы этого захотите,
а главное, сумеете включить курс в существующую программу обучения у себя в
ректорате и деканате, конечно, пока в качестве факультативного курса.
Спешите.

Пишите мне по адресу: vshel@iis.nsk.su

Еще мне кажется был бы полезен курс по SMT-солверам. Так как в основном все SMT-солверы западные, не знаю вообще есть ли или были ли российские солверы. А учитывая курс на импортозамещение - это может быть актуально. В любом случае нужно обучать будущие поколения всему стеку технологий, которые сейчас используются, иначе через какое-то количество лет люди могут не разобраться как работает эта магическая штуковина.

http://forum.oberoncore.ru/viewtopic.php?p=98112#p98112

Правильно ли я понял, что Владимир Шелехов поставил крест на планах разработать свой Дракон-редактор?

Смотрите:
http://forum.oberoncore.ru/viewtopic.php?p=94602#p94602 от Четверг, 28 Январь, 2016 09:42

1. Учить, безусловно, применению SMT нужно.
2. По поводу российского не знаю точно, посмотрите украинский.

Да поставил. Но не крест. А грант Фонда В. Потанина тут не причем.

Изначально такое желание было.
Но Дракон-сообщество эту идею отвергло.
А в планах трехлетнего гранта РФФИ записана разработка конвертора на язык Дракон, причем не в этом году.
Однако сделать хотел в этом, Не повезло с исполнителем. И в этом году пока никого не нашел.

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

В последнее время Артем Бразовский из Минска познакомил меня со своей реализацией изоморфного преобразования дракон-схем из текста в графику (и обратно), что полностью подтверждает правильность Вашей идеи.

Ну и, конечно, от всего сердца поздравляю Вас с грантом фонда Потанина!
Желаю больших успехов!

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

В дедуктивной верификации обычно используется метод Хоара.
Программа должна быть написана на языке Си.
Разработка программы с дедуктивной верификацией по трудоемкости в 20 раз больше в сравнении с обычным стилем разработки, применяющим тестирование. Поэтому в больших программных комплексах дедуктивная верификация используется лишь для небольших критических участков кода.
Дедуктивная верификация при наличии в программе указателей становится крайне сложной.

Проверка на модели (Model Checking) возможна для небольших программ с конечным (не чрезмерно большим) числом состояний. Проверяемые условия корректности записываются на языке темпоральной логики, обычно LTL или CTL. Проверка реализуется автоматически. Проверка может проводиться в течении нескольких недель или даже месяцев. При обнаружении ошибки система выдает контрпример. Проверка на модели обходится дешевле дедуктивной верификации, но также требует высокой квалификации.

В программе Марсохода применялась лишь проверка на моделях, в частности потому, что руководитель проекта Джерард Хольцман является автором известной системы Spin.