Я взглянул на Hoare Logic в колледже. То, что мы сделали, было очень просто. Большинство из того, что я сделал, доказывали правильность простых программ, состоящих из операторов while loops, if и последовательности инструкций, но не более того. Эти методы кажутся очень полезными!
Являются ли формальные методы широко используемыми в промышленности?
Используются ли эти методы для определения критически важного программного обеспечения?
Это вопрос, близкий моему сердцу (я исследователь в Software Verification с использованием формальной логики), поэтому вы, вероятно, не будете удивлены, когда я скажу, что эти методы имеют полезное место и еще не используются достаточно в отрасли.
Существует много уровней "формальных методов", поэтому я предполагаю, что вы имеете в виду те, кто опирается на строгую математическую основу (в отличие от, скажем, следуя примеру 6-сигма-стиля). Некоторые типы формальных методов имели большой успех - системы типов, являющиеся одним из примеров. Инструменты статического анализа, основанные на анализе потока данных, также популярны, проверка модели почти повсеместна в аппаратном дизайне, а вычислительные модели, такие как Pi-Calculus и CCS, кажутся вдохновляющими на реальные изменения в практическом языке для concurrency. Анализ терминации - это тот, который в последнее время преуспел в прессе - проект SDV в Microsoft и работа Байрона Кука - это недавние примеры кросс-исследований в области исследований/практики в формальных методах.
Hoare Reasoning пока не преуспел в отрасли - это по многим причинам, чем я могу перечислить, но я подозреваю, что в основном это связано со сложностью написания, а затем с проверкой спецификаций для реальных программ (они, как правило, становятся большими, и не могут выразить свойства многих сред реального мира). Различные подполя в этом типе рассуждений в настоящее время вносят большой вклад в эти проблемы - Логика разделения является одной.
Это отчасти характер текущих (твердых) исследований. Но я должен признаться, что мы, как теоретики, полностью не смогли обучить отрасль тому, почему наши методы полезны, чтобы они соответствовали отраслевым потребностям и чтобы они были доступны для разработчиков программного обеспечения. На каком-то уровне это не наша проблема - мы исследователи, часто математики, и практическое использование не в наших умах. Кроме того, разрабатываемые методы часто слишком эмбриональны для использования в крупномасштабных системах - мы работаем над небольшими программами, на упрощенных системах, получаем математику и двигаемся дальше. Я не так много покупаю эти оправдания, хотя мы должны проявлять большую активность в продвижении наших идей и создании обратной связи между отраслью и нашей работой (одна из основных причин, по которой я вернулся к исследованиям).
Вероятно, хорошая идея для меня воскресить мой блог и сделать еще несколько сообщений по этому поводу...
Ну, сэр Тони Хоар присоединился к Microsoft Research около 10 лет назад, и одна из вещей, которые он начал, - это формальная проверка ядра Windows NT. Действительно, это была одна из причин долгой задержки Windows Vista: начиная с Vista, большие части ядра на самом деле официально подтверждены wrt. к определенным свойствам, таким как отсутствие тупиков, отсутствие утечек информации и т.д.
Это, конечно, не типично, но, вероятно, это самое важное приложение для проверки официальной программы с точки зрения ее влияния (в конце концов, почти каждый человек в какой-то мере имеет форму или форму, на которые влияет компьютер, работающий под управлением Windows).
Я не могу много прокомментировать критически важное программное обеспечение, хотя я знаю, что индустрия авионики использует широкий спектр методов для проверки программного обеспечения, в том числе методов стиля Хоар.
Формальные методы пострадали, потому что ранние сторонники, такие как Эдсберг Дейкстра, настаивали на том, что их следует использовать повсюду. Ни формализмы, ни поддержка программного обеспечения не были выполнены. Более разумные сторонники считают, что эти методы следует использовать для трудных задач. Они широко не используются в промышленности, но усыновление растет. Вероятно, наибольшие успехи были в использовании формальных методов для проверки свойств безопасности программного обеспечения. Некоторые из моих любимых примеров - это SPIN проверка модели и код доказательства, не содержащий Джорджа Некула.
Отвлекаясь от практики и исследований, Microsoft Singularity проект операционной системы использует формальные методы для обеспечения гарантий безопасности, которые обычно требуются аппаратная поддержка. Это, в свою очередь, приводит к более быстрой работе и более надежным гарантиям. Например, в сингулярности они доказали, что если в систему разрешен драйвер стороннего устройства (что означает, что основные условия проверки были доказаны), то это не может привести к разрушению всей этой ОС: худшее, что он может сделать, это собственное устройство.
Формальные методы пока еще широко не используются в промышленности, но они более широко используются, чем 20 лет назад, и через 20 лет они будут еще более широко использоваться. Таким образом, вы надежно защищены: -)
Да, они используются, но не широко во всех областях. Существует больше методов, чем простая логика, некоторые из них используются больше, а некоторые меньше, в зависимости от пригодности для данной задачи. Общей проблемой является то, что программное обеспечение является biiiiiiig и проверяет, что все это правильно, все еще слишком сложно.
Например, теорема-доказательство (программное обеспечение, которое помогает людям в доказательстве правильности программы) ACL2 используется для доказательства того, что определенный процессор обработки с плавающей точкой не имеет определенного типа ошибок. Это была большая задача, поэтому этот метод не слишком распространен.
Проверка модели, другая форма формальной проверки, используется довольно широко в наши дни, например, Microsoft предоставляет тип проверки модели в наборе для разработки драйверов и может быть использована для проверки драйвера для набора общих ошибок. Контроллеры моделей также часто используются для проверки аппаратных схем.
Строгое тестирование можно также рассматривать как официальную проверку - есть некоторые формальные спецификации, какие пути программы должны быть проверены и т.д.
"Используются ли формальные методы в промышленности?"
Да.
Оператор assert во многих языках программирования связан с формальными методами проверки программы.
"Являются ли формальные методы широко используемыми в промышленности?"
Нет.
"Используются ли эти методы для определения критически важного программного обеспечения?"
Иногда. Чаще всего они используются, чтобы доказать, что программное обеспечение безопасно. Более формально они используются для подтверждения определенных утверждений о безопасности, связанных с безопасностью.
Существует два разных подхода к формальным методам в отрасли.
Один из подходов состоит в том, чтобы полностью изменить процесс разработки. Обозначения 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). Другие полагаются на абстрактную интерпретацию, другую технику с более автоматическим подходом.
Моя область знаний - это использование формальных методов для анализа статического кода, чтобы показать, что программное обеспечение не имеет ошибок во время выполнения. Это реализовано с использованием метода формальных методов, известного как "абстрактная интерпретация". Этот метод существенно позволяет вам доказать некоторые атрибуты s/w-программы. Например. докажите, что a + b не будет переполняться, или x/(x-y) не приведет к делению на ноль. Примером статического анализа, использующим этот метод, является Polyspace.
В отношении вашего вопроса: "Являются ли формальные методы широко используемыми в промышленности?" и "Используются ли эти методы для определения критически важного программного обеспечения?"
Ответ: да. Это мнение основано на моем опыте и поддержке инструмента Polyspace для отраслей промышленности, которые полагаются на использование встроенного программного обеспечения для управления критическими для безопасности системами, такими как электронный дроссель в автомобиле, тормозная система для поезда, контроллер реактивного двигателя, инфузионный насос для доставки лекарств, и т.д. Эти отрасли действительно используют эти типы инструментов формальных методов.
Я не верю, что все 100% этих отраслевых сегментов используют эти инструменты, но использование растет. Мое мнение таково, что индустрия аэрокосмической и автомобильной промышленности ведет к тому, что индустрия медицинских устройств быстро наращивает использование.
Polyspace - это (ужасно дорогой, но очень хороший) коммерческий продукт, основанный на проверке программы. Это довольно прагматично, поскольку он масштабируется от "расширенного модульного тестирования, который, вероятно, найдет некоторые ошибки", "следующие три года вашей жизни будут потрачены, показывая, что эти 10 файлов имеют нулевые дефекты".
Он больше основан на отрицательной проверке ( "эта программа не испортит ваш стек" ) вместо положительной проверки ( "эта программа будет делать именно то, что эти 50 страниц уравнений говорят, что это будет" ).
Чтобы добавить к Jorg ответ, здесь interview с Тони Хор. Инструменты Jorg, на мой взгляд, относятся к PREfast и PREfix. Подробнее см. здесь.
Помимо других более процедурных подходов, логика Хоар была в основе Design by Contract, введенной в качестве объектно-ориентированной техники Бертран Мейер в Eiffel (см. статью Майера 1992 года, стр. 4). Хотя дизайн по контракту - это не то же самое, что формальные методы проверки (во-первых, DbC ничего не доказывает до тех пор, пока программное обеспечение не будет выполнено), на мой взгляд это обеспечивает более практическое использование.