ГОСТ Р МЭК 61508-7—2012
анимация. Анимация может придать дополнительную уверенность в том. что система соответствует как реаль
ным. так и специфицированным требованиям.
В следующих пунктах настоящего приложения описаны два полуформальных метода:
В.2.3.2 Конечные автоматы/диаграммы переходов
П р и м е ч а н и е — Ссылка наданный метод/средство приведена в МЭК61508-3 (таблицы В.5. В.7. С.15иС.17).
Цель. Проведение моделирования, специфицирование или реализация структуры управления системы.
Описание. Многие системы могут быть описаны в терминах их состояний, входов идействий. Таким образом,
находясь в состоянии S1 и при получении входа /, система может выполнить действие А и перейти в состояние S2.
Путем описания действий системы для каждого входа в каждом состоянии можно полностью описать систему. Такая
модель системы называется машиной с конечными состояниями (или конечными автоматами). Ев часто
изображают в виде так называемой диаграммы переходов, которая показывает, как система переходит из одного
состояния в другое, или в виде матрицы, в которой для каждого состояния и входа задаютсядействия по переходу в
новое состояние.
В случае если система усложняется ипи имеет естественную структуру, то это может быть отражено в уров-
невой структуре конечного автомата. Диаграмма состояний — тип диаграммы переходов, в которой разрешены
вложенные состояния (состояние объекта разделяется на два или больше подсостояний, которые могут разви
ваться параллельно, и. возможно, в некоторый момент могут опять объединиться в одно состояние); это добавляет
выразительные возможности нотации переходов, но добавляет и дополнительную сложность, которая может быть
нежелательной для системы, связанной с безопасностью. Диаграммы состояний имеют формальную (математи
ческую) спецификацию. Диаграммы переходов могут применяться ко всей системе или к ее некоторому
объекту или элементу.
Спецификация или проект, выраженные в виде конечного автомата, могут быть проверены на:
- полноту (система или объект должны иметь действие и новое состояние для каждого входа в каждом со
стоянии):
- согласованность (возможно только одно состояние для каждой пары состояниеУвход):
- достижимость (возможно или нет перейти из одного состояния в другое с помощью некоторой последова
тельности входов)и
- отсутствие бесконечных циклов и тупиковых состояний и т. д.
Эти свойства являются важными для критических систем, так как легко разработать инструменты для обес
печения таких проверок, используя различные модели, основанные на теории конечных автоматов (формальные
языки, сети Петри, графы Маркова и т. д.). Существуют также алгоритмы, позволяющие автоматически генериро
вать тестовые примеры для верификации реализаций конечных автоматов или анимации модели конечного авто
мата. Диаграммы переходов и диаграммы состояний широко поддерживаются инструментальными средствами,
которые позволяют сформировать и проверить диаграммы, а также сгенерировать программный код для реализа
ции описанного конечного автомата.
Они могут также использоваться для вычислений вероятности отказа, см. В.6 и С.6.
Литература:
Introduction to Automata Theory. Languages, and Computation (3rd Edition). J. Hopcroft. R. Motwani. J. UHman,
Addison-Wesley Longman Publishing Co. 2006. ISBN: 0321462254.
Securisation des architectures mformatiques. Jean-Louis Boulanger. Hermes — Lavoisier. 2009. ISBN:
978-2-7462-1991-5.
B.2.3.3 Моделирование во времени сетями Петри
П р и м е ч а н и е — Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблицы В.5. В.7, С.15
и С.17).
Цель. Моделирование соответствующих аспектов поведения системы, оценка и. возможно, повышение
безопасности и эксплуатационных требований путем анализа и повторного проектирования.
Описание. Метод сетей Петри является частным случаем метода конечных автоматов. Сети Петри относятся
к классу моделей, описываемых теорией графов, и используются для представления информации и управления
потоками в системах, в которых процессы конкурентны и асинхронны.
Сеть Петри — это сеть позиций и переходов. Позиции могут быть «маркированными» или «немаркиро
ванными». Переход считают «активизированным», если все его входы маркированы. В активизированном со
стоянии позиции разрешается (но не требуется) быть «возбужденной». Если позиция «возбуждена», то вход,
поступающий на переход, становится немаркированным, а вместо него каждый выход из перехода оказывается
маркированным.
Потенциальные опасности могут быть представлены в виде конкретных состояний (маркировок) в модели
сети Петри. Модель гложет быть расширена с тем. чтобы обеспечить возможности моделирования систем во вре
мени. И хотя «классические» сети Петри концентрируются на моделировании потоков управления, существуют
некоторые расширения модели сети Петри, в которых моделируются потоки данных.
Литература:
Timed Petri Nets: Theory and Application. Jiacun Wang. Spnnger. 1998, ISBN 0792382706.
Securisation des architectures informatiques. Jean-Louis Boulanger. Hermes — Lavoisier. 2009. ISBN:
978-2-7462-1991-5.
19