У формальных методов проверки программы есть место в промышленности?

Question

Я взглянул на Hoare Logic в колледже. То, что мы сделали, было очень просто. Большинство из того, что я сделал, доказывали правильность простых программ, состоящих из while петель, if инструкций и последовательности инструкций, но не более того. Эти методы кажутся очень полезными!

Формальные методы, используемые в промышленности широко?

Эти методы используются для определения критически важного программного обеспечения?

Answer 1

Это вопрос, близкий к моему сердцу (я исследователь в области проверки программного обеспечения с использованием формальной логики), поэтому вы, вероятно, не будете удивлены, когда я скажу, что эти методы имеют полезное место и еще не являются достаточно используемых в промышленности.

Существует множество уровней «формальных методов», поэтому я предполагаю, что вы имеете в виду те, кто опирается на строгую математическую основу (в отличие от, скажем, следуя примеру 6-сигма-стиля). Некоторые типы формальных методов имели большой успех - системы типов, являющиеся одним из примеров. Статические аналитические инструменты, основанные на анализе потока данных, также популярны, проверка модели почти повсеместна в аппаратном дизайне, а вычислительные модели, такие как Pi-Calculus и CCS, по-видимому, вдохновляют некоторые реальные изменения в практическом дизайне языков для параллелизма. Анализ терминации - это тот, который недавно был прессой - проект SDV в Microsoft и работа Байрона Кука - это недавние примеры исследования/практики кроссовера в формальных методах.

Hoare Reasoning пока не сделал больших успехов в отрасли - это по многим причинам, чем я могу перечислить, но я подозреваю, что в основном это связано со сложностью написания, а затем доказывает спецификации для реальных программ (они, как правило, получают big, и не могут выразить свойства многих сред реального мира). Различные подполя в этом типе рассуждений в настоящее время вносят большой вклад в эти проблемы - разделяющая логика - одна.

Это частично характер текущих (твердых) исследований. Но я должен признаться, что мы, как теоретики, полностью не смогли обучить отрасль тому, почему наши методы полезны, чтобы они соответствовали отраслевым потребностям и чтобы они были доступны для разработчиков программного обеспечения. На каком-то уровне это не наша проблема - мы исследователи, часто математики, и практическое использование не является главным в наших умах. Кроме того, разрабатываемые методы часто слишком эмбриональны для использования в крупномасштабных системах - мы работаем над небольшими программами, на упрощенных системах, получаем математику и двигаемся дальше. Я не так много покупаю эти оправдания, хотя - мы должны быть более активными в продвижении наших идей и получении обратной связи между отраслью и нашей работой (одна из основных причин, по которой я вернулся к исследованиям).

Это, вероятно, хорошая идея для меня, чтобы воскресить мой блог, и сделать еще несколько сообщений на этом материале ...

Answer 2

«Формальные методы, используемые в промышленности?»

Да.

Заявление assert на многих языках программирования связано с формальными методами проверки программы.

«Являются ли формальные методы широко используемыми в промышленности?»

No.

«Являются ли эти методы используются для доказательства критически важного программного обеспечения?»

Иногда. Чаще всего они используются, чтобы доказать, что программное обеспечение безопасно. Более формально они используются для подтверждения определенных утверждений о безопасности, связанных с безопасностью.

Answer 3

Ну, сэр Тони Хоар присоединился к Microsoft Research около 10 лет назад, и одна из вещей, которые он начал, - это формальная проверка ядра Windows NT. Действительно, это была одна из причин долгой задержки Windows Vista: начиная с Vista, большие части ядра - это, фактически формально подтвержденный wrt. к некоторым свойствам, таким как отсутствие тупиков, отсутствие утечек информации и т. д.

Это, конечно, не типично, но, вероятно, это самое важное применение формальной проверки программы с точки зрения ее воздействия (в конце концов, почти каждый человек бытие в некотором роде, форма или форма, на которые влияет компьютер под управлением Windows).

Answer 4

Да, они используются, но не широко во всех областях. Существует больше методов, чем простая логика, некоторые из них используются больше, а некоторые меньше, в зависимости от пригодности для данной задачи. Общей проблемой является то, что программное обеспечение является biiiiiiig и проверяет, что все это правильно, все еще слишком сложно.

Например, теоретический прокси (программное обеспечение, которое помогает людям проверять правильность программы) ACL2 используется для доказательства того, что определенный процессор обработки с плавающей точкой не имеет определенного типа ошибок. Это была большая задача, поэтому эта техника не слишком распространена.

Проверка модели, еще одна форма формальной проверки, используется довольно широко в наши дни, например, Microsoft предоставляет тип проверки модели в наборе для разработки драйверов и может использоваться для проверки драйвера на набор распространенных ошибок. Контроллеры моделей также часто используются для проверки аппаратных схем.

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

Answer 5

Polyspace является а (чудовищно дорого, но очень хороший) коммерческий продукт на основе верификации программ. Это довольно прагматично, поскольку он масштабируется от «расширенного модульного тестирования, которое, вероятно, найдет некоторые ошибки», «следующие три года вашей жизни будут потрачены, показывая, что эти 10 файлов имеют нулевые дефекты».

Он основан скорее на отрицательной проверке («эта программа не испортит ваш стек») вместо положительной проверки («эта программа будет делать именно то, что эти 50 страниц уравнений говорят, что это будет»).

Answer 6

Я не могу комментировать много критически важных программ, хотя я знаю, что индустрия авионики использует широкий спектр методов для проверки программного обеспечения, в том числе методов стиля Хоар.

Формальные методы пострадали, поскольку ранние сторонники, такие как Эдсберг Дейкстра, настаивали на том, что их следует использовать повсюду. Ни формализмы, ни поддержка программного обеспечения не были выполнены. Более разумные сторонники считают, что эти методы следует использовать для трудных задач. Они широко не используются в промышленности, но усыновление растет. Вероятно, наибольшие успехи были в использовании формальных методов для проверки свойств безопасности программного обеспечения. Некоторые из моих любимых примеров - это контрольная модель SPIN и сопроводительный код Джорджа Некулы.

Исходя из практики и исследований, проект операционной системы Microsoft Singularity основан на использовании формальных методов для обеспечения гарантий безопасности, которые обычно требуют аппаратной поддержки. Это, в свою очередь, приводит к более быстрой работе и более надежным гарантиям.Например, в особенности они доказали, что если в систему разрешен сторонний драйвер устройства (что означает, что основные условия проверки были доказаны), тогда он не может уничтожить всю эту ОС –, что он наихудший, что он может сделать, это собственное устройство.

Формальные методы еще широко не используются в промышленности, но они более широко используются, чем 20 лет назад, а через 20 лет они будут использоваться еще более широко. Итак, вы надеетесь на будущее :-)

Answer 7

Чтобы добавить к answer Йорга, вот interview с Тони Хоаре. Инструменты Jorg, на мой взгляд, относятся к PREfast и PREfix. См. here для получения дополнительной информации.

Answer 8

Существует два разных подхода к формальным методам в отрасли.

Один из подходов - полностью изменить процесс разработки. Обозначения Z и метод B, которые были упомянуты, относятся к этой первой категории. B был применен к разработке безликой линии метро 14 в Париже (если у вас есть шанс, заберитесь в передний вагон. Не часто вы получаете возможность увидеть рельсы перед вами).

Другой, более инкрементный подход заключается в том, чтобы сохранить существующие процессы разработки и проверки и заменить только одну из задач проверки за один раз новым методом. Это очень привлекательно, но это означает разработку инструментов статического анализа для выхода, используемых языков, которые часто нелегко анализировать (потому что они не были разработаны). Если вы идете (например)

http://dblp.uni-trier.de/db/indices/a-tree/d/Delmas:David.html

(извините, только одна гиперссылка допускается для новых пользователей :()

вы найдете примеры практического применения формальных методов верификации C (со статическими анализаторами Astrée, Caveat, Fluctuat, Frama-C) и двоичным кодом (с инструментами от AbsInt GmbH).

Кстати, поскольку вы упомянули Hoare Logic в приведенном выше списке инструментов, только Caveat основанный на логике Хоар (и Frama-C имеет плагин логики Hoare). Другие r а также абстрактную интерпретацию, другую технику с более автоматическим подходом.

Answer 9

Помимо других более процедурных подходов, Хоара логика была в основе дизайна по контракту, введенная в качестве метода объектно-ориентированного Бертран Мейер в Eiffel (see Meyer's article of 1992, страница 4). Хотя дизайн по контракту - это не то же самое, что формальные методы проверки (во-первых, DbC не не доказывает ничего, пока программное обеспечение не будет выполнено), на мой взгляд, это обеспечивает более практическое использование.

Answer 10

Область моей компетенции - использование формальных методов для анализа статического кода, чтобы показать, что программное обеспечение не содержит ошибок во время выполнения. Это реализовано с использованием метода формальных методов, известного как «абстрактная интерпретация». Этот метод существенно позволяет вам доказать некоторые атрибуты s/w-программы. Например. докажите, что a + b не будет переполняться, или x/(x-y) не приведет к делению на ноль. Примером статического анализа, который использует этот метод, является Polyspace.

Что касается вашего вопроса: «Являются ли формальные методы широко используемыми в промышленности?» и «Используются ли эти методы для определения критически важного программного обеспечения?»

Ответ на этот вопрос да.Это мнение основано на моем опыте и поддержке инструмента Polyspace для отраслей промышленности, которые полагаются на использование встроенного программного обеспечения для управления критическими для безопасности системами, такими как электронный дроссель в автомобиле, тормозная система для поезда, контроллер реактивного двигателя, инфузионный насос для доставки лекарств, и т. д. Эти отрасли действительно используют эти типы инструментов формальных методов.

Я не верю, что все 100% этих отраслевых сегментов используют эти инструменты, но использование увеличивается. Мое мнение таково, что индустрия аэрокосмической промышленности и автомобилестроения ведет к тому, что индустрия медицинских устройств быстро наращивает использование.