Формальные методы в ИТ

Для повышения надёжности ключевые элементы компьютерной инфраструктуры должны быть формально верифицированы, т. е. должно быть математически доказано, что они соответствуют требованиям, проверка самих требований — отдельный вопрос, но и для этой задачи существуют формальные методы описания и верификации спецификаций. Верификация — не решение всех проблем, но это наиболее надёжный метод создания ПО из доступных нам, который позволяет быть уверенным, что реализация соответствует требованиям, ведь чаще всего ошибки случаются именно в реализации. Таким образом, мы сможем сделать иерархию надёжных компонентов, в которой каждый следующий будет опираться на надёжные предыдущие. Подробнее в отдельной статье [verify].


ОБСУДИТЬ