- стрелки, отмеченной заштрихованным кругом, с именем сигнала управления, проходящего в структурной диаграмме от одного модуля к другому, и эта стрелка также изображается параллельно линии, соединяющей два модуля.
Из любой нетривиальной диаграммы потока данных можно создать множество различных структурных диаграмм.
Диаграммы потоков данных отображают взаимоотношение между информацией и функциями системы. Структурные диаграммы отображают способ реализации элементов системы. Оба метода представляют собой действующие, хотя и различные точки зрения на конкретную систему.
Литература:
Software Engineering. I. Sommerville, Addison-Wesley, 3rd Edition, 1989.
Structured Design. L. L. Constantine and E. Yourdon, Englewood Cliffs, New Jersey, Prentice Hall, 1979.
Reliable Software Through Composite Design. G. J. Myers, New York, Van Nostrand, 1975.
C.2.4 Формальные методы
Примечание - Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблицы А.1, А.2, А.4 и В.5).
С.2.4.1 Общие положения
Цель: разработка программных средств, основанных на математических принципах. К этим средствам относятся методы формального проектирования и формального кодирования.
Описание: на основе формальных методов разработаны средства описания системы для решения отдельных задач на этапах спецификации, проектирования или реализации. Создаваемое в результате описание представляет собой строгую нотацию, математически анализируемую для обнаружения различных видов несогласованностей или некорректностей. Более того, такое описание может быть в некоторых случаях проанализировано автоматически по аналогии с проверкой компилятором синтаксиса исходной программы или, с целью показать различные аспекты поведения описываемой системы, использована анимация. Анимация может дать дополнительную уверенность в том, что система соответствует как реальным, так и формально специфицированным требованиям, поскольку это улучшает восприятие человеком специфицированного поведения системы.
Формальный метод обычно предлагает нотацию (как правило, используется один из методов дискретной математики), метод вывода описания в данной нотации и различные методы анализа описания для проверки корректности различных свойств системы.
Примечание - Приведенное выше описание содержится также в В.2.2.
Ряд формальных методов CCS, CSP, HOL, LOTOS, OBJ, временная логика, VDM и Z описан в подпунктах настоящего пункта. Следует заметить, что другие методы, например метод конечных автоматов (см. В.2.3.2) и сети Петри (см. В.2.3.3), в зависимости от корректности использования методами соответствующего строгого математического аппарата, могут рассматриваться как формальные.
Литература:
The Practice of Formal Methods In Safety-Critical Systems. S. Liu, V. Stavridou, B. Dutertre, J. Systems. Software 28, 77-87, Elsevier, 1995.
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. Milner, 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, где поведение оператора наблюдаемо, однако подробности реализации скрыты.
Спецификация OBJ и последующая пошаговая реализация подвергаются тем же формальным методам проверки, что и другие формальные методы. Более того, поскольку конструктивные аспекты спецификации OBJ автоматически исполнимы, существует непосредственная возможность подтверждения соответствия системы на основе самой спецификации. Исполнение - это по существу оценка функций системы путем подстановки выражений (перезаписыванием), которая продолжается до тех пор, пока не будут получены конкретные выходные значения. Эта исполнимость позволяет конечным пользователям рассматриваемой системы получать «облик» планируемой системы на этапе ее спецификации без необходимости знакомства с методами, лежащими в основе формальных спецификаций.
Как и все другие методы ADT, метод OBJ применим только к последовательным системам или к последовательным аспектам параллельных систем. Метод OBJ применяют для спецификации как малых, так и крупных промышленных приложений.
Литература:
An Introduction to OBJ: A language for Writing and Testing Specifications. J. A. Goguen and J. Tardo, Specification of Reliable Software, IEEE Press 1979, reprinted in Software Specification Techniques, N. Gehani, A. McGrettrick (eds), Addison-Wesley, 1985.
Algebraic Specification for Practical Software Production. С Rattray, Cogan Press, 1987.
An Algebraic Approach to the Standardisation and Certification of Graphics Software. R. Gnatz, Computer Graphics Forum 2 (2/3), 1983.
C.2.4.7 Временная логика
Цель: непосредственное выражение требований к безопасности и эксплуатации, а также формальное представление сохранения этих качеств на последующих этапах разработки.
Описание: стандартная предикатная логика первого порядка не содержит концепций времени. Временная логика расширяет логику первого порядка добавлением модальных операторов (например, «с этого момента» и «случайно»). Эти операторы могут использоваться для уточнения суждений о системе. Например, свойства безопасности могут потребовать использовать модальный оператор «с этого момента», но может потребоваться, чтобы и другие необходимые состояния системы были достигнуты «случайно» из некоторого другого начального состояния. Временные формулы интерпретируются последовательностями состояний (поведениями). Представление состояния зависит от выбранного уровня описания. Оно может относиться ко всей системе, системным компонентам или компьютерной программе.
Квантифицированные временные интервалы и ограничения во временной логике не обрабатываются явно. Абсолютное время обрабатывается путем образования дополнительных временных состояний, что является частью описания состояния.
Литература:
Temporal Logic of Programs. F. Kroger. EATCS Monographs on Computer Science, Vol. 8, Springer Verlag, 1987.
Design for Safety using Temporal Logic. J. Gorski. SAFECOMP 86, Sarlat, France, Pergamon Press, October 1986.
The Temporal Logic of Programs. A. Pnueli, 18th Annual Symposium on Foundations of Computer Science, IEEE, 1977.
Verifying Concurrent Processes Using Temporal Logic, Hailpern, T. Brent, Springer Verlag, 1981.
C.2.4.8 VDM, VDM++ - метод разработки Vienna
Цель: систематическая спецификация и реализация последовательных (VDM) и параллельных (VDM++) программ реального времени.
Описание: VDM - это математический метод спецификации и уточнения реализаций, который позволяет доказать их корректность относительно спецификации.
В этом основанном на модели методе спецификации состояние системы моделируется в терминах теоретико-множественных структур, в которых описаны инварианты (предикаты), а операции над этим состоянием моделируются путем определения их пред- и пост- условий в терминах системных состояний [29]. Операции могут проверяться на сохранение системных инвариантов.
Выполнение спецификаций осуществляется путем реализации состояния системы в терминах структур данных в заданном языке и уточнения операций в терминах программы на заданном языке. Этапы реализации и уточнения позволяют логически вывести свойства, устанавливающие корректность этих этапов. Выполняются или нет эти свойства, определяет разработчик.
В принципе VDM используется на этапе создания спецификации, но может также использоваться на этапах проектирования и реализации исходного кода. VDM может быть также применен к последовательно структурированным программам или к последовательным процессам в параллельных системах.
Объектно-ориентированное и параллельное для реального времени расширения VDM, VDM++ представляют собой язык формализованных спецификаций, основанный на языке VDM-SL, созданном в ИСО, и на объектно-ориентированном языке Smalltalk.
VDM++ имеет широкий диапазон конструкций, что позволяет пользователю формально специфицировать параллельные системы реального времени в объектно-ориентированной среде. В VDM++ полная формальная спецификация содержит совокупность спецификаций классов и отдельных характеристик рабочего пространства.
К средствам описания реального времени на языке VDM++ относятся:
- временные выражения, предусмотренные для представления, как текущего момента, так и момента вызова метода внутри тела метода;
- выражение, описывающее синхронизирующий сигнал, которое может быть добавлено к методу для спецификации верхних (или нижних) пределов времени исполнения для корректности реализаций;
- переменные непрерывного времени, которые должны быть введены. С условными операторами и операторами действия допускается специфицировать отношения (например, дифференциальные уравнения) между этими временными функциями, что оказалось очень полезно при спецификации требований к системам, действующим в среде с непрерывным временем. Уточняющие шаги приводят к дискретным программным решениям для программ реального времени.
Литература:
Conformity Clause for VDM-SL, G. I. Parkin and B. A. Wichmann, Lecture Notes in Computer Science 670, FME' 93 Industrial-Strength Formal Methods, First International Symposium of Formal Methods in Europe. Editors: J. С Р. Woodcock and P. G. Larsen. Springer Verlag, 501-520.
Major VDM+ - Language characteristics: http://www.ifad.dk/products/vdmlangchar.html
Systematic Software Development using VDM. С. В. Jones. Prentice-Hall. 2nd Edition, 1990.
Software Development - A Rigorous Approach. С. В. Jones. Prentice-Hall, 1980.
Formal Specification and Software Development. D. Bjorner and С. В. Jones, Prentice-Hall, 1982.
The Specification of Complex Systems. B. Cohen, W. T. Harwood and M. I. Jackson. Addison Wesley, 1986.
C.2.4.9 Z
Цель: Z - это нотация языка спецификаций для последовательных систем и метод проектирования, позволяющий разработчику выполнять работу, начиная со спецификации на языке Z до исполнительных алгоритмов, обеспечивая при этом доказательство их корректности по отношению к спецификации.
Язык Z в принципе используется на этапе спецификации, однако данный язык был разработан для использования от этапа составления спецификации до проектирования и реализации систем. Более всего он подходит для разработки последовательных систем, ориентированных на данные.
Описание: как и в VDM, в методе спецификации, реализованном в языке Z, состояние системы моделируется в терминах теоретико-множественных структур, в которых описаны инварианты (предикаты), а операции над этим состоянием моделируются путем определения их пред- и пост- условий в терминах системных состояний. Операции допускается проверять на сохранение системных инвариантов для демонстрации их согласованности. Формальная часть спецификации подразделяется на схемы, которые обеспечивают возможность структурирования спецификаций путем их усовершенствования.
