Существуют ли системы или есть программное обеспечение, которое разработано с доказательством правильности его резервного копирования? Или все критические системы разработаны только с агрессивным обзором кода и циклом тестирования?Существуют ли какие-либо гарантии программного обеспечения в критических системах?
Кодирование для приложений высокой целостности, в реальном мире, как правило, включает в себя прыжки через кучу QA обручи. Иногда эти обручи на самом деле имеют какое-то отношение к правильному использованию программного обеспечения.
Медицинское оборудование в США регулируется FDA. Они публикуют свод правил, касающихся «дизайна», который включает в себя всю разработку программного обеспечения. Эти правила в основном соответствуют стандарту ISO 9000 по стероидам. Вы должны иметь кучу документов, которые написаны, отмечены рецензентами, обновлены с комментариями к обзору и подписаны старшим менеджером. Поскольку правила подкреплены законом, FDA хочет увидеть доказательства того, что эти записи не были подделаны, например, написав «ожидаемый результат» теста после того, как вы увидели, какой результат дал тест. Таким образом, вам нужно либо заблокировать полностью защищенную систему CM, либо все это должно быть подписано и датировано на бумаге (включая исходный код). Инспекторы УЛХ имеют настоящие правоприменительные полномочия; если они сочтут нужным, они могут проверить ваш исходный код вооруженным федеральным маршалом. Однако они не являются специалистами по программному обеспечению: их работа заключается не в том, чтобы судить о качестве вашего кода, просто чтобы убедиться, что вы выполнили все правила.
Авиационная промышленность должна следовать за DO-178B, которая также является ISO-9000 на стероидах. Вы должны создавать множество документов и демонстрировать прослеживаемость между ними. Я не знаю, поддерживает ли FAA тот же подход к QA, что и FDA.
Проблема в том, что никто не знает, как производить программное обеспечение, которое делает то, что он должен. Таким образом, вместо этого у нас есть своего рода подход к грузовым кулинарам, где мы производим много документации в надежде, что это наполнит наше программное обеспечение качеством. Справедливо, что качественное программное обеспечение, как правило, имеет четкие требования и простую логическую архитектуру, но это не означает, что создание документа требований или «документа архитектуры» улучшит ситуацию.
Данные свидетельствуют о том, что фактором, оказывающим наибольшее влияние на правильность кода, является команда, которая его создала. Однако вы не можете написать юридическое ограничение для команды. Поэтому вместо этого люди, обладающие мандатом качества, вынуждены писать ограничения на процесс, в неопределенной надежде, что это будет иметь аналогичный эффект.
См. They Write The Right Stuff для интересного изучения того, как они разрабатывают программное обеспечение для космического челнока.
Выдержки:
Но как много работы программного обеспечения делает не то, что делает его замечательным. Что отличает , насколько хорошо работает программное обеспечение . Это программное обеспечение никогда не заканчивается . Это никогда не должно быть перезагружено. Это программное обеспечение без ошибок. Идеально, так же прекрасно, как человеческие существ. Рассмотрим эти статистические данные : последние три версии программы - каждая 420 000 строк длиной - всего одна ошибка. Последние версии этого программного обеспечения имели из 17 ошибок. Коммерческие программы эквивалентной сложности имели бы 5 000 ошибок.
Чтобы быть справедливым, следует, вероятно, также процитировать строку, в которой говорится, что это, вероятно, самая дорогая компания по разработке программного обеспечения нации :) Но определенно интересно читать. – ShiDoiSi
@ vs - Возможно, это само собой разумеется, когда вы говорите о правительственных агентствах;) – Jay
Заканчивать эту колонку Уолтера Брайта, в основном, утверждая, что это практически невозможно, чтобы написать совершенное программное обеспечение, так the best thing to do is fail fast and build in redundancy.
хорошее чтение. Спасибо. – fuentesjr
Да, существуют системы, разработанные с доказательством правильности. Praxis делает это в течение многих лет, используя SPARK Ada, и теперь мы делаем это с C и Escher C Verifier. Это не панацея, потому что, хотя мы доказываем, что код удовлетворяет спецификации, обычно трудно быть уверенным, что спецификация подходит для соответствующего приложения.
Одним из препятствий для более широкого применения формальных доказательств является то, что существующий стандарт авиационного программного обеспечения DO-178B не является дружественным формальным методам. Предполагается, что в настоящее время выполняется переписывание DO-178C.
Проблема с доказательством правильности заключается в том, что вы можете доказать это только в отношении формальной спецификации. Однако, как вы говорите, вы не можете доказать, что формальная спецификация верна, вы можете только просмотреть ее. Это означает, что вам нужны рецензенты, которые могут 1: понять формальную спецификацию, 2: подумать, как программисты, и 3: понять проблемную область достаточно хорошо, чтобы выявить несоответствия. Пересечение всех 3 множеств, как правило, пусто. –
отличная почта. Спасибо. – fuentesjr