ГОСТ Р МЭК 61508-7—2007
В.2.3 Полуформальные методы
Цель: создание недвусмысленных и согласованных частей спецификации с целью обнаружения ошибок и
пропусков.
П р и м е ч а н и е — Ссылка на данный метод/средство приведена в МЭК 61508-2 (таблицы В.1. В.2 и В.6} и
в МЭК 61508-3 (таблицы А.1, А.2 и А.4).
В.2.3.1 Общие положения
Цель: убедиться в том. что проект соотвествует своей спецификации.
Описание: полуформальные методы обеспечивают средства создания описания системы на стадиях ее
разработки (например спецификации, проектирования или кодирования). Описание может быть в некоторых
случаях проанализировано на ЭВМ или для отображения различных аспектов поведения системы использована
анимация. Анимация может придатьдополнительную уверенность втом. что система соответствует какреальным,
так и специфицированным требованиям.
В следующих пунктах настоящего приложения описаны два полуформальных метода.
В.2.3.2 Метод конечных автоматов /диаграммы переходов состояний
П р и м е ч а н и е — Ссыпка на данный метод/средство приведена в МЭК 61508-3 (таблицы В.5 и В.7).
Цель: проведение моделирования, специфицирование или реализация структуры управления системы.
Описание: многие системы могут быть описаны в терминах их состояний, входов и действий. Таким обра
зом. находясь всостоянии S1 и при получении входа I. система может выполнить действие А и перейти в состоя ние
S2. Путем описания действий системы для каждого входа в каждом состоянии можно полностью описать
систему. Такая модель системы называется «автоматом с конечными состояниями». Ее часто изображают в виде
так называемой «диаграммы переходов состояний», которая показывает, как система переходит из одного состо
яния в другое, или в виде матрицы, в которой для каждого состояния и входа задаются действия по переходу 8
новое состояние.
В случае, если система усложняется или имеет естественную структуру, тоэто может быть отражено вуров-
невой структуре «автомата с конечными состояниями».
Спецификация (проект), выраженная(ый) в виде «автомата с конечными состояниями», могут быть прове
рены:
- на полноту (система должна иметь действие и новое состояние для каждого входа в каждом состоянии);
- согласованность (только одно изменение состояния описывается для каждой пары состояние/вход) и
- достижимость (можно или нельзя перейти из одного состояния в другое при любой последовательности
входов).
Это важные свойства для критических систем. Инструменты для обеспечения этих проверок легко разрабо
тать. Существуют также алгоритмы, позволяющие автоматически генерировать тестовые примеры для верифика
ции реализаций «автомата с конечными состояниями» или анимации модели «автомата с конечными
состояни ями».
Литература:
Introduction to theory of Finite State Machines. A. Gill. McGraw-Hill. 1962.
B.2.3.3 Метод сетей Петри
П р и м е ч а н и е — Ссыпка на данный метод/средство приведена в МЭК 61508-3 (таблицы В.5 и В.7).
Цель: моделирование соответствующих аспектов поведения системы, оценка и. возможно, повышение бе
зопасности и эксплуатационных требований путем анализа и повторного проектирования.
Описание, сети Петри относятся к классу моделей, описываемых теорией графов, и используются для
представления информации и управления потоками в системах, в которых процессы конкурентны и асинхронны.
Сеть Петри — это сеть позиций и переходов. Позиции могут быть «маркированными» или «немаркирован
ными». Переход считают «активизированным», если все его входы маркированы. В активизированном состоянии
позиции разрешается (но не требуется) быть «возбужденной». Если позиция «возбуждена», то вход, поступаю
щий на переход, становится немаркированным, а вместо него каждый выход из перехода оказывается маркиро
ванным.
Потенциальные опасности могут быть представлены в виде конкретных состояний (маркировок) в модели
сети Петри. Модель может быть расширена с тем. чтобы обеспечить возможности моделирования систем во
времени. И хотя «классические» сети Петри концентрируются на моделировании потоков управления, существуют
некоторые расширения модели сети Петри, в которых моделируются потоки данных.
Литература:
Petri nets: Properties, analysis and applications. T. Murata. Proc. IEEE 77 (4). 541—580. April 1989.
Safety analysis using Petri nets. N. G. Leveson. J. L. Stolzy. Proc. 15thAnn. Int. Sympon Fault-Tolerant Computing,
358—363. IEEE, 1985.
Using Petri nets for safety analysis of unmanned Metro system. M. El Koursi. P. Ozello. Proc. SAFECOMP ’92.
135—139. Pergamon Press. 1992.
20