Имеют ли место формальные методы проверки программ в промышленности?
Я взглянул на Hoare Logic в колледже. То, что мы сделали, было действительно просто. Большую часть того, что я сделал, было доказательство правильности простых программ, состоящих из while петли, if заявления и последовательность инструкций, но не более того. Эти методы кажутся очень полезными!
Широко ли используются формальные методы в промышленности?
Используются ли эти методы для доказательства критически важного программного обеспечения?
10 ответов
Этот вопрос мне близок (я - исследователь в области верификации программного обеспечения с использованием формальной логики), поэтому вы, вероятно, не удивитесь, когда я скажу, что я считаю, что эти методы полезны и еще недостаточно используются в промышленность.
Существует много уровней "формальных методов", поэтому я предполагаю, что вы имеете в виду те, которые опираются на строгую математическую основу (в отличие, скажем, после некоторого процесса в стиле 6-сигма). Некоторые типы формальных методов имели большой успех - системы типов являются одним из примеров. Инструменты статического анализа, основанные на анализе потока данных, также популярны, проверка моделей почти повсеместна в аппаратном проектировании, а вычислительные модели, такие как Pi-Calculus и CCS, похоже, вдохновляют на реальные изменения в практическом проектировании языка для параллелизма. Анализ прекращения - тот, который был в последнее время широко освещен - проект SDV в Microsoft и работа Байрона Кука - недавние примеры кроссовера исследования / практики в формальных методах.
До сих пор Hoare Reasoning не добился больших успехов в отрасли - это по многим причинам, которые я не могу перечислить, но я подозреваю, что это в основном связано со сложностью написания, а затем с проверкой спецификаций для реальных программ (они имеют тенденцию становиться большими и терпеть неудачу выразить свойства многих реальных мировых сред). Различные подполя в этом типе рассуждений в настоящее время делают большие шаги в этих проблемах - логика разделения - одна.
Это частично характер продолжающихся (трудных) исследований. Но я должен признаться, что мы, теоретики, совершенно не смогли объяснить индустрии, почему наши методы полезны, чтобы они соответствовали потребностям отрасли и сделали их доступными для разработчиков программного обеспечения. На некотором уровне это не наша проблема - мы исследователи, часто математики, и практическое использование не является главным в наших умах. Кроме того, разрабатываемые методы часто слишком зачаточны для использования в крупномасштабных системах - мы работаем над небольшими программами, над упрощенными системами, занимаемся математикой и идем дальше. Хотя я не очень-то покупаю эти оправдания - мы должны быть более активными в продвижении наших идей и получении обратной связи между отраслью и нашей работой (одна из главных причин, по которой я вернулся к исследованиям).
Вероятно, это хорошая идея, чтобы я возродил свой блог и сделал еще несколько публикаций на эту тему...
Что ж, сэр Тони Хоар присоединился к Microsoft Research около 10 лет назад, и одна из вещей, которые он начал, была формальная проверка ядра Windows NT. Действительно, это было одной из причин длительной задержки Windows Vista: начиная с Vista, большие части ядра фактически проверяются формально. определенным свойствам, таким как отсутствие тупиков, отсутствие утечек информации и т. д.
Это, конечно, не типично, но, вероятно, это единственное наиболее важное применение формальной проверки программы с точки зрения ее воздействия (в конце концов, почти каждый человек в той или иной форме подвержен влиянию той или иной формы компьютера, работающего под управлением Windows).
Я не могу много комментировать критически важное программное обеспечение, хотя я знаю, что индустрия авионики использует широкий спектр методов для проверки программного обеспечения, включая методы в стиле Хоара.
Формальные методы пострадали, потому что ранние защитники, такие как Эдсгер Дейкстра, настаивали на том, что они должны использоваться везде. Ни формализм, ни поддержка программного обеспечения не подошли к работе. Более разумные сторонники считают, что эти методы следует использовать для решения сложных проблем. Они не широко используются в промышленности, но их использование растет. Вероятно, наибольшее распространение получили формальные методы проверки свойств безопасности программного обеспечения. Некоторые из моих любимых примеров - проверка модели SPIN и код проверки Джорджа Некулы.
Отходя от практики и к исследованиям, проект операционной системы Microsoft Singularity предусматривает использование формальных методов для обеспечения гарантий безопасности, которые обычно требуют аппаратной поддержки. Это, в свою очередь, приводит к более быстрой производительности и более сильным гарантиям. Например, в единственном числе они доказали, что если в систему допущен драйвер устройства стороннего производителя (что означает, что базовые условия проверки были доказаны), то он не может отключить всю эту ОС - он хуже всего может сделать это подключить ее. собственное устройство.
Формальные методы еще не получили широкого применения в промышленности, но они используются более широко, чем 20 лет назад, а через 20 лет они будут все еще широко использоваться. Так что вы ориентированы на будущее:-)
Да, они используются, но не широко во всех областях. Есть больше методов, чем просто логика Hoare, некоторые используются больше, некоторые меньше, в зависимости от пригодности для данной задачи. Общая проблема заключается в том, что программное обеспечение является biiiiiiig, и проверка того, что все это правильно, все еще является слишком сложной проблемой.
Например, средство доказательства теорем (программное обеспечение, которое помогает людям в проверке правильности программы) ACL2 использовалось для доказательства того, что определенный блок обработки с плавающей запятой не имеет ошибок определенного типа. Это была большая задача, поэтому эта техника не слишком распространена.
Проверка моделей, другой вид формальной проверки, используется в настоящее время довольно широко, например, Microsoft предоставляет тип проверки моделей в комплекте для разработки драйверов, и ее можно использовать для проверки драйвера на наличие ряда распространенных ошибок. Модели проверки также часто используются при проверке аппаратных схем.
Тщательное тестирование также может рассматриваться как формальная проверка - есть некоторые формальные спецификации, какие пути программы должны быть проверены и так далее.
"Используются ли формальные методы в промышленности?"
Да.
assert Оператор во многих языках программирования связан с формальными методами проверки программы.
"Широко ли используются формальные методы в промышленности?"
Нет.
"Используются ли эти методы для доказательства критически важного программного обеспечения?"
Иногда. Чаще всего они используются, чтобы доказать, что программное обеспечение является безопасным. Более формально, они используются, чтобы доказать определенные связанные с безопасностью утверждения о программном обеспечении.
Моя область знаний - использование формальных методов для статического анализа кода, чтобы показать, что программное обеспечение не содержит ошибок времени выполнения. Это реализуется с помощью формальной методики, известной как "абстрактная интерпретация". Техника, по сути, позволяет вам доказать определенные атрибуты как / W программы. Например, докажите, что a+b не будет переполнено или x/(xy) не приведет к делению на ноль. Примером инструмента статического анализа, который использует эту технику, является Polyspace.
Относительно вашего вопроса: "Широко ли используются формальные методы в промышленности?" и "Используются ли эти методы для доказательства критически важного программного обеспечения?"
Ответ - да. Это мнение основано на моем опыте и поддержке инструмента Polyspace для отраслей, которые полагаются на использование встроенного программного обеспечения для управления критическими для безопасности системами, такими как электронный дроссель в автомобиле, тормозная система для поезда, контроллер реактивного двигателя, инфузионный насос для доставки лекарств, и т.д. Эти отрасли действительно используют эти типы инструментов формальных методов.
Я не верю, что все 100% этих сегментов промышленности используют эти инструменты, но их использование растет. Мое мнение таково, что аэрокосмическая и автомобильная промышленность лидируют в отрасли медицинского оборудования, быстро наращивающей использование.
Существует два разных подхода к формальным методам в отрасли.
Один из подходов - полностью изменить процесс разработки. Обозначения Z и B-метод, которые были упомянуты, относятся к этой первой категории. B был применен для развития линии метро без водителя 14 в Париже (если у вас есть шанс, заберитесь в передний вагон. У вас не часто есть шанс увидеть рельсы перед вами).
Другой, более постепенный, подход заключается в сохранении существующих процессов разработки и проверки и замене только одной из задач проверки одновременно новым методом. Это очень привлекательно, но это означает разработку инструментов статического анализа для выхода из используемых языков, которые зачастую нелегко анализировать (потому что они не предназначены для этого). Если вы идете (например)
http://dblp.uni-trier.de/db/indices/a-tree/d/Delmas:David.html
(извините, для новых пользователей разрешена только одна гиперссылка:()
Вы найдете примеры практического применения формальных методов для проверки программ на Си (с помощью статических анализаторов Astrée, Caveat, Fluctuat, Frama-C) и двоичного кода (с помощью инструментов от AbsInt GmbH).
Кстати, поскольку вы упомянули Hoare Logic, в приведенном выше списке инструментов только Caveat основан на логике Hoare (а Frama-C имеет подключаемый модуль логики Hoare). Другие полагаются на абстрактную интерпретацию, другую технику с более автоматическим подходом.
Polyspace - это (ужасно дорогой, но очень хороший) коммерческий продукт, основанный на проверке программ. Это довольно прагматично, поскольку оно масштабируется от "расширенного модульного тестирования, которое, вероятно, обнаружит некоторые ошибки", до "следующих трех лет вашей жизни, которые будут потрачены на то, чтобы эти 10 файлов не имели дефектов".
Она основана скорее на отрицательной проверке ("эта программа не повредит ваш стек"), а не на положительной проверке ("эта программа будет делать именно то, что говорят эти 50 страниц уравнений").
Помимо других процедурных подходов, логика Хоара лежала в основе " Проектирования по контракту", представленного Бертраном Мейером в Eiffel как объектно-ориентированная техника ( см. Статью Майера от 1992 года, стр. 4). Хотя Design by Contract - это не то же самое, что формальные методы проверки (с одной стороны, DbC ничего не доказывает, пока не будет запущено программное обеспечение), на мой взгляд, он обеспечивает более практическое использование.