ГОСТ Р МЭК 61508-7—2012
How to Produce Correct Software — An Introduction to Formal Specification and Program Development by
Transformations. E. A. Boiten et el.. The Computer Journal 35 (6). 547—554. 1992.
C.2.4.2 CCS — расчет взаимодействующих систем
Цель. Описание и анализ поведения систем, реализующих параллельные коммуникационные процессы.
Описание. CCS — это математический аппарат, описывающий поведение систем. Проект системы модели
руется в виде сети независимых процессов, реализующихся последовательно или параллельно. Процессы могут
взаимодействовать через порты (аналогичные каналам CSP). и взаимодействие осуществляется только при готов
ности обоих процессов. Может быть смоделировано отсутствие детерминизма. Начиная с описания всей системы на
высоком уровне абстрагирования (трассирование), можно выполнять пошаговое уточнение системы (стратегия
сверху вниз) в рамках композиции взаимодействующих процессов, общее поведение которых формирует также по
ведение всей системы. В равной степени можно выполнять и стратегию снизу вверх, комбинируя процессы и полу чая
в результате необходимые свойства формируемой системы, используя правила вывода композиционного типа.
Литература:
Communication and Concurrency. R. Milner. Prentice-Hall, 1989, ISBN 9780131150072.
C.2.4.3 CSP — взаимодействующие последовательные процессы
Цель. Спецификация конкурирующих программных систем, то есть систем, процессы которых реализуются
одновременно.
Описание. Метод CSP обеспечивает язык для спецификаций процессов системы и подтверждения соотве-
ствия реализации процессов их спецификациям (описанным как трасса, то есть допустимая последовательность
событий).
Система моделируется в виде сети независимых процессов, составленных последовательно или параллель
но. Каждый независимый процесс описывается в терминах всех его возможных поведений. Независимые процессы
могут взаимодействовать (синхронно или обмениваться данными) через каналы, и взаимодействие происходит
только при готовности обоих процессов. Может быть промоделирована относительная синхронизация событий.
Теоретические положения метода CSPбыли непосредственно включены в архитектуру транспьютера INMOS,
а язык OCCAM позволил непосредственно реализовывать на сетях транспьютеров системы, специфицированные
в языке CSP.
Литература:
Communicating Sequential Processes: The First 25 Years. A.Abdallah, C. Jones, J. Sanders (Eds.). Springer. 2004,
ISBN 3540258132. 9783540258131.
C.2.4.4 HOL — логика высшего порядка
Цель. Спецификация и верификация аппаратных средств.
Описание. HOL представляет собой разработанную в компьютерной лаборатории Кембриджского универ
ситета конкретную логическую нотацию и систему, которая ее автоматически поддерживает. Логическая нотация
взята в основном из простой теории типов Черча, а машинная реализация основана на теории LCF (логике вы
числимых функции).
Литература:
Higher-Order Computational Logic. J. Uoyd. In Computational Logic: Logic Programming and Beyond, Lecture
Notes in Computer Science. Springer Berlin/Heidelberg. 2002, ISBN 978-3-540-43959-2.
C.2.4.5 LOTOS
Цель. Описание и анализ поведения систем, реализующих параллельные коммуникационные процессы.
Описание. LOTOS (язык для спецификации процессов, упорядоченных во времени) основан на CCS с до
полнительными возможностями из близких алгебраических теорий CSP и CIRCAL (теория цепей). LOTOS преодо
левает недостатки CCS в управлении структурами данных и представлении значений выражений, обьединяя его с
аспектами языка абстрактных типов данных ACT ONE. Процесс описания аспектов в LOTOS может быть однако
использован для других формальных методов при описании абстрактных типов данных.
Литература:
Model Checking for Software Architectures. R. Mateescu. In Software Architecture. Lecture Notes in Computer
Science. Springer Berlin/Heidelberg. 2004, ISBN 978-3-540-22000-8.
ISO 8807:1989, Information processing systems — Open Systems Interconnection — LOTOS—A formal description
technique based on the temporal ordering of observational behavior.
C.2.4.6 OBJ
Цель. Обеспечение точной спецификации системы в процессе диалога с пользователем и подтверждение
соответствия системы до ее реализации.
Описание. OBJ представляет собой алгебраический язык спецификаций. Пользователи определяют требо
вания в терминах алгебраических выражений. Системные аспекты (поведение или конструктивы) специфициру
ются в терминах операций, действующих над абстрактными типами данных (ADT). ADT подобен языку ADA. где
поведение оператора наблюдаемо, однако подробности реализации скрыты.
Спецификация OBJ и последующая пошаговая реализация подвергаются тем же формальным методам про
верки. что и другие формальные методы. Более того, поскольку конструктивные аспекты спецификации OBJ авто
матически исполнимы, существует непосредственная возможность подтверждения соответствия системы на осно ве
самой спецификации. Исполнение — это по существу оценка функций системы путем подстановки выражений
(перезаписыванием), которая продолжается до тех пор. пока не будут получены конкретные выходные значения.
Эта исполнимость позволяет конечным пользователям рассматриваемой системы получать «облик» планируемой
37