IEC TS 61508-3-2:2024
Функциональная безопасность электрических/электронных/программируемых электронных систем, связанных с безопасностью. Часть 3-2: Требования и руководство по использованию математических и логических методов для установления точных свойств программного обеспечения и его документации.
- Стандартный №
- IEC TS 61508-3-2:2024
- Дата публикации
- 2024
- Разместил
- International Electrotechnical Commission (IEC)
- Последняя версия
- IEC TS 61508-3-2:2024
- сфера применения
-
Интерпретация основного содержания технической спецификации IEC TS 61508-3-2:2024
Стандарт IEC TS 61508-3-2, ключевой компонент серии стандартов IEC 61508, был опубликован Международной электротехнической комиссией (МЭК) в августе 2024 года. Он содержит подробные требования и руководство по применению математических и логических методов (M<) в программном обеспечении, связанном с безопасностью. Эта спецификация направлена на улучшение систематических возможностей критически важного для безопасности программного обеспечения с помощью формальных методов, гарантируя его соответствие указанным требованиям уровня полноты безопасности (SIL).
Предпосылки разработки спецификации и технологическая эволюция
В связи с широким применением цифровых технологий в критически важных для безопасности областях традиционные методы разработки программного обеспечения сталкиваются с серьезными проблемами в обеспечении надежности программного обеспечения. Хотя стандарт IEC 61508-3:2010 обеспечивает базовую структуру для безопасной разработки программного обеспечения, в нём отсутствуют конкретные рекомендации по применению формальных методов. Выпуск данной технической спецификации восполняет этот пробел и отражает консенсус отрасли о важности технологии формальной верификации в системах, критически важных для безопасности. Что касается технологического развития, спецификация включает в себя новейшие результаты исследований в области формальных методов, проверки моделей и абстрактной интерпретации, преобразуя передовые академические технологии в промышленно применимые инженерные практики. Особо следует отметить, что спецификация устанавливает чёткие требования к применению таких инструментов, как автоматизированные средства проверки и проверки моделей.
Ключевые термины и определения
Спецификация устанавливает полную терминологическую систему, предоставляя точную концептуальную основу для применения математических и логических методов:
Категории терминов Основные термины Техническое значение Требования к применению Формальная основа Формальный язык Язык с определенной грамматикой, который может быть проанализирован с помощью численных вычислений Должен быть однозначным и поддающимся вычислительной проверке Методы проверки Абстрактная интерпретация Статический анализ, обеспечивающий надежные результаты для абстрактных состояний программы Должен гарантировать надежность Процесс разработки Точка подтверждения Доказуемые свойства триплета программного обеспечения/документации (S1, S2, P) Должны быть формально проверены Уровень кода Уровень исполняемого исходного кода (ESCL) Наивысший уровень кода, который полностью описывает поведение программного обеспечения Должен быть явно выбран и проверен Определения этих терминов отражают двойное стремление спецификации к математической точности и инженерной практичности, закладывая основа для последующих технических требований.
Требования к спецификации формальных требований безопасности (FSRS)
Глава 5 определяет конкретные требования к спецификации формальных требований безопасности:
5.1 Требование ясности: FSRS должна быть однозначной, строгой формальной спецификацией, которая может быть написана на языке формальных спецификаций или на контролируемом естественном языке. В спецификации подчеркивается, что формальность не обязательно означает полную автоматизацию; ручной анализ приемлем.
5.2 Требование проверки: FSRS должна быть проверена на согласованность и относительную полноту с использованием математических и/или логических методов. Проверки согласованности гарантируют отсутствие внутренних противоречий в спецификации, а проверки относительной полноты гарантируют, что все сценарии, которые потенциально могут привести к опасностям, были рассмотрены в FSRS.
Рекомендации по технической реализации: В реальных проектах рекомендуется применять стратегию многоуровневой формальной спецификации, сначала используя формальный язык высокого уровня (такой как метод Z или B) для описания требований безопасности на уровне системы, а затем постепенно дорабатывая их до формальных спецификаций на уровне программного обеспечения.
Формальные требования к спецификациям архитектуры и проектирования программного обеспечения
Глава 6 определяет формальные требования к спецификациям архитектуры/проектирования программного обеспечения (SWA/DS):
6.1 Требования к строгости: SWA/DS должны быть строгими, то есть спецификация должна быть недвусмысленной, четко охватывать все возможные поведения и допускать тщательную проверку на корректность и некорректность.
6.2 Проверка точек гарантии: Удовлетворение FSRS со стороны SWA/DS является ключевой точкой гарантии и должно быть формально, строго и правильно проверено. Спецификация явно указывает, что автоматизированная формальная верификация не является обязательной, а ручная формальная верификация приемлема.
Это требование отражает рассмотрение спецификации практической осуществимости, признавая, что полностью автоматизированная верификация может быть нецелесообразной или экономически невыгодной в некоторых случаях.
Выбор и проверка уровня исполняемого исходного кода (ESCL)
Глава 7 рассматривает вопрос выбора нескольких уровней кода в языках программирования высокого уровня:
7.1 Выбор уровня: При использовании языка программирования высокого уровня может быть несколько уровней, которые полностью описывают точное поведение программного обеспечения. Разработчики должны явно выбрать один из уровней в качестве ESCL. Например, при разработке на Java в качестве ESCL может быть выбран исходный код или байт-код Java.
7.2 Проверка точки гарантии: Соответствие кода ESCL требованиям SWA/DS является еще одной ключевой точкой гарантии и должно быть формально проверено. В спецификации еще раз подчеркивается, что автоматическая верификация не является обязательным требованием.
Это положение обеспечивает гибкость разработки, позволяя выбирать наиболее подходящую стратегию верификации в зависимости от конкретных обстоятельств проекта.
Требования к гарантии компиляции и выполнения
Главы 8 и 9 рассматривают конкретные требования к компиляции и выполнению соответственно:
8. Проверка компиляции: Соответствие целевого кода ESCL является гарантированной точкой и должно быть строго и правильно формально проверено. Спецификация признает, что ручная проверка часто нецелесообразна, и рекомендует использовать сертифицированный компилятор для предоставления формальных гарантий состояния.
9. Ошибки выполнения: Необходимо разработать список типов ошибок времени выполнения, которых следует избегать, и строго и правильно формально проверить их, чтобы гарантировать, что эти ошибки не возникнут. Кроме того, обработчики исключений времени выполнения должны быть проверены для достижения указанного состояния системы при возникновении исключения.
Тип проверки Объект проверки Метод проверки Требования к инструментам Проверка компиляции Целевой код или ESCL Формальная проверка, сертифицированный компилятор Компилятор формальной проверки Проверка во время выполнения Избежание ошибок, обработка исключений Формальная проверка, статический анализ Инструменты статического анализа, проверка модели Анализ времени WCET/WCRT/Schedulability Анализ времени выполнения в наихудшем случае Инструменты анализа WCET
Применимые технологии и методологии
Глава 10 и Приложения A, B и C устанавливают комплексную структуру методологии:
10.1 Выбор технологий: Выбранные технологии M< должны быть четко определены, обоснованы, надежны и соответствовать требуемым задачам. В Приложении A представлена классификация 25 применимых технологий M<, охватывающих весь жизненный цикл от спецификации требований до проверки целевого кода.
Характеристики технической системы: Техническая система, устанавливаемая спецификацией, обладает следующими примечательными характеристиками:
- Комплексность: Охватывает все этапы жизненного цикла разработки программного обеспечения
- Иерархичность: Многоуровневая технология, от высокоуровневых формальных спецификаций до низкоуровневой проверки кода
- Практичность: Делает акцент на применении зрелых промышленных технологий, а не чисто академических подходов
- Гибкость: Позволяет выбирать подходящую комбинацию технологий на основе специфики проекта
В приложениях B и C представлены конкретные технические инструменты и свойства, которые они гарантируют, а также подробные рекомендации для инженерной практики.
Рекомендации по реализации и передовой опыт
На основе требований спецификации предлагаются следующие рекомендации по реализации:
1. Стратегия постепенной формализации: Рекомендуется использовать подход постепенной формализации, сначала применяя формальные методы к ключевым функциям безопасности, а затем постепенно расширяя его на всю систему. Это помогает снизить начальную сложность и стоимость внедрения.
2. Интеграция цепочки инструментов: Создайте интегрированную цепочку инструментов формальной верификации, чтобы гарантировать, что результаты различных этапов верификации могут быть взаимосвязаны и отслеживаемы. Обратите особое внимание на интеграцию инструментов верификации компилятора и инструментов статического анализа.
3. Обучение персонала: Усилить обучение разработчиков формальным методам, в частности, умению писать формальные спецификации и применять методы верификации.
4. Управление процессами: Включить мероприятия по формальной верификации в управление процессом разработки программного обеспечения, прояснить цели верификации и критерии приемки для каждого этапа.
5. Управление доказательствами: Создать комплексную систему управления доказательствами верификации, чтобы гарантировать, что результаты верификации на всех точках обеспечения могут быть эффективно проанализированы и отслежены.
Прикладная ценность стандартов и влияние на отрасль
Выпуск IEC TS 61508-3-2:2024 оказывает значительное влияние на отрасль программного обеспечения, критически важного для безопасности:
Продвижение технологий: спецификация будет способствовать широкому применению формальных методов в отрасли и способствовать разработке и совершенствованию инструментов и технологий верификации.
Повышение качества: благодаря применению методов математической логики можно значительно повысить надежность и достоверность программного обеспечения, критически важного для безопасности.
Оптимизация затрат: хотя первоначальные инвестиции в формальную верификацию высоки, она может значительно снизить стоимость последующего тестирования и обслуживания и имеет ценовые преимущества с точки зрения полного жизненного цикла.
Упрощение сертификации: она предоставляет четкие технические требования и методы верификации, что помогает упростить процесс сертификации безопасности.
Эта техническая спецификация представляет будущее Направление развития разработки критически важного для безопасности программного обеспечения и обеспечивает техническую основу и методическое руководство для создания высоконадежных цифровых систем безопасности.
IEC TS 61508-3-2:2024 Ссылочный документ
- IEC 61508-3:2010 Функциональная безопасность электрических/электронных/программируемых электронных систем, связанных с безопасностью. Часть 3. Требования к программному обеспечению
- IEC 61508-4:2010 Функциональная безопасность электрических/электронных/программируемых электронных систем, связанных с безопасностью. Часть 4. Определения и сокращения.
IEC TS 61508-3-2:2024 История
- 2024 IEC TS 61508-3-2:2024 Функциональная безопасность электрических/электронных/программируемых электронных систем, связанных с безопасностью. Часть 3-2: Требования и руководство по использованию математических и логических методов для установления точных свойств программного обеспечения и его документации.
