Имеют ли формальные методы вершины программы место в промышленности?

Question

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

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

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

Answer 1

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

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

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

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

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

Answer 2

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

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

Answer 3

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

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

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

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

Answer 4

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

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

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

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

Answer 5

"Используются ли формальные методы в промышленности?"

Да.

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

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

Нет.

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

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

Answer 6

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

Один из подходов заключается в том, чтобы полностью изменить процесс разработки. 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, в приведенном выше списке инструментов, только предостережение основано на логике Hoare (а Frama-C имеет плагин Hoare Logic). Другие полагаются на абстрактную интерпретацию, другую технику с более автоматическим подходом.

Answer 7

Моя область знаний-это использование формальных методов для анализа статического кода, чтобы показать, что программное обеспечение не имеет ошибок времени выполнения. Это реализовано с использованием формального метода методов, известной «абстрактной интерпретации». Техника, по сути, позволяет вам доказать определенные атрибуты программы AS/W. Например, докажите, что A+B не будет переполняться или x/(xy) не приведет к разделению на ноль. Примером статического анализа, который использует этот метод, является Polyspace.

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

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

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

Answer 8

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

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

Answer 9

Добавить в Jorg's отвечать, вот интервью с Тони Хоаром. Инструменты, которые, как я думаю, ссылаются Jorg, предварительные и префикс. Видеть здесь Чтобы получить больше информации.

Answer 10

Помимо других более процедурных подходов, Hoare Logic была на основе Дизайн по контракту, представленная как объектно -ориентированная техника Бертран Мейер в Эйфелеве (Смотрите статью Мейера 1992 года, стр. 4). Хотя дизайн по контракту не то же самое, что формальные методы проверки (с одной стороны, DBC не доказывать что угодно, пока программное обеспечение не будет выполнено), на мой взгляд, оно обеспечивает более практичное использование.