И. Соммервилл - Инженерия программного обеспечения (1133538), страница 110
Текст из файла (страница 110)
Однако природа критических систем такова, что, как правило, в дополнение к обычному анализу и тестированию системы необходимы еще процессы доказательства ее надежности. Зго требуется по двум причинам. 1. Цена отказа критюиских пестам. В критических системах стоимость отказа и его последствия потенциально значительно выше, чем в других системах.
Поэтому эко. комически выгоднее выделить достаточно средств на верификацию и аттестацию критических систем, чтобы обнаружить и исправить возможные ошибки еще в процессе разработки системы. 2. Аттестация свойств функциональной надежности. Заказчики критических систем должны быть уверены в том, что система соответствует определенным показателям функциональной надежности (работоспособность, безотказность, безопасность и защищенность). Для оценки этих свойств требуется специальный процесс верификации и аттестации, который рассматриваетсл далее в главе, По указанным выше причинам стоимость процесса верификации и аттестации для критических систем обычно значительно выше, чем для других систем.
Нет ничего удивительного в том, что на верификацию и аттестацию критических систем приходится более 50% от полной стоимости разработки. Конечно, такие расходы оправдывают себя, если удается избежать дорогостоящих отказов системы. Например, в 1996 году вследствие отказа программного обеспечения, установленного на ракете Апапе 5, потеряно несколько спутников, стоимостью сотни миллионов долларов. В процессе азтестации критических систем кроме непосредственной аттестации систем должна также проводиться аттестация процессов, используемых при ее разработке. Как отмечается в главах 8 и 24, на качество системы влияет качество процессов разработки ПО.
Поэтому при создании систем с высокими требованиями надежности необходимо прежде всего обеспечить четкое соблюдение стандартов процесса разработки. Такая аттестация процесса разработки является неотьемлемой частью стандартов управления качеством 13О 9000', кратко рассмотренных в главе 24. Согласно этим стандартам, на все используемые процессы разработки и связанные с ними процессы, обеспечивающие их соблюдение, должна быть документация. Как правило, требуется иметь систему сертификации полноты и завершенности процессов разработки и проверки качества промежуточных и конечного продуктов, например в виде специальных форм, Стандарты 1ЯО 9000 определяют, какие промежугочные продукты процесса должны производиться и контролироваться и кто отвечает за нх производство и проверку.
Использование форм, которые описывают процесс анализа системных отказов, рассматривается в разделе 21.3.3. 21.1. Формальные методы и критические системы В орщнизациях, занимающихся разработкой критических систем, все еще продолжаются дебаты о роли формальных методов в процессе разработки систем с критическими требовя е Международное оргппиепцне но емандариюпцио Ггпйпипдоно! Беаадапе Оеданитна - БО), лаитеь аееоцапцией нпцнонапи|ип орттппций по пппндарпаппцив, одеспечивпет рперпвотьу и поддержку меогдународниа емапдпрнов е сфере воммуниппций и ойина информпцпей. -Прим.
род. 21. Аттестация критических систем 429 пнями к безопасности и надежности. Использование формальной математической спецификации и связанной с ней верификации лвляется стандартом в Великобритании для систем, критических по обеспечению безопасности [2411, Однако большинспю разработчиков критических систем считают форьшльные методы неэффективными и уверены, что нх ис. пользование может привести даже к снижению (а не повышению) надежности системы.
Формальные методы применяются на двух уровнях разработки критических систем. 1. Разработка формальной спецификации системы и математический анализ противоречий в формальной спецификации. Как отмечалось в главе 9, данная методика эффективно выявляет ошибки и упущения в системной спецификации. В этой главе использование формального подхода рассматривается на примере спецификации части системы, отвечающей за инъекции инсулина, которая описана в главе 16.
2. Формальная верификация для проверки соответствия программного кода системной спецификации. Для формальной верификации нужна формальная спецификация. Формальная верификация эффективно выявляет ошибки, сделанные на этапах программирования и проектирования системы.
Аргумент за использование формальной спецификации и связанной с ней верифика. ции программ состоит в том, что во время формального специфицирования выполняется тщательный и подробный анализ требований. Зтот анализ позволяет выявить потенциальные противоречия и упущения, которые в противном случае мокнут оказаться незаме. ченными вплоть до появления рабочей версии системы. Формальная верификация демонстрирует соответствие разрабатываемой программы спецификации. Против использования формальной спецификации выдвигается следующий аргумент: ее использование требует специальной системы нотаций, пользоваться которой может только специально обученный персонал.
Используемая лля формальной спецификации система нотаций может оказаться непонятной специалистам в той предметной области, где будет эксплуатироваться система. Поэтому проблемы согласования требований необходимо решить с помощью специальных формальных методов. В этой ситуации разработ. чики ПО не могут распознать потенциальные проблемы требований, поскольку не явля. ю'гся специалистами в предметной области приложения; специалисты в области приложения также ие мог1т обнаружить проблемы, так как они не понимают спецификацию. Поэтому, песлютря на то что спецификация может быть математически корректной, свойства системы, которые требуются а действительности, в спецификации могуг быть не определены.
Верификация нетривиальной системы ПО занимает много времени и требует применения специальных средств и методов. например методов доказательства теорем и математического оценивания. Поэтому верификация является чрезвычайно дорогостоящим процессом, причем с увеличением размеров системы расходы на формальную верификацию возрастают нелинейно. Именно поэтому многие считают формальную верификацию экономически не выгодной.
Такого же уровня надежности или безопасности можно достигнуть с меньшими затратами, используя такие методы верификации, как инспектирование и тестирование системы. Такое утверждение пока невозможно ин подтвердить, нн опровергнугь, поэтому при разработке некоторых систем все равно применяются фор. мальные методы. Иногда говорят, что использование формальных методов в процессе разработки сис. темы позволяет создать более надежные и безотказные системы.
Несомненно, формальная спецификация содержит меньше противоречий, которые должен разрешать разра- 430 Часть Ч. Верификация и аттестация ботчик. Однако формальиал спецификация и доказательство не гарантируют, что система окажется надежной на практике, чему есть несколько причин. 1. Спввификлчил может нв вгврвжлэгв рвпвьимл глрвбввлхий пввыввамвлвй аиэмим. Установлено, что многие ошибки являются следствием ошибок и упущений в системной спецификации, не обнаруженных при создании формальной спецификации [2261. Кроме того, пользователям часто непонятны формальные нотации. поэтому они пе мо~ут непосредственно проанализировать формальную спецификацию и обнаружить в ней ошибки и упущения.
2. В двказаэмлыэмах мввуэг дьшв выибхи. Доказательства больших и сложных программ, как правило, также большие и сложные, поэтому часто содержат ошибки. 3. При двквзвэмвьгэмв лрименявэил неверный кглбввя ислввьвввлния. Если система используется неверно, то доказательство также может быть неверным. Несмотря на все эти недостатки, я полагаю, что формальные методы играют важную роль в разработке падежного и безопасного ПО. Формальные спецификации весьма эффективно выявляют проблемы требований, которые являются наиболее распространенными ошибкаии. Формальная верификация повышает уровень надежности наиболее критических компонентов этих систем.
Формальные методы получают все большее распро. страиеиие, поскольку постояипо растет спрос иа надежные системы и увеличивается число специалистов. знакомых с этими методами. Но должно пройти еще немало времени, чтобы использование формальных методов в процессе разработки критических систем стало обычным делом. 21.2.
Аттестация безотказности Как уже отмечалось в главе 17, для специфицирования требований безотказности систем разработано множество различных числовых показателей. Чтобы быть увереииым. что система соответствует требованиям, необходимо измерить ее показатели безотказности, учитывая работу типичного пользователя. Процесс измерения показателей безотказности системы представлен иа рис. 21.1; ои состоит из четырех этапов. 1.
На этапе определения операционного профиля изучаются аналогичные существующие системы. Операционный профиль задает разные классы входных данных системы и вероятность их ввода в нормальных режимах ее работы. Этот этап рас. сматривается в следующем разделе. 2. Подбирается ииожество тестовых данных (иногда с помощью генератора тестовых даииых), соответствующих операционному профилю.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
