DRAKON.SU

Текущее время: Четверг, 28 Март, 2024 23:48

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 50 ]  На страницу Пред.  1, 2, 3
Автор Сообщение
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 11 Декабрь, 2015 11:49 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5846
Откуда: Москва
TAU писал(а):
Я поговорил с Анатолием Абрамовичем.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Суббота, 12 Декабрь, 2015 14:31 

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

    Глава 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'а.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Вторник, 15 Декабрь, 2015 14:19 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 219
Откуда: Казань
Кроме того, что нужно уметь проводить дедуктивную верификацию, необходимо также научится составлять математические модели для различных ситуаций.

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

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Воскресенье, 11 Сентябрь, 2016 13:29 

Зарегистрирован: Вторник, 22 Сентябрь, 2015 20:43
Сообщения: 76
Я получил грант Фонда В.Потанина на разработку магистерского курса
Грант предусматривает разработку видеолекций и преподавание курса в двух аэрокосмических университетах: Самарском Университете и Сибирском Государственном Аэрокосмическом Университете (г. Красноярск).

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

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

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

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Понедельник, 12 Сентябрь, 2016 12:20 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 219
Откуда: Казань
Еще мне кажется был бы полезен курс по SMT-солверам. Так как в основном все SMT-солверы западные, не знаю вообще есть ли или были ли российские солверы. А учитывая курс на импортозамещение - это может быть актуально. В любом случае нужно обучать будущие поколения всему стеку технологий, которые сейчас используются, иначе через какое-то количество лет люди могут не разобраться как работает эта магическая штуковина.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Суббота, 01 Октябрь, 2016 18:43 

Зарегистрирован: Среда, 07 Январь, 2015 14:53
Сообщения: 1356
http://forum.oberoncore.ru/viewtopic.php?p=98112#p98112
Владимир Шелехов писал(а):
Я получил грант Фонда В.Потанина на разработку магистерского курса

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

Смотрите:
http://forum.oberoncore.ru/viewtopic.php?p=94602#p94602 от Четверг, 28 Январь, 2016 09:42
Цитата:
Разработка дуального (текстового и графического) редактора автоматных программ запланирована на следующий год в рамках работ по гранту РФФИ. Первая задача -- конструирование транслятора с языка автоматных программ на язык Дракон. Проектирование включает три этапа:
- разработка формальной семантики языка Дракон
- построение праобраза Дракон-программы в текстовом языке программирования
- кодирование автоматной программы через примитивы Дракон-программы.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Понедельник, 03 Октябрь, 2016 23:54 

Зарегистрирован: Воскресенье, 09 Март, 2008 22:38
Сообщения: 341
Rifat писал(а):
Еще мне кажется был бы полезен курс по SMT-солверам. Так как в основном все SMT-солверы западные, не знаю вообще есть ли или были ли российские солверы. А учитывая курс на импортозамещение - это может быть актуально. В любом случае нужно обучать будущие поколения всему стеку технологий, которые сейчас используются, иначе через какое-то количество лет люди могут не разобраться как работает эта магическая штуковина.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Среда, 05 Октябрь, 2016 19:32 

Зарегистрирован: Вторник, 22 Сентябрь, 2015 20:43
Сообщения: 76
LKom писал(а):
Владимир Шелехов писал(а):
Я получил грант Фонда В.Потанина на разработку магистерского курса

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Среда, 05 Октябрь, 2016 20:12 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5846
Откуда: Москва
Владимир Шелехов писал(а):
Изначально такое желание было.
Но Дракон-сообщество эту идею отвергло.
Почему отвергло?
Владимир Иванович, это не так. Возможно, были какие-то вопросы, но это обычное дело, тем более на форуме.
Я горячо поддерживаю Вашу идею дракон-редактора и по-прежнему надеюсь на успешное завершение Вашего проекта.

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Суббота, 20 Май, 2017 13:30 

Зарегистрирован: Вторник, 22 Сентябрь, 2015 20:43
Сообщения: 76
Rifat писал(а):
Что можете сказать про перспективы использования формальных методов при разработке бортового программного обеспечения?

Какие подход вы считаете наиболее перспективными?
- использование ручного доказательства при содействии proof checker-а.
- использование полностью автоматического доказательства

И какие методы Вы считаете наиболее перспективными?
- метод Хоара
- метод индуктивных утверждений
- Model Checking
- итд.

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

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

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

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


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 50 ]  На страницу Пред.  1, 2, 3

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 1


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2008-2024, участники конференции «DRAKON.SU», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB