Как создать критически важное программное обеспечение?

15

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

Однако, после изучения формальных методов (особенно LTL, CTL и их братьев и сестер), я чувствую, что их можно использовать только для проверки правильности спецификации (безопасность, жизнеспособность, справедливость и т. Д.).

Но тогда как проверить, что программное обеспечение (не только спецификация) действительно правильно?

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

fajrian
источник
2
Что вы подразумеваете под «... что программное обеспечение действительно правильно ...» ? Что из следующего 2 вы имеете в виду: 1) Программное обеспечение соответствует спецификации. 2) Конкретные блоки кода соответствуют некоторому заданному свойству или некоторым отношениям ввода-вывода.
Джорджио Камерани,
@GiorgioCamerani: Первый
фейрианский
2
Правильность программы обычно означает, что (1) она соответствует спецификации и (2) она никогда не падает. Точка (1) на самом деле является утверждением о паре (программе, спецификации), а не о самой программе. Еще одним осложнением является то, что «программа» обычно является сокращением для «модели программы», поскольку сами программы слишком сложны или не имеют точной семантики. Учитывая это, я думаю , что вы спрашиваете о разрыве между программой и ее моделью, но я не совсем уверен.
Раду ГРИГОРЕ
@RaduGRIGore: На самом деле я не понимаю, что такое «модель». Но я думаю, что вы обращаетесь к моему вопросу довольно близко По сути, меня интересует разрыв между спецификацией и исходным кодом программы. Много глупостей может случиться, когда программисты (как я) реализуют спецификацию.
Fajrian
1
@fajrian: Я подозреваю, что вы говорите «спецификация» для того, что я бы назвал «моделью». Существуют инструменты, которые работают с программами, написанными на таких языках, как C или Java, или даже с машинным кодом. (Тем не менее, это все еще модель, так как они должны предполагать некоторую семантику, которая должна , но не может соответствовать тому, что делает компилятор / процессор.)
Radu GRIGore

Ответы:

11

Вопрос довольно широкий. Чтобы ответить на него в разумном месте, я сделаю много упрощений.

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

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

  • (маленький шаг) операционная семантика : Это очень похоже на определение языка программирования путем написания для него интерпретатора. Для этого вам нужно сказать, что такое состояние , и на него влияет каждое утверждение на языке. (Вы можете спросить, на каком языке вы пишете переводчик, но я буду притворяться, что вы нет.)
  • аксиоматическая семантика : здесь каждый тип оператора поставляется со схемой аксиомы. Таким образом, грубо говоря, всякий раз, когда используется конкретное утверждение этого типа, оно означает возможность использования определенных аксиом. Например, присваивание поставляется со схемой { P [ x / e ] }Иксзнак равное ; конкретное назначение x : = x + 1 идет с аксиомой { x + 1 = 1 }{п[Икс/е]}Иксзнак равное{п}Иксзнак равноИкс+1 если мы создаем схему с помощью P = ( x = 1 ) .{Икс+1знак равно1}Иксзнак равноИкс+1{Иксзнак равно1}пзнак равно(Иксзнак равно1)

(Есть и другие. Я чувствую себя особенно плохо из-за того, что опускаю денотационную семантику, но этот ответ уже длинный.) Машинный код плюс операционная семантика довольно близки к тому, что большинство людей назвали бы «настоящей программой». Вот оригинальный документ, в котором используется операционная семантика для подмножества машинного кода DEC Alpha:

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

Таким образом, я мог бы подумать о трех причинах, которые привели к вашему вопросу:

  1. Вы видели только семантику высокого уровня, которая не похожа на то, что вы называете программой, и вам интересно, есть ли она низкоуровневая. Ответ - да.
  2. Вы удивляетесь, как вы доказываете, что модель соответствует реальности. Как в физике, вы не делаете. Вы просто придумываете лучшие модели и сравниваете их с реальностью.
  3. Вы не видели различий между синтаксисом и семантикой, а также различными способами присвоения значений программам. Два предыдущих вопроса содержат список некоторых книг.

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

Раду ГРИГОРЕ
источник
8

Одним из подходов к сокращению разрыва между программой и ее спецификацией является использование языка с формальной семантикой. Интересным примером здесь будет Эстерель . Загляните на веб-страницу Жерара Берри, где вы найдете интересные рассказы о его работе по внедрению формальных методов в реальный мир. http://www-sop.inria.fr/members/Gerard.Berry/

ps был на аэробусе? Вы летали с формальными методами!

Росс Дункан
источник
1
любая ссылка на то, как airbus использует формальные методы, будет полезна. (понимаю, что это, возможно, запатентованная информация.)
vzn
@RossDuncan Я нашел эту веб-страницу после перехода на веб-страницу Берри и нескольких поисков. Это формальные методы, которые Airbus использовал, на которые вы ссылались?
scaaahu
У меня нет никакой внутренней информации относительно использования Esterel Airbus; мой комментарий просто повторяет замечание, которое Берри сделала во время лекции. Однако эта страница трубит об успешном использовании продукта SCADE с Airbus. Если вы посмотрите на историю Esterel, она была принята Dassault довольно рано. Google твой друг.
Росс Дункан
2
Airbus также использует astree.ens.fr
Radu GRIGore
7

Наука о создании надежного программного обеспечения в «реальном мире» все еще находится в стадии разработки и в некоторой степени граничит с неотъемлемым культурным или антропологическим исследованием, потому что компьютеры и программное обеспечение не «вызывают» ошибки, а люди! Этот ответ будет сфокусирован на общих подходах Q / A, в которых формальная проверка программного обеспечения может рассматриваться как один из элементов.

Замечательное наблюдение заключается в том, что часто программное обеспечение, которое является «достаточно хорошим», но все же «глючным», может часто превосходить лучшее тестируемое, но менее функциональное программное обеспечение на рынке. другими словами, рынок не всегда делает ставку на качество программного обеспечения, и современные методы разработки программного обеспечения, которые не всегда подчеркивают качество, в некоторой степени отражают это. Кроме того, качество часто может привести к значительным расходам на конечный продукт. с этими оговорками, вот некоторые из основ:

  • резервированные / отказоустойчивые системы. это широкая область изучения. Отказоустойчивость и избыточность могут быть встроены во многие уровни системы. например, маршрутизатор, сервер, дисковод и так далее.

  • тестирование . все типы - модульное тестирование, интеграционное тестирование, приемочное тестирование пользователя, регрессионное тестирование и т. д.

  • В настоящее время автоматизированное тестирование с помощью наборов тестов, которые можно запускать без присмотра, более развито / важно. Испытательные комплекты часто связаны с инструментом сборки.

  • важной концепцией в тестировании является покрытие кода . т.е. какой код выполняется тестом. тест не может найти ошибку в коде, которая не «затронута» тестом.

  • Другой ключевой концепцией в тестировании является использование тестового кода, к которому нелегко получить прямой доступ.

  • Тесты должны осуществлять все уровни программного обеспечения. если программное обеспечение хорошо модульно, это не сложно. тесты более высокого уровня должны глубоко проникать в код. тесты, которые выполняют большие объемы кода с небольшими настройками теста, увеличивают «тестовый рычаг» .

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

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

  • можно увлечься тестированием! Существует проблема как с небольшим, так и слишком большим количеством испытаний. есть "сладкое пятно". программное обеспечение не может быть успешно встроено ни в одну из крайностей.

  • Используйте все основные инструменты наиболее эффективным способом. отладчики, профилировщики кода, инструменты покрытия тестового кода, система отслеживания дефектов и т. д.! не обязательно совершать исправления, но отслеживать даже самые маленькие дефекты в программном обеспечении для отслеживания.

  • осторожное использование SCM, управление исходным кодом и методы ветвления важны для предотвращения регрессий, изоляции и прогрессирования исправлений и т. д.

  • Программирование N-версии : практика, часто используемая для разработки критически важного программного обеспечения. Предпосылкой этой практики является то, что N независимо разработанных программ вряд ли будут иметь одинаковую общую ошибку / ошибку. Это было подвергнуто критике в нескольких статьях . NVP , однако, является практикой, а не теоретической концепцией.

Я полагаю, что физик Фейнман имеет некоторые сведения о методе, который НАСА использовало для обеспечения надежности систем космических челноков, в своей книге «Какое тебе дело до того, что думают другие люди»? - он сказал, что у них было две команды, скажем, команда A и команда B. команда A создала программное обеспечение. команда B приняла состязательный подход к команде A и попыталась взломать программное обеспечение.

это помогает, если команда B имеет хороший опыт разработки программного обеспечения, то есть они сами могут писать жгуты кода / программные тесты и так далее. в этом случае у команды B был почти такой же уровень ресурсов, как у команды A. С другой стороны, этот подход дорог, потому что он может почти удвоить стоимость создания программного обеспечения. более типично, есть меньшая команда QA по сравнению с командой разработчиков.

ВЗН
источник
8
Кто-то должен проверить вашу ОС на предмет корректности в отношении спецификации, согласно которой нажатие клавиши Shift и буквы создает заглавную букву.
Андрей Бауэр
1
Приложение: ограничения по графику могут повлиять на качество. см. также треугольник MGT проекта, состоящий из объема, стоимости, графика и качества, «области», на которую влияют все 3. см. также «Почему ИТ-индустрия не может выполнять крупные, безошибочные проекты быстро, как в других отраслях?» , Я не добавлял элемент N-версии сам [другой ответ покрывал его], но учтите, что Фейнман упомянул, что НАСА использовало его также в дизайне космического челнока.
августа
1
Другим интересным примером является марсоход, который имеет большой объем кода, большая часть которого генерируется автоматически. в этом случае до полевых испытаний проверялось большинство программного обеспечения, и оно использовалось повторно.
vzn
6

Старый подход (но он все еще используется в некоторых приложениях) - это программирование N-версии

Из Википедии:

N-версия программирования ( NVP ), также известная как многоверсионное программирование , представляет собой метод или процесс в программной инженерии, где несколько функционально эквивалентных программ независимо генерируются из одних и тех же исходных спецификаций. Концепция программирования N-версии была введена в 1977 году Лимингом Ченом и Альгирдасом Авизиенисом с главной гипотезой о том, что «независимость усилий по программированию значительно снизит вероятность идентичных сбоев программного обеспечения, возникающих в двух или более версиях программы». Цель NVP заключается в повышении надежности работы программного обеспечения за счет повышения отказоустойчивости или избыточности.
....

См. Например: « Проблемы при повреждении здания - терпимая система управления полетом для гражданского самолета »

Марцио де Биаси
источник
Стоит отметить, что n-версия программирования не работает . Фундаментальное предположение, а именно, что ошибки в повторных испытаниях процесса разработки программного обеспечения независимы, совершенно неверно . Эта идея теоретически не имеет смысла (сложный для реализации алгоритм не станет волшебно проще для второй независимой команды), и он также опровергнут экспериментально: эксперимент Джона Найта и Нэнси Левесон, показывающий, что предположение о независимости не является статистически обоснованным является одной из самых известных статей в области разработки программного обеспечения.
Нил Кришнасвами
@NeelKrishnaswami: Я согласен! Тем не менее, я думаю (но я не эксперт), что не работает, следует заменить на него, не улучшая надежность, как это должно быть по сравнению с другими подходами . Ссылаясь на K & L: « ... Мы никогда не предлагали использовать наш результат в качестве основы для принятия решения об эффективности программирования N-версии. Мы просто предполагали, что осторожность будет уместной ... ». Я думаю, что дискуссия о том, насколько подход NVP может быть полезен для проектирования критических систем, все еще открыта (см. Недавнюю работу Хури и др.)
Марцио Де Биаси
4

fajrian, этот вопрос, который вы задали, охватывает две самые большие проблемы в исследованиях инженера-программиста: соответствие спецификации и модели, а также модели и кода. Моделируйте здесь представление о том, что будет делать система, или как это будет сделано, есть много уровней для моделирования системы.

Итак, есть люди, которые пытаются найти лучший ответ на ваш вопрос. Потому что очень сложно проверить правильность программного обеспечения на основе модели, например, используя формальные методы. Я знаю, что JML - это способ сделать это, но я не знаю границ его использования.

Чтобы подвести итог, как трудно проверить правильность кода, люди пытаются смешать формальные методы и тестирование, например, автоматически создавая тестирование из спецификаций. Одним из примеров систем реального времени является TIOSTS , основанный на событиях входа / выхода по времени.

Только тестирование не является формальным методическим подходом, оно повышает надежность, но не проверяет правильность.


источник
3

Два или три года назад я начал изучать формальные методы, применяемые к программному обеспечению. Это был квест, движимый любопытством и ощущением, что мне нужно было изучать инструменты и методы программирования с более длительными промежутками времени. Хотя я мечтал о Серебряной Пуле , я действительно думал, что нет ответа на вопрос: «Как я могу написать правильную программу?».

На данном этапе квеста после попытки использования некоторых инструментов (Z, B, VHDL и Estelle) я использую TLA + . Это вариант временной логики с программными инструментами для проверки моделей и механических доказательств. Я думаю, что я выбрал этот подход, потому что Л. Лэмпорт был за этим, синтаксис был прост, было много примеров, было сообщество, заботящееся об этом, и язык и инструменты были довольно хорошо задокументированы.

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

Короче говоря, я думаю, что следующая метафора (от Лампорта) действительно мощная: «Ожидаете ли вы, что дом будет автоматически построен по проекту? Купите ли вы дом, который еще не построен, и у него нет проекта?» ,

Во время этого квеста я нашел следующие полезные ресурсы:

Удачи!

marcmagransdeabril
источник
1

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

Как создать критически важное программное обеспечение?

Существуют инструменты, которые автоматически анализируют ваш код на наличие ошибок (нарушений спецификации или «типичных ошибок»). Насколько мне известно, эти методы в основном основаны на статическом анализе и не имеют непосредственного отношения к упомянутым вами теориям (LTL / CTL / ...), но они обнаруживают ошибки в реальном коде, и это уже возможно с практической точки зрения. Посмотреть, использовать такие инструменты в промышленных проектах. Лично я не использовал многие из них, но кажется, что эти инструменты начинают приниматься практикующими. Для дальнейшего чтения я могу порекомендовать следующую статью в блоге:

http://www.altdevblogaday.com/2011/12/24/static-code-analysis/

Markus
источник
Пример реализации с использованием Java, Apache
findbugs
0

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

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

Подробнее читайте в этой обзорной статье. Сертифицирующие алгоритмы Макконнелла Р.М. и Мелхорна К. и Нахера С. и Швейцера П.

Пратик Деогхаре
источник
В 1998 году Пнуэли, Зигель и Сингерман описали эту идею, примененную к компиляторам, под названием валидации перевода. Компиляторы по своей природе более высокого порядка (входные данные - программа, выходные данные - программа), поэтому их трудно проверить. Но есть сумасшедшие люди, такие как X. Leroy, которые все равно разрабатывают проверенные компиляторы. (Сумасшедший в лучшем смысле этого слова!)
Раду GRIGore
-2

Но тогда как проверить, что программное обеспечение (не только спецификация) действительно правильно?

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

Теоретически, если ваши модульные тесты имеют 100% охват кода (т. Е. Тестируется каждый метод в вашем коде), ваше программное обеспечение должно быть корректным, если сами тесты являются точными и реалистичными.

gillesv
источник
5
Для любой достаточно сложной программы покрытие кода (путем тестирования) не может гарантировать корректность. Вы должны были бы покрыть все возможные казни; все строки кода не достаточно.
Раду ГРИГОРЕ
1
Покрытие кода - слишком расплывчатая концепция. Мы различаем, например, покрытие метода, покрытие оператора, покрытие филиала, покрытие пути и так далее. Как указывает Раду, для нетривиальных программ тестирование часто приводит к комбинаторным взрывам. Тем не менее, программное обеспечение для аэронавтики имеет довольно большой послужной список, и его правильность часто основывается на всесторонних испытаниях.
Мартин Бергер
Если вы имеете в виду тестирование такими инструментами, как JUnit, этот тип стандартного автоматического тестирования не может охватывать все случаи (если программа не очень мала). Для типичного применения этого вида тестирования обычно достаточно. Но для критически важных приложений я не знаю, достаточно ли этого (или нет).
фейрианский
2
@vzn: По моему опыту, между учеными и, соответственно, практиками есть замечательное согласие между тем, что считается ошибкой. Кроме того, могу поспорить, что большинство моих (бывших) коллег из отрасли согласятся с тем, что «тестируется каждый метод в вашем коде», что звучит не очень обнадеживающе. (И нет, я не понизил голос. Я почти никогда не делаю.)
Раду ГРИГОР
1
@vzn: я сказал, что ты сказал иначе? Я просто пытался объяснить, почему я считаю, что другие не голосуют против этого ответа. В настоящее время я не могу ответить на этот вопрос, потому что я не понимаю его.
Раду ГРИГОРЕ