DRAKON.SU

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

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




Начать новую тему Ответить на тему  [ Сообщений: 4 ] 
Автор Сообщение
СообщениеДобавлено: Среда, 12 Октябрь, 2016 07:36 

Зарегистрирован: Вторник, 22 Сентябрь, 2015 20:43
Сообщения: 76
Данная рубрика предназначена для вопросов, замечаний и предложений по магистерскому курсу

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

В настоящий момент в Новосибирском Государственном Университете прочитаны две лекции по второму разделу курса "Спецификация и верификация программ в предикатном и автоматном программировании". В ближайшее время они будут выложены на сайт. Лекции первого раздела по SMT-решателям, а также вводные лекции по курсу доступны на сайте.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 09 Январь, 2018 14:51 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 1443
Вот какие предложения возникают (с позиции предметника, не теоретика программирования).

А) Добавил бы в дополнительные источники работу Агафонова (описана в прилагаемой понятийной карточке) - как подводку к языковому базису ФМПИ. Ну и монографию (и/или пособия)
Зверева - для сведения о подходе к формальным методам (попытался пояснить своё понимание в аннотации на Пойа, так что прилагаю тоже). Вероятно, как классическое неформальное введение можно и Пойа - но на него, возможно, и так обращается внимание в других
курсах по специальности.

Б) Наверное, неплохо было бы (скорее всего, где-то в Разделе 4) обратить внимание на наглядные представления спецификаций и дать соответствующие источники. Аргументацию за
подобное можно, ессно, найти на этом же сайте - прежде всего для алгоритмических структур управления. К этому для полноты добавляется для структур данных и исполнителей. Некий
вариант связки - как описано у Фути и Судзуки: (структурно-временные диаграммы задействования трактов Катана-
исполнителя при прохождении данных по алгоритмам команд) - но удобно и по отдельности.

    Свежий пример потребности - авария на Восточном. Одна из версий - контроллер разгонного блока изначально был загружен данными о Байконуре как точке старта, а в связи с переназначением блока для применения с Восточного эти данные так и не поменяли.
    Возможно, проверка данных была ненаглядной - допустим, выводят для персонала (стартового в том числе) как сводки символьно. Если бы те же значения визуализировались (адекватно
    их смыслам; понятно, что на внешнем технологическом АРМ, а не скромными ресурсами бортовых), то что-то было бы проще "отловить". Конкретно эти данные - наложить на карту как
    точку - трудно предположить, что у стартовика, готовящего блок для запуска с Восточного, не вызвало бы вопросов положение исходной точки на Байконуре.

Кое-что есть в верификаторах - Spin, допустим, визуализирует модель (найденный контрпример). Кстати, обзор графических средств описания деятельности для программирования есть
в монографии Тюгашева (представлена в карточках Ист с Тюгашевым*) - может, достаточно на неё и сослаться.

В) Ну и основные результаты школы, к которой принадлежит Тюгашев, можно упомянуть в списке. Имеется в виду исчисление УА РВ. Как по-своему вводящее формальные методы в
программную инженерию. Есть монография (там же как /23/). Кстати, один из результатов - логико-временные модели - имеет формальное графическое представление, реализованное в
среде ГРАФКОНТ-ГЕОЗ. Но уж тут специалистам разбираться, какой где уровень формальности методов.


Вложения:
Ист с Тюгашевым из ТексТабГраф A3S СИН Каталоги Описание деятельности (текущий).pdf [115.28 КБ]
Скачиваний: 423
Ист Пойа из Макет Проект Прил3 Источники Информатика для занятых (текущий).pdf [139.38 КБ]
Скачиваний: 461
Ист Агафонов из ЛиТабГраф A3S Прил2 Источники ГРАФИТ (текущий).pdf [151.93 КБ]
Скачиваний: 405
Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Суббота, 05 Сентябрь, 2020 13:46 

Зарегистрирован: Вторник, 22 Сентябрь, 2015 20:43
Сообщения: 76
Многие хотели бы начать работать на какой-нибудь системе автоматического доказательства.
Но непонятно, какую выбрать. Их много. И все они такие сложные.

Рекомендую систему Why3.
Ее проще освоить по сравнению с другими, такими как PVS и Coq.
Язык функционального программирования WhyML, используемый для спецификаций и программирования,
обладает высокой выразительностью.
Имеется больший набор (~20) разнообразных автоматических мощных решателей.
Последняя версия Why3 оснащена универсальной и простой системой интерактивного доказательства,
позволяющая "руками" провести любое доказательство.
На системе Why3 выполнены десятки серьезных производственных проектов.

В прошлом году я верифицировал на Why3 семь нетривиальных программ из библиотеки ядра ОС Linux.
В этом году появился курс в Новосибирском Государственном университете:
    Язык спецификаций и методы автоматического доказательства в системе Why3

Видеолекции доступны на сайте: Формальные методы в программной инженерии, Раздел 4.

Имеется также дистрибутив Why3 с набором инструментов доказательства:
alt-ergo 2.3.0, cvc3 2.4.1, cvc4 1.7, z3 4.8.6, coq 8.9.0.
http://wasp.iis.nsk.su/pres/why3-1.3.1-deb.zip
В системе Windows ставится на версии VirtualBox, не ниже 6.1.6. Пользователь user,
пароль: 123. Нужно будет настроить связь через Windows-директорию (с общим доступом)
вашего компьютера. Запуск Why3 реализуется нажатием на файл с расширением mlw


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Суббота, 05 Сентябрь, 2020 19:42 

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

https://forum.oberoncore.ru/viewtopic.p ... 71#p112471


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 4 ] 

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


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

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


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

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