ГОСТ Р МЭК 62279—2016
Описание. Проверка модели — это процесс проверки, определяющий является ли данная структура моде
лью заданной логической формулы. Это общая концепция и применяется ко всем типам логик и подходящих струк
тур. Простой задачей проверки модели является определение, является ли данная структура моделью заданной
логической формулы в логике высказываний.
Для алгоритмической проверки формальных систем был разработан важный класс методов проверки моде
ли. Этодостигается проверкой, удовлетворяет ли структура, часто получаемая из проекта аппаратных средств или
программного обеспечения, формальной спецификации, обычно представленной формулой во временной логике.
Проверка модели чаще всего применяется в проектах аппаратных средств. Для программного обеспечения
из-за неразрешимости (см. теорию вычислимости) этот подход не может быть полностью алгоритмизован; обычно
данный подход не гложет доказать или опровергнуть заданное свойство.
Структура обычно задается в виде описания в исходном коде языка описания промышленных аппаратных
средств или языка специального назначения. Такая программа соответствует конечному автомату, т. е. направ
ленному графу, состоящему из узлов (или вершин) и дут. С каждым узлом связан набор атомарных высказываний,
обычно устанавливающих, какие элементы памяти с ним связаны. Узлы представляют состояния системы, дуги
представляют возможные переходы, которые могут изменить состояние, а атомарные высказывания представляют
основные свойства, которые характеризуют точку выполнения.
Формально, проблема может быть представлена следующим образом: задается желаемое свойство, выра
женное в виде формулы р во временной логике, и структура
М
с начальным состоянием s. и если
М
имеет конечное
значение, как это выполняется для аппаратных средств, то проверка модели сводится к поиску на графе.
D.29 Формальное доказательство
Цель. Используя теоретические и математические модели и правила возможно доказать правильность про
граммы или модели, не выполняя ее.
Описание. Ряд операторов включаются в различные места программы и они используются в качестве пред- и
постусловий для различных путей в программе. Доказательство заключается в демонстрации того, что программа
преобразует предусловия в постусловия согласно ряду логических правил, и что программа завершается.
В настоящем приложении описано несколько формальных методов, например. CCS. CSP. HOL. LOTOS. OBJ,
Временная логика. VDM и Z. Их описания можно найти в D.28.
D.30 Прямое исправление
Цель. Обеспечить корректное функционирование в присутствии одного или более сбоев.
Описание. Если был обнаружен сбой, то текущее состояние системы обрабатывается, чтобы получить со
стояние. которое будет непротиворечивым спустя некоторое время. Эта концепция особенно подходит для систем
реального времени с небольшой базой данных и с высокой скоростью изменения внутреннего состояния. Пред
полагается. что. по крайней мере, часть состояния системы может быть окружением, и только часть состояний
системы находится под влияние (принуждением) окружения.
D.31 Постепенное отключение функций
Цель. Обеспечение пригодности наиболее критичных системных функций, несмотря на отказы, путем игно
рирования наименее критичных функций.
Описание. Данный метод устанавливает приоритеты для различных функций, выполняемых системой. Про
ект создаваемой системы гарантирует, что в случае недостаточности ресурсов для выполнения всех системных
функций функции высшего приоритета будут выполнены в предпочтение функциям более низкого приоритета.
Например, функции регистрации ошибки и события могут оказаться задачей более низкого приоритета, чем си
стемные функции управления, и в этом случае управление системой будет продолжаться, даже если аппаратные
средства из-за регистрации ошибки окажутся неработоспособными.
Другим примером была бы система сигнализации, где в случав потери связи с центром управления ло
кальное линейное путевое оборудование автоматически устанавливает доступные маршруты для направления с
трафиком наивысшего приоритета. Будет происходить постепенное отключение функций, потому что поезда при
оритетных маршрутов будут в состоянии пройти через область, где произошла потеря связи с центром управления,
но другие движения, такие как маневровое передвижение, будет невозможно.
D.32 Анализ влияния
Цель. Определение влияния изменения или расширения в программном обеспечении, которое оказывается
на другие программные модули этого программного обеспечения, а также на другие системы.
Описание. Перед выполнением модификации или расширения программного обеспечения следует выпол
нить анализ, чтобы определить влияние модификации или расширения на программное обеспечение, а также
определить, на какие программные системы и программные модули это повлияет.
Далее принимается решение о повторной верификации программной системы. Это зависит от числа подвер
гнувшихся воздействию программных модулей, их критичности и характера изменений. Возможными решениями
могут быть:
81