ГОСТ Р МЭК 61508-7—2007
Formal Methods: Use and Relevance for Development of Safety-Critical Systems. L. M. Barroca, J. A. McDermid.
The Computer Journal 35 (6). 579-599, 1992.
How to Produce Correct Software — An Introduction to Formal Specification and Program Development by
Transformations. E. A Boiten et al. The Computer Journal 35 (6). 547—554. 1992.
C.2.4.2 CCS — расчет взаимодействующих систем
Цепь: описание и анализ поведения систем, реализующих параллельные коммуникационные процессы.
Описание: CCS — это математический аппарат, описывающий поведение систем. Проект системы модели
руется в виде сети независимых процессов, реализующихся последовательно или параллельно. Процессы могут
взаимодействовать через порты (аналогичные каналам CSP). и взаимодействие осуществляется только при го
товности обоих процессов. Отсутствие детерминизма может быть смоделировано. Начиная с описания всей
системы на высоком уровне абстрагирования (трассирование), можно выполнять пошаговое уточнение системы
(стратегия сверху вниз) в рамках композиции взаимодействующих процессов, общее поведение которых форми
рует также поведение всей системы. В равной степени можно выполнять и стратегию снизу вверх, комбинируя
процессы и получая в результате необходимые свойства формируемой системы, используя правила вывода
композиционного типа.
Литература:
Communication and Concurrency. R. Miner. Prentice-Hall. 1989.
The Specification of Complex Systems. B. Cohen. W. T. Harwood and M. I. Jackson. Addison Wesley. 1986.
C.2.4.3 CSP — взаимодействующие последовательные процессы
Цель: спецификация конкурирующих программных систем, то есть систем, процессы которых реализуются
одновременно.
Описание: метод CSP обеспечивает язык для системных спецификаций процессов и подтверждения соот-
вествия реализации процессов их спецификациям (описанным как «трасса — допустимая последовательность
событий»).
Система моделируется в виде сети независимых процессов, составленных последовательно или парал
лельно. Каждый независимый процесс описывается в терминах всех его возможных поведений. Независимые
процессы могут взаимодействовать (синхронно или обмениваться данными) через каналы, и взаимодействие
происходит только при готовности обоих процессов. Может быть промоделирована относительная синхрониза ция
событий.
Теоретические положения метода CSP были непосредственновключены вархитектуру транспьютера INMOS.
а язык OCCAM позволил непосредственно реализовывать на сетях транспьютеров системы, специфицирован
ные в языке CSP.
Литература:
Communicating Sequential Processes. С A. R. Hoare. Prentice-Hall. 1985.
С.2.4.4 HOL — логика высшего порядка
Цель: спецификация и верификация аппаратных средств.
Описание: HOL представляет собой разработанную в компьютерной лаборатории Кембриджского универ
ситета конкретную логическую нотацию и систему, которая ее автоматически поддерживает. Логическая нотация
взята в основном из простой теории типов Черча, а машинная реализация основана на теории LCF (логихе
вычислимых функции).
Литература:
HOL: A Machine Orientated Formulation of Higher Order Logic. M. Gordon. University of Cambridge Technical
Report. No. 68. 1985.
Specification and Verification Using Higher-Order Logic: A Case Study. F. K. Hanna and N. Daeche. in: Formal
Aspects of VLSI Design: Proceedings of 1985 Edinburgh Workshop on VLSI. pp. 179 — 213. G. Milne and P. A.
Subrahmanyam (Eds.). North Holland. 1986
Application of formal methods to VIPER microprocessor. W. J. Cullyer. С H. Pygott. Proc. IEEE 134. 133 — 141.
1987.
C.2.4.5 LOTOS
Цель: описание и анализ поведения систем, реализующих параллельные коммуникационные процессы.
Описание: LOTOS (язык для спецификации процессов, упорядоченных во времени) основан на CCS с
дополнительными возможностями из близких алгебраических теорий CSP и CIRCAL (теория цепей). LOTOS
преодолевает недостатки CCS в управлении структурами данных и представлении значений выражений, объеди
няя его со вторым компонентом, основанным на языке абстрактных типов данных ACT ONE. Процесс описания
компонентов в LOTOS гложет быть также использован для других формальных методов при описании абстракт
ных типов данных (24).
С.2.4.6 OBJ
Цель: обеспечение точной спецификации системы в процессе диалога с пользователем и подтверждение
соответствия системы до ее реализации.
Описание: OBJ представляет собой алгебраический язык спецификаций. Пользователи определяют требо
вания в терминах алгебраических выражений. Системные аспекты (поведение или конструктивы) специфициру
ются в терминах операций, действующих над абстрактными типами данных (ADT). ADT подобен языку ADA, где
поведение оператора наблюдаемо, однако подробности реализации скрыты.
36