Редактирование: ВПнМ, 01 лекция (от 08 февраля)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 26: | Строка 26: | ||
* Проектирование, в ходе которого разрабатывается архитектура системы | * Проектирование, в ходе которого разрабатывается архитектура системы | ||
* Реализация | * Реализация | ||
- | * | + | * Темтированик |
- | * Эксплуатация, в ходе которой внедряется система, | + | * Эксплуатация, в ходе которой внедряется система, исопльзуется |
Ошибки могут появляться на всех этих этапах. В ходе анализа можно не так понять пользователя, в ходе разработки архитектуры, есть ошибки в ходе тестирования и эксплуатации. | Ошибки могут появляться на всех этих этапах. В ходе анализа можно не так понять пользователя, в ходе разработки архитектуры, есть ошибки в ходе тестирования и эксплуатации. | ||
- | Наибольшее количество ошибок вносится на этапах проектирования и реализации. Обнаруживаются на этапе тестирования, особенно сборочного. Выглядит всё неплохо, но цена ошибки резко | + | Наибольшее количество ошибок вносится на этапах проектирования и реализации. Обнаруживаются на этапе тестирования, особенно сборочного. Выглядит всё неплохо, но цена ошибки резко возврастает в ходе эксплуатации. |
== Правильность программ == | == Правильность программ == | ||
Строка 43: | Строка 43: | ||
Все другие ошибки, которые есть, выявляются во время разработки программы. Процесс поиска этих ошибок --- процесс верификации: проверка, соответствует ли реализация спецификации. При этом считается, что спецификация правильная. | Все другие ошибки, которые есть, выявляются во время разработки программы. Процесс поиска этих ошибок --- процесс верификации: проверка, соответствует ли реализация спецификации. При этом считается, что спецификация правильная. | ||
- | В ходе верификации/ | + | В ходе верификации/валидвции нужно найти ошибки, или доказать, что их нет. |
Когда средство создаётся, средств на тестирование обычно нет. Но существуют другие системы, в которых ошибок не должно быть ни при каких обстоятельствах. Это системы с повышенными требованиями к надёжности. Это системы либо с большой ценой ошибки, либо приводящие к невосполнимым потерям. | Когда средство создаётся, средств на тестирование обычно нет. Но существуют другие системы, в которых ошибок не должно быть ни при каких обстоятельствах. Это системы с повышенными требованиями к надёжности. Это системы либо с большой ценой ошибки, либо приводящие к невосполнимым потерям. | ||
Строка 82: | Строка 82: | ||
* Проверяется та программа, которая будет использоваться | * Проверяется та программа, которая будет использоваться | ||
* Для проведения теста не требуется дополнительных инструментальных средств | * Для проведения теста не требуется дополнительных инструментальных средств | ||
- | * Удобная локализация ошибки. Средства | + | * Удобная локализация ошибки. Средства тетстирования и отладки очень хорошо позволяют найти место в коде, где она находится |
Минусы: | Минусы: | ||
* Не всегда есть условия для тестирования системы | * Не всегда есть условия для тестирования системы | ||
- | * Проблема с воспроизводимостью тестов. Ошибка должна быть воспроизводима для понимания и отладки. Если речь идёт про системы взаимодействия с реальным окружением или когда она связана с историей взаимодействия, то в этих случаях ошибка может быть | + | * Проблема с воспроизводимостью тестов. Ошибка должна быть воспроизводима для понимания и отладки. Если речь идёт про системы взаимодействия с реальным окружением или когда она связана с историей взаимодействия, то в этих случаях ошибка может быть невоспроизводима. |
Эти минусы решаются применением имитационного моделирования: имитация окружения, и т. д. | Эти минусы решаются применением имитационного моделирования: имитация окружения, и т. д. | ||
Строка 92: | Строка 92: | ||
* ЧЯ: для последовательных программ сложно перебрать все входные данные | * ЧЯ: для последовательных программ сложно перебрать все входные данные | ||
* ЧЯ: для параллельных дополнительно возникают цепочки взаимодействия и перестановки | * ЧЯ: для параллельных дополнительно возникают цепочки взаимодействия и перестановки | ||
- | * ЧЯ: для динамических структур, | + | * ЧЯ: для динамических структур, взаимодейсьвующих с окружением --- невозможно |
* ПЯ: большой размер покрытия, растёт экспоненциально с размером | * ПЯ: большой размер покрытия, растёт экспоненциально с размером | ||
* Часто невозможно построение 100% покрытия, например, в случае наличия недостижимого кода. | * Часто невозможно построение 100% покрытия, например, в случае наличия недостижимого кода. | ||
Строка 132: | Строка 132: | ||
==== Системы с разделением ресурсов ==== | ==== Системы с разделением ресурсов ==== | ||
- | * Дорожный | + | * Дорожный траффик. Пример с дедлоком на перекрёстке |
* Телефонные сети. Если два человека звонят друг другу одновременно, то возникает блокировка. | * Телефонные сети. Если два человека звонят друг другу одновременно, то возникает блокировка. | ||
* ОС. Пример с дедлоком | * ОС. Пример с дедлоком | ||
Строка 181: | Строка 181: | ||
return m; | return m; | ||
} | } | ||
- | Проверим, инициализирована ли переменная m в месте, отмеченном стрелочкой. Для этого расширяем множество значениий m неинициализированным состоянием ( | + | Проверим, инициализирована ли переменная m в месте, отмеченном стрелочкой. Для этого расширяем множество значениий m неинициализированным состоянием (алсо, можно посмотреть [[Введение в теорию построения оптимизирующих компиляторов, 04 лекция (от 24 октября)|эту лекцию]] [[Введение в теорию построения оптимизирующих компиляторов|спецкурса Чернова]] — [[Участник:83.237.57.184|83.237.57.184]]): |
: dom(m) = Int + { ω } — возможные состояния m — множество значений Int и «пустое» состояние | : dom(m) = Int + { ω } — возможные состояния m — множество значений Int и «пустое» состояние | ||
: NI = { ω } — неинициализированные состояния — пустое состояние | : NI = { ω } — неинициализированные состояния — пустое состояние | ||
Строка 219: | Строка 219: | ||
Процесс верификации состоит из 3 этапов: | Процесс верификации состоит из 3 этапов: | ||
* Моделирование. Строим адекватную корректную модель. Цель моделирования --- объяснить. У нас есть программа, есть инструментальное средство верификации. У него есть свой язык. Иногда это делается путём трансляции с языка написания программы на входной язык средства. Но при этом может получиться слишком сложная модель. Тогда необходима абстракция, которая упрощает модель. Модель при этом должна быть корректной и адекватной. Более детально это будет рассматриваться на следующих лекциях. Корректная модель корректно моделирует, а адекватная корректно экстраполирует свойства на систему. Поскольку мы от чего-то абстрагируемся, оставляя то, что нужно, нужно знать, что нужно; модель без задачи не имеет смысла. Но обычно здесь формулируется класс свойств, например, корректна ли программа работает с разделяемыми ресурсами. Тогда построим модель программы, которая работает с разделяемыми ресурсами, от остального абстрагируемся. | * Моделирование. Строим адекватную корректную модель. Цель моделирования --- объяснить. У нас есть программа, есть инструментальное средство верификации. У него есть свой язык. Иногда это делается путём трансляции с языка написания программы на входной язык средства. Но при этом может получиться слишком сложная модель. Тогда необходима абстракция, которая упрощает модель. Модель при этом должна быть корректной и адекватной. Более детально это будет рассматриваться на следующих лекциях. Корректная модель корректно моделирует, а адекватная корректно экстраполирует свойства на систему. Поскольку мы от чего-то абстрагируемся, оставляя то, что нужно, нужно знать, что нужно; модель без задачи не имеет смысла. Но обычно здесь формулируется класс свойств, например, корректна ли программа работает с разделяемыми ресурсами. Тогда построим модель программы, которая работает с разделяемыми ресурсами, от остального абстрагируемся. | ||
- | * Спецификация свойств. Это темпоральная логика плюс | + | * Спецификация свойств. Это темпоральная логика плюс сс нккоторыми добавками, которые использует Spin. Вопрос полноты свойств здесь не затрагивается. Это вопрос валидации и мы считаем, что свойства полны. |
- | * Верификация. Мы передаём модель и свойства в инстр. систему, нажимаем на кнопку проверить, и получаем контрпример. Дальше нужно понять, о чём контрпример говорит, анализ контрпримеров --- это прерогатива человека, | + | * Верификация. Мы передаём модель и свойства в инстр. систему, нажимаем на кнопку проверить, и получаем контрпример. Дальше нужно понять, о чём контрпример говорит, анализ контрпримеров --- это прерогатива человека, котрый разбирается, что произошло: некорректная модель, модель не подходит для свойств, неправильная модель. Однако, если контрпример подтверждается, то мы нашли ошибку. Исправляем её и запускаем заново. Если модель конечная адекватна, то мы гарантированно получим ответ. Она позволяет выялвять редкие ошибки, которые обычно тестированием не выявляются. |
Недостаток: работает только для конечных моделей. Бывают такие программы и свойства, которые нельзя проверить с помощью конечной модели. Если кто-то захочет проверить самоприменимость, то никакая верификация не поможет. | Недостаток: работает только для конечных моделей. Бывают такие программы и свойства, которые нельзя проверить с помощью конечной модели. Если кто-то захочет проверить самоприменимость, то никакая верификация не поможет. |