В информатике и инженерии программного обеспечения формальными методами называется группа техник, основанных на математическом аппарате для спецификации, разработки и верификации программного и аппаратного обеспечения. Использование формальных методов для проектирования программного и аппаратного обеспечения обусловлено ожиданиями того, что, как и в других инженерных областях, использование математического анализа может существенно поднять надёжность систем. При этом формальные методы довольно сложны, требуют специальной подготовки, временных и ресурсных вложений, и при этом нередко основываются на не всегда достижимых в реальных условиях предположениях. Это приводит к тому, что формальные методы чаще всего находят применение в проектировании высокоточных систем, где важность безопасности оправдывает любые средства.
Или
Формальные методы верификации ПО используют формальные модели
требований, поведения и окружения ПО для анализа его свойств. Такие модели
являются либо логико-алгебраическими, либо исполнимыми, либо промежуточными, имеющими черты и логико-алгебраических, и исполнимых моделей.
Назовите известные вам программные инструменты формальной верификации ПО.
Верификация – проверка корректности результатов некоторого этапа разработки по отношению к требованиям, сформулированным на предыдущих этапах.
Формальная верификация состоит из: формальная проверка, результаты и требования должны быть представлены в виде формальных моделей (результат = реализация, требования = спецификация), соответствие м-ду ними должно быть определено формально.
Полное модлирование:
n Дедуктивный анализ
(theorem proving) Floyd – 1967
n Проверка моделей
(model checking) Clarke, Emerson – 1981
n Проверка симуляции
(simulation checking, equivalence checking) Moore – 1956
n Символическое выполнение
(symbolic execution) Topor, Burstall – 1972
n Абстрактная интерпретация
(abstract interpretation) Cousot – 1975
Неполное моделирование:
n Формальное тестирование
(formal conformance testing) Василевский – 1973
Hennessy, DeNicola – 1984
Верификационный мониторинг
(runtime verification, passive testing)
С 1970-х было много работ, в которых этот термин не употреблялся
~1999 – термин (Havelund, Rosu?)
Какой из подходов формальной верификации ПО может быть полностью автоматизирован?
Проверка моделей