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

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

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

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

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

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

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

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

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

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

• Некула, Ли, Кодекс по доказательству , 1996

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• Методы спецификации программного обеспечения . Эта книга предоставляет широкий обзор существующих методов и инструментов. Там вы можете найти основные объяснения и примеры Z, SDL, TLA +, сетей Петри, Coq и т. Д.
• Если вы считаете, что TLA + соответствует вашим потребностям, я очень рекомендую книгу « Спецификация систем» . Вы можете получить книгу бесплатно, и она содержит примеры для игры :).
• Недавно я прочитал несколько связанных статей, которые дают две различные точки зрения на состояние современных формальных методов: случай формальных методов и формально проверенная математика .

Удачи!

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

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

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

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

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

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

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

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

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

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