Как мы можем знать, что формальные методы работают?

Важной целью формальных методов является доказательство правильности систем, либо автоматизированными, либо управляемыми человеком средствами. Тем не менее, кажется, что даже если вы можете предоставить подтверждение правильности, вы НЕ МОЖЕТЕ гарантировать, что система не выйдет из строя. Например:

• Спецификация может некорректно моделировать систему, или производственная система может быть слишком сложной для моделирования, или система может иметь недостатки по своей природе из-за противоречивых требований. Какие методы известны для проверки, имеет ли спецификация какой-либо смысл?
• Процесс доказательства тоже может быть ошибочным! Кто знает, что эти правила вывода являются правильными и законными? Кроме того, доказательства могут быть очень большими, и как мы узнаем, что они не содержат ошибок? В этом суть критики де Милло, Липтона и Перлиса «Социальные процессы и доказательства теорем и программ». Как современные формальные методы исследователи реагируют на эту критику?
• Во время выполнения существует много недетерминированных событий и факторов, которые могут серьезно повлиять на систему. Например, космические лучи могут изменять ОЗУ непредсказуемым образом, и в целом у нас нет никаких гарантий, что аппаратное обеспечение не пострадает от византийских ошибок, которые, как доказал Лампорт, очень трудно противостоять. Таким образом, правильность статической системы не гарантирует, что система не выйдет из строя! Известны ли какие-либо методы, позволяющие объяснить ошибочность реального оборудования?
• В настоящее время тестирование является наиболее важным инструментом для определения того, что программное обеспечение работает. Кажется, это должен быть дополнительный инструмент с формальными методами. Тем не менее, я в основном вижу исследования, которые либо сосредоточены на формальных методах или тестировании. Что известно об объединении двух?

Относительно 4: Есть много работы, объединяющей формальные методы и тестирование. Погуглив «формальные методы тестирования», обнаруживается довольно большой объем работы. Хотя существует много разных целей такой работы, одна из ключевых целей состоит в создании более эффективных наборов тестов. Этот доклад дает хорошее введение, основанное на проверке модели.

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

Относительно пункта 3: Была проделана определенная работа по проверке систем в настройках, где ошибки смоделированы явно, в том числе « Неисправная логика: рассуждения об отказоустойчивых программах». Мэтью Меола и Дэвид Уокер. Европейский симпозиум по программированию, 2010 г. Работа по проверке вероятностной модели и вероятностной проверке, безусловно, также в некоторой степени решает проблему неисправностей.

Ваши очки в порядке:

• Правильность всех спецификаций в конечном итоге субъективна: они воспринимаются как правильное решение проблемы в соответствии с их пользователями, или нет. От этого не уйдет разработка программного обеспечения, и ни у одного метода нет серебряной пули для этого.
• Много работы уходит на то, чтобы доказать, что процесс верен в отношении своих предположений. Обычно есть информация, доступная экспертам для проверки этих правил. Любая человеческая деятельность подвержена ошибкам, но очень формализованные системы, использующие хорошо изученные подходы, гораздо менее подвержены ошибкам, чем почти все другие человеческие процессы.
• В какой-то момент любая система имеет режим отказа за пределами этой системы. Вам все еще лучше устранить все предсказуемые источники ошибок, даже если вы оставите некоторые непредсказуемые источники неучтенными.
• Тестирование и проверка могут легко сосуществовать. Тестирование является менее конкретным, более специальным процессом, поэтому вы можете найти менее формальную работу над ним. Но вас может заинтересовать такой инструмент, как QuickCheck, который дополняет тестами доказательства, предлагаемые системой типов Haskell.

Формальные методы уже продемонстрировали свою эффективность. Без них нам не удалось бы справиться со сложностью проектирования современных цифровых систем (микропроцессоров).

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

За исключением очевидных различий между программным обеспечением и инженерными физическими системами (например, мостами, где можно добавить факторы безопасности), они играют роль инженерной математики в CS. Однако использование FM всегда зависит от выгоды / стоимости. Нечеткое тестирование окупается в таких компаниях, как Microsoft (Google SAGE на одном слайде).

Даже в микро есть подсистемы (например, микропроцессорные конвейеры), где FV не оказал такого же влияния, как в других местах (например, FPU, где обычное тестирование вообще не проводилось во многих случаях, когда формальная символическая оценка траектории доказала отсутствие ошибок : Kaivola et al. CAV'09).

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

Относительно 2: если система формализована в помощнике по проверке (например, Twelf или Agda или Coq), и свойства обоснованности и полноты проверены, и доказательства сделаны в этой кодировке, это не проблема. Возможно, вы формализовали систему, которая не описывает то, что вы хотели, но, по крайней мере, у вас не будет неправильных доказательств или сломанной системы, в которой вы рассуждаете.

Тем не менее, кажется, что даже если вы можете предоставить подтверждение правильности, вы НЕ МОЖЕТЕ гарантировать, что система не выйдет из строя.

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

Какие методы известны для проверки, имеет ли спецификация какой-либо смысл?

Возможно, вас заинтересуют инструменты проверки моделей для спецификаций формальных систем .

Процесс доказательства тоже может быть ошибочным! Кто знает, что эти правила вывода являются правильными и законными?

Я думаю (из-за теоремы Гёделя о неполноте), что система правил вывода непротиворечива, обязательно обращается к еще более мощному набору правил вывода.

Кроме того, доказательства могут быть очень большими, и как мы узнаем, что они не содержат ошибок?

Надеемся, что огромные доказательства проверяются небольшим средством проверки, которое может быть прочитано и понято людьми в разумные сроки. Это иногда называют «критерием де Брюйна». Если вы считаете, что средство проверки не подтвердит неправильное доказательство, вам нужно только проверить средство проверки.

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

Как насчет отказоустойчивого типизированного ассемблера ?

Тем не менее, я в основном вижу исследования, которые либо сосредоточены на формальных методах или тестировании. Что известно об объединении двух?

«Конференция TAP посвящена сближению доказательств и тестов» .

Просто поиск в Google для «доказательств и тестов» имеет несколько хороших результатов выше сгиба.

Какие методы известны для проверки, имеет ли спецификация какой-либо смысл?

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

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

Конечно, есть поле проверки, известное как проверка во время выполнения , вы также можете использовать проверку модели на основе выполнения на реальной системе, работающей в полностью виртуальной среде, в зависимости от конкретного сценария (я внес свой вклад в это с помощью V-DS + APMC ). Тем не менее, это явно серьезная проблема для добавления взаимодействия между системой и средой в процесс проверки.

Тем не менее, я в основном вижу исследования, которые либо сосредоточены на формальных методах или тестировании. Что известно об объединении двух?

Ух ты, сегодня я буду совершенно бесстыдным и снова процитирую себя. Вместе с соавторами мы работаем над совмещением проверки и тестирования моделей, вы можете посмотреть список публикаций бывшего аспиранта нашей группы или выполнить поиск «приблизительной вероятностной проверки модели» или «проверки статистической модели» в любой хорошей поисковой системе (работа сделана Юнес и др., Сен и др. Или я и др. И многие другие).

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