Назовите известные вам программные инструменты формальной верификации ПО

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

Формальная верификация состоит из: формальная проверка, результаты и требования должны быть представлены в виде формальных моделей (результат = реализация, требования = спецификация), соответствие м-ду ними должно быть определено формально.

Полное модлирование:

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?)

146. Какой из подходов формальной верификации ПО может быть полностью автоматизирован?

Проверка моделей

147. Для ПО какого назначения и сфер применения следует использовать формальную верификацию?

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

148. В чём преимущество формальной верификации ПО по сравнению с тестированием?

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

149. Какой вид переносимости программ определяет стандарт POSIX?

на уровне исходных кодов