И. Соммервилл - Инженерия программного обеспечения (1133538), страница 112
Текст из файла (страница 112)
Верификация и атгестация ошибки повышает бсзотказность на некоторую постоянную величину. Однако нс все ояшбки равновероятны, Исправление наиболее часто проявляющихся ошибок приводит к возрастанию безотказности на бальшую величину, чем исправлспис редко проявллю. шихся ошибок. Поэтому возрастание безотказности на каждом врсменнпм шаге нс будет постоянным.
В более поздних моделях возрастания безотказности, например предложенных в рабате [222), для решения этой проблемы вводится случайный элсмснт, который позволлст более точно оценить рост безотказности после исправлений ошибок в системе, Таким образом, нри каждом исправлении ошибки безотказность возрастает пс равномерно, а на некоторую всличину, зависящую от случайного параметра (рис. 21.4). 3 И 6 2 Я Н 12 Э 14 6 Врмм Рис. 264, й(адель ввзрппптшя безпэекпгквпни нп основе Яккции еп случайным шпица В модсли, предложенной в [222), возможно уменьшение безотказности, если исправление ошибок вносит в ПО дополнитсльныс ошибки.
Данная модель также демонстрирует тот факт, что по мере исправлсния ошибок скорость возрастания безотказности в среднем понижается. Причина такого понижения обусловлена тем, что в процсссс тестирования пзиболсс вероятные ошибки обнаруживаются самыми первыми, прн этом исправлс. и ив паиболсс вероятных ошибок вносит наибольший вклад в возрастание бсзотказности. Описанныс вышс модели явллются дискретными и основаны на пошаговом возрастании безотказности. Перед тестированием новая всрсия ПО с исправленными ошибками должна иметь более низкую интенсивность отказов, чем предыдущая.
Но для того, чтобы колнчсствснно оценить бсзоткаэпость системы после заданного количества тестирований, нужны математические модели. Множество таких моделей, адаптированных для разных предметных областей прсдставлсно в работах [2, 246, 26ь). Проще вссто оцснить безотказность, подобрав к измеренным данным известную модель безотказности. Затсм эта модель экстраполнрустся на требующийся уровень безотказности.
Время, за которое можно достичь заданной безотказности, затем лыко опрслслить по графику модели безотказности (рис. 21.6). Тестирование и отладка системы долж. пы продолжаться до момента времени достижснил псобходимого уровня бсзотказностп. 21. Атгестацин критических систем 435 61 ййо Требуемый уровень бэзоплзноотк Проллолэтаэмоо йэаыя Врака достижения требуемой безотказности Рис.
2Е5. Отэгливпккс безотказности Оценка безотказности системы но модслн безотказности имеет два принципиальных преимущества. 1. Планкрозпттиг эмокировлниэ. При составлении графика тсстироааинл можно оценить врсмк. в течение которого завершится тестирование. Если это время оказывастсл больше, чем запланировано в графике разработки системы, длл тестирования необходимо привлечь дополнительные ресурсы. 2. Т1эебовлккл заказчика.
Иногда модель безотказности показывает, что возрастание безотказности идет мсдлснно и длл относительно малого прироста бсзотказносттт трсбустся приложить непропорционально много усилий. В такой ситуации совмс. стно с заказчиком можно пересмотреть требования надсжносттт. В другой ситуации модель можст показать, что необходимый уровень безотказности, ио асей видимости, никогда нс будет достигнут. В этом случае также следует пересмотреть системныс трсбоваиил. Использование моделей возрастания безотказности н их применение иа практике описано в работах [105, 307, 312, 29" 1. 21.3. Гарантии безопасности Получение гарантий безопасности системы и аттестация сс бсзотказности — разные процессы.
Безотказность можно определить количественно с помощью различных число. вых показателей. Безопасность нсльзл достовсрно определить каким-либо количсствснпылт гпособолт н, следовательно, нсвозиожно измерить в ходе тссгироваиил системы. Поэтому аттестация безопасности опрсдсллст уровень надежности системы, который может варьироватьсл от -очень низкого" до "очень высокого". Здесь трсбустсл профсссиональпав оцснка безопасности. Во многих сл> чалх опрсдслснис безопасности частично базирустск на опыте организации, разрабатываюптсй систему. Если в органиэации ужо 456 Часть Ч.
Верификация и аттестация есть предварительно разработанные надежно функционирующие безопасные системы, то разумно предположить, что в данной органиэации будут разработаны подобные безопас. ные системы. С другой стороны. оценка безопасности должна опираться на реэльну»о архитектуру системы, результаты верификации и аттестации, а также на процессы, которые применялись при разработке системы. 21.3.1. Верификация и аттестация Верификация и аттестацил систем, критических по обеспечению безопасности, имеет много общего с тестированием любых систем с высокими требованиями надежности.
Чтобы обнаружить как можно больше системных дефектов, следует применить всестороннее тестирование, а при оценке безотказности системы использовать статистическое тестирование. Однако вследствие чрезвычайно низкой частоты отказов, присущих многим системам. критическим по обеспечению Г>еэопасностн, с помощью статистического тестирования ие всегда удается количественно оценить безотказность системы, поскольку лля этого требустсл провести чрезвычайно большое количество тестов. При оценке безо. пасностн системы эти тесты, используемые сов>»есгно с такими методами тестирования, как инспектирование кода и статические проверки (см.
главу 19), всего лишь дают основание считать систему безопасной. Прн создании систем, критических по обеспечению безопасности, важен всесторонний анализ разрабатываемой системы. Предложено пять типов анализа системы, обязательных для систем с критическими требованиями безопасности [270). 1. Анализ правильности функционированил системы. 2. Анализ возможности изменения и понлтности системной архитектуры. 5.
Анализ соответствия алгоритма обработки и структуры даннык определенному в спецификации поведению системы.' 4. Анализ сагласованн»эсти программного кода, алгоритмов и структур данных. 5. Анализ адекватности тестовых сценариев системным требованиям. Все доказательства безопасности системы строятся на следующем предположении: количество ошибок в системе, которые приводят к аварийным ситуациям, намного меньше общего количества имеющихся в системе ошибок. Обеспечение безопасности должно сосредоточиться на выявлении потенциально опасных ошибок. Если оказывается, что эти ошибки нс пролвляются или проявляются, но ие приводят к серьезным последствиям, то система считается надежной. В следующем разделе обсуждаются основы доказательства безопасности.
21.3.2. Доказательство безопасности Доказательства правильности программ были предложены в качестве методов верифи. кации ПО более 25 лет назад, Однако этн методы используютсл в основном в исследователь. скнх лабораториях. Практические проблемы построения доказательства правильности ПО настолько сложны, что некоторые организации считают использование данных методов в процессе разработки обычных систем неоправданно дорогим. Но, как подчеркивалось в начале главы, для ряда критических приложений экономически выгодно использовать доказательства правильности системы, чем ликвидировать последствия отказов. Несмотря на то что для большинства систем разрабатывать доказательства правильности нерентабельно, иногда возникает необходимость разработать доказательства безопасности, демонстрирующие соответствие данной программы требованиям по обеспече- 21.
Аттестация критических систем 437 нию безопасности. При доказательстве безопасности необязательно доказывать соответствие программы спецификации. Необходимо только показать, что выполнение програм. мы нс приводит к сбоям с опасными последствиями. Наиболее эффективный метод доказательства безопасности системы — доказательство от противного.
В начале доказательства делают предположение, что во время работы программы может возникнуть опасное состояние, определенное в процессе анализа рисков. Затем выполняют систематический анализ кода и доказывают, что предусловия для данного состояния противоречат пес»условиям всск ветвей программы, приводящих к данному состоянию. Если это действительно так, то начальное предположение об опасном состоянии неверно.
Если это же верно для всех других определенных рисков, значит, система безопасна. Рассмотрим для примера код, представленный в листинге 21.1, который является частью реализации системы управления инъекциями инсулина. В код добавлены комментарии, чтобы связать его с деревом отказов, показанным на рис. 17.3.
Листинг 21.1. Программа управления иньекциями инсулина //Вводимая доза инсулина является функцией уровня сахара в крови, //предыдущей суммарной введенной дозы и времени предылущей инъекции сиггепгрозе = сошрцсе1пзц11п () //проверка безопасности: если необходимо, изменяется сцггепгпове //1-й оператор 16 16 (ргечбоцзрове == 0) ( 12(сцггепгпове > 16) сиггепсрове = 16; ) е1зе 12 (сцггепгрове > (ргеу1оиврове * 2) ) сцггепсрове = (ргеубоцврове * 2; //2-й оператор 12 16 (сиггепгрове < шдпбшця»г»ове) сцггепсрове = О» е1зе 12 (сцггепгрове > шахрове) сцггепгрове = шахповег адлппбзсег1пзц11п (сцггепсрове)г Доказательство безопасности для данного кода включает доказательство того, что вводимая доза инсулина никогда не превысит максимальный уровень, отдельно установленный для юзл»доге больного диабетои.
Таким образом, совсем нсобязатсльно доказывать, что система выдает "правильную" дозу, достаточно доказать, что пациенту»»ик»»гд»» нс будет выдана слишком большая доза инсулина. Для построспия доказательства безопасности находим прсдусловис для опасного состояния, в данном случае это условие сцпеп(0озе > п)ах0озе. Затем нсобходимо показать, что все ветви программы приводят к противоречию с данным условислс Если зто лсйствитслыю так, то условис опасного состояния никогда нс будет испнгным, а слсдоватсльно, система безопасна. Доказательство безопасности, подобное представленному на рис. 21.6, намного короче, чем формальная верификация системы. Сначала определяются всс возможныс ветви, которые приводят к потенциально опасному состоянию.