Руководство по гарантии конструирования бортовой электронной аппаратуры КТ-254 (1015618), страница 23
Текст из файла (страница 23)
Верификация условий, относящихся к схемам, компонентам, внутренним функциям,функциональным атрибутам и аномальным поведениям.7. Верификация условий, относящихся к проверенным входным зависимостям и выходнымповедениям.8. Процедуры и результаты верификации.9. Данные трассируемости процедур верификации к условиям верификации безопасностиаппаратуры для специального анализа данных безопасности аппаратуры.3.3.3. Формальные методыТермин «формальные методы» относится к использованию методов логической идискретной математики при спецификации, конструировании и создании компьютерных систем.74Примечание: Материал для данного раздела получен из справочника “Formal MethodsSpecification and Analysis Guidebook for the Verification of Software and Computer Systems, Volume II:A Practitioner’s Companion,” May 1997, NASA-GB-001-97.
Более детальное представлениеформальных методов с иллюстративными примерами дано там.Применение формальных методов подразделяется на две категории - описательную идедуктивную. В описательных методах применяются формальные технические языки, которыеданы для ясного понятного описания требований и других артефактов проекта. Дедуктивныеметоды основаны на дисциплине, которая требует использовать полный перечень всех допущенийи этапов обоснования. Кроме этого каждый этап обоснования должен содержать небольшоеколичество допускаемых правил, представляющих интерес.
Более жесткие формальные методыприменяют эти методы для подтверждения обоснования, используемого для доказательстватребований или других аспектов конструирования или реализации сложной или критичнойсистемы. Целью формальных методов является уменьшение необходимости полагаться наинтуицию человека и его суждения при оценке аргументов. Таким образом, дедуктивныеформальные методы уменьшают приемлемость аргумента до уровня вычисления, что может впринципе, быть проверено с помощью инструмента, заменяя тем самым внутреннююсубъективность процесса рассмотрения на повторяемое применение.Существует несколько областей, в которых применение формальных методов даетдополнительную гарантию процесса конструирования. Хотя формальные методы применяются врамках процесса конструирования, повышение гарантии конструирования может быть достигнутоза счет целевого применения.
Ниже перечисляются некоторые возможности:1. Формальные методы могут применяться на разных этапах жизненного циклаконструирования. Обычно применение формальных методов наиболее эффективно на раннихэтапах жизненного цикла, особенно во время определения требований и конструирования навысоком уровне.2. Формальные методы могут быть применимы ко всему проекту или они могут бытьпредназначены для отдельных компонентов. Анализ FFPA используется для того, чтобыопределить какие тракты функционального отказа необходимо анализировать с помощьюформальных методов. С использованием формальных методов могут эффективно анализироватьсяаппаратная реализация отказоустойчивых функций и протоколов сложных параллельныхвзаимодействий.3. Формальные методы могут применяться для верификации функциональности системыили для установления специфических свойств.
Хотя формальные методы традиционно связаны с“доказательством правильности“, т.е. с гарантией соответствия компонентов функциональнымспецификациям, они также могут применяться только к наиболее важным свойствам. Часто болееважно подтвердить, что конструкция не проявляет нежелательных свойств, а не доказывать, чтоона имеет полную функциональность.Практическое применение формальных методов обычно требует инструментальнойподдержки.
Используемые инструменты должны быть оценены и, если необходимо,квалифицированы, как описано в подразделе 11.4.3.3.3.1. Методология формальных методовПрименение формальных методов начинается с выражения требований, используяформальный язык. Спецификация требований служит важной описательной функцией. Онаобеспечивает базу для документирования, соединения и макетирования поведения и свойствсистемы, используя однозначные указания. Кроме того, спецификация требований служитосновой для вычисления или формального прогнозирования поведения системы. Формальнаямодель компонента, который должен анализироваться, строится с использованием формальногоязыка.
Модель анализируется по отношению к формальному установлению требований, используяправила выбранной формальной логики. Характеристики модели определяются стилемформального анализа, который должен быть выполнен.Уровень детализации в модели компонента определяется целью выбранного формального75способа анализа.
Некоторые подходы приспосабливаются к нахождению ошибокконструирования, которые могут ускользать от испытаний, а другие подходы стараютсягарантировать отсутствие ошибок конструирования определенных классов.1. Обнаружение ошибки. Наиболее общим формальным способом для обнаружения ошибкисчитается проверка модели. В этом случае требования выражаются как формулы во временнойрешаемой логике. Модель компонента - это абстрактный механизм состояния, созданный так,чтобы свойства, которые должны испытываться, сохранялись. Процедура доказательства являетсяавтоматической.
Неудачная попытка доказательства указывает на ошибку конструирования вмоделируемом компоненте. Результат неудачного доказательства это последовательность входныхстимулов, которые специально демонстрируют, как компонент не удовлетворяет установленномутребованию.2. Предотвращение ошибки.
Формальные методы, направленные на предотвращениеошибок, обычно основаны на языке спецификаций и теории обеспечения доказательства. Дляувеличения выразительности могут устанавливаться более сложные требования и создаватьсяболее сложные модели компонента. Однако процедура доказательства может быть толькочастично автоматизированной.
Соответствующий уровень детализации для моделей компонентаможет быть синтезируемым описанием на языке высокого уровня конструирования. В некоторыхслучаях одна и та же модель может применяться как для моделирования, так и для формальногоанализа. Полным доказательством является очевидность того, что компонент логически правиленв отношении к установленным требованиям для анализируемого входного пространства.3.3.3.2. Разрешение вопросов выявленных формальными методамиСуществует три возможных результата дедуктивного формального анализа:1. Если попытка доказательства успешная, проверка завершена.
Уровень гарантииконструирования зависит от правильности применяемых моделей. Например, если модельэлемента аппаратуры соответствует техническому проектированию, доказательство обеспечиваетгарантию функциональной корректности данных всеобъемлющего испытания.2. В некоторых случаях неудачное доказательство приводит к точному контрпримеру, т.е.оно определяет сценарий испытания, который ясно показывает, каким образом проект несоответствует установленным требованиям. Оно может указывать либо на недостатки в проекте,либо на недостатки в требованиях. Такие недостатки могут быть решены соответствующимисправлением проекта, пересмотром требований, оказавшихся физически нереализуемыми, илииспользованием другого метода.
Все контрпримеры должны быть идентифицированы, чтобыподнятые ими вопросы можно было разрешить. Изменения в проекте или требованиях должныбыть направлены обратно в соответствующий процесс.a. После того, как проект или требование были изменены, в связи с недостаткомвыявленным неудавшейся попыткой доказательства, доказательство должно быть предпринятозаново, чтобы подтвердить, что модификация успешно решает выявленную проблему. Этот циклповторяется до тех пор, пока не будет получено успешное доказательство.b. В случаях, когда контрпример считается разрешаемым без изменения проекта илитребований, но средство определяет только один контрпример, т.е. разрешенный контрпример,процесс должен быть модифицирован, так чтобы он мог идентифицировать другие контрпримеры.3.
Наиболее трудным случаем для решения является случай, когда доказательство не можетбыть проверено и контрпример не может быть идентифицирован. Одним из возможных вариантовявляется пересмотр проекта для того, чтобы упростить проверку. В противном случае, проверкаможет быть распределена на составляющие с четким определением примеров, которыерассмотрены доказательством и примеров, когда требования должны быть рассмотрены спомощью других средств. Изменения в проекте и производные требования должны бытьвозвращены обратно в FFPA.3.3.3.3. Данные формальных методовДанные, разработанные при применении формальных методов, включают:761.
Описание подходов используемых специальных формальных методов, описаниекомпонентов или тракта функционального отказа, к которым будут применены формальныеметоды.2. Формальное установление требований.3. Формальные модели компонента.4. Доказательство и достаточно детальный сценарий для создания доказательства,относящийся к моделям компонента, и для формального установления требований, включаякоррекцию в данных трассируемости.5. Идентификацию применяемых инструментов и результатов оценки инструментов.6.
Идентификацию верификационных контрольных примеров и требований, дополненныхили измененных в результате анализа.7. Установление уровня полноты верификации для трактов функционального отказа,достигнутого в анализе. Включается перечень выявленных анализом недостатков, не разрешенныхпри модификации верификационных контрольных примеров или требований, и обоснованиеприемлемости недостатков.77Приложение ССловарь терминовНастоящие определения даны для терминов, используемых в данном документе. Еслитермин не определен в этом приложении, он может быть определен в тексте.Анализ (Analysis) - Процесс математического или любого логического объяснения, которыйведет от установления предпосылок к выводу, касающемуся специальных способностейоборудования или элемента аппаратуры и его адекватности для конкретного применения.Анализ границ конструирования (Design Margin Analysis) - Процесс определяющий, чтосумма воздействия различных границ конструирования компонентов аппаратуры обеспечиваетизделие, которое соответствует или превосходит требования к его характеристиками, а такжетребования к технологичности и обслуживанию.Анализ покрытия (Coverage Analysis) - Процесс определения степени, при которойпредложенный процесс проверки аппаратуры удовлетворяет его цели.Аномальное поведение (Anomalous Behavior) - Поведение, которое несовместимо сустановленными требованиями.Архитектура системы (System Architecture) - Структура аппаратуры и ПО, выбранная дляреализации требований к системе.Базовая версия (Baseline) - определенная и одобренная конфигурация, которая с этогомомента служит основой для дальнейшего конструирования и которая изменяется только приизменении процедур контроля.Безопасность (Safety) - Состояние, при котором величина риска ниже, чем его предельноезначение.
Предельное значение-это верхняя граница приемлемого риска. Он характерен длятехнических процессов или состояний. Риск определяется частотой или вероятностью появления ипредполагаемым наносимым вредом.Верификация (Verification) - Оценка реализации требований для определения дляопределения того, что они могут удовлетвореныВид отказа (Failure Mode) - Характер проявления отказа.Время воздействия (Exposure Time) - Период времени между последним известныммоментом правильного функционирования элемента аппаратуры и известным временем егоследующего правильного функционирования.Выпуск (Release) - Акт официальной передачи данных элемента аппаратуры под контрольконфигурации.Гарантия (Assuarance) - Результат запланированных или систематических действий,необходимых для обеспечения доказательства и очевидности того, что изделие или процессудовлетворяют заданным требованиям.Гарантия конструирования (Design assurance) - Все запланированные и систематическиедействия, используемые для того, чтобы привести достаточные основания на соответствующемуровне достоверности, что ошибки конструирования были выявлены и устранены, так чтоаппаратура удовлетворяет действующему сертифицирующему базису.Готовность (Availability) - Вероятность того, что элемент или функция находятся вработоспособном состоянии.Дефект (Defect) - Любое несоответствие характеристик установленным требованиям.Дефекты надежности (Reliability Defects) - Дефекты, которые вызывают отказ аппаратуры свысокой интенсивностью, когда условия нагрузки не превосходят номинальные расчетныепределы.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
