ГОСТРМЭК 62279—2016
D.28 Формальные методы
D.28.1 Общие положения
Цель. «Формальные методы» относятся к математически строгим методам и инструментальным средствам
для спецификации, проектирования и проверки систем программного обеспечения и аппаратных средств.
Описание. «Математически строгий» означает, что спецификации, используемые в формальных методах,
являются правильно построенными операторами в математической логике, а формальные проверки — строгие
выводы в этой логике (т. е. каждый шаг выполняется по правилам вывода и. следовательно, может быть проверен с
помощью механического процесса). Важность формальных методов в том, что они обеспечивают средства сим
вольного исследования всего пространства состояний цифрового проекта (или аппаратных средств или программ
ного обеспечения) и установливают свойство правильности или безопасности, которое является истиной для всех
возможных входов. Однако в настоящее время это редко реализуется на практике (за исключением критических
компонентов критических систем безопасности) из-за большой сложности реальных систем.
Используется несколько подходов, чтобы преодолеть астрономический размер пространства состояний, свя
занного с реальными системами:
- применяются формальные методы к требованиям и проектам высокого уровня, где от большинства дета
лей выполнено абстрагирование;
- применяются формальные методы только к самым критическим компонентам;
- анализируются модели программного обеспечения и аппаратных средств, в которых значения переменных
делают дискретными, а их диапазоны существенно уменьшают;
- анализируются модели систем иерархическим способом, который реализует принцип «разделяй и вла
ствуй»;
- насколько это возможно, максимально автоматизируются проверки.
Несмотря на то. что математическая логика используется во всех формальных методах, нет никакого един
ственного лучшего «формального метода». Каждая прикладная предметная область требует различных методов
моделирования и различных подходов доказательства. Кроме того, даже в определенной прикладной предметной
области, различные стадии жизненного цикла могут быть лучше всего выполнены с использованием других инстру
ментальных средств и методов. Например, программа автоматического доказательства теоремы могла бы лучше
всего использоваться для анализа правильности описания на уровне межрегистровых пересылок схемы быстрого
преобразования Фурье, тогда как алгебраические методы вывода могли бы лучше всего использоваться для ана лиза
правильности усовершенствований проекта, представленного на уровне логических элементов. Поэтому во всем
мире разработано большое количество формальных методов.
В следующих пунктах описаны несколько примеров формальных методов. Список примеров здесь не ис
черпывающий. Описаны формальные методы: CSP. CCS. HOL. LOTOS. OBJ. временная логика. VDM, Z Метод. В
Метод и метод проверки моделей.
0.28.2 Взаимодействующие последовательные процессы (CSP)
Цель. Спецификация конкурирующих программных систем, то есть систем, процессы которых реализуются
одновременно.
Описание. Метод CSP обеспечивает языкдля спецификации процессов системы и доказательства соответ
ствия реализации процессов их спецификациям (описанным как трасса, то есть в виде допустимых последователь
ностей событий).
Система моделируется в виде сети независимых процессов. Каждый независимый процесс описывается в
терминах всех его возможных поведений. Моделируемая система состоит из последовательных или параллельных
процессов. Процессы могут взаимодействовать (синхронно или обмениваться данными) через каналы, и взаи
модействие происходит только при готовности обоих процессов. Может быть промоделирована относительная
синхронизация событий.
Теоретические положения метода CSP были непосредственно включены в архитектуру транспьютера
INMOS4 а язык OCCAM2*позволил непосредственно реализовывать на сетях транспьютеров системы, специфи
цированных в языке CSP.
0.28.3 Расчет взаимодействующих систем (CCS)
Цель. Описание и анализ поведения систем, реализующих параллельные коммуникационные процессы.
Описание. Аналогично CSP. CCS также является математическим аппаратом, описывающим поведение си
стем. Проект системы моделируется в виде сети независимых процессов, реализующихся последовательно или
параллельно. Процессы могут взаимодействовать через порты (аналогичные каналам CSP), и взаимодействие
осуществляется только при готовности обоих процессов. Может быть смоделировано отсутствие детерминизма.
Начиная с описания всей системы на высоком уровне абстрагирования (трассирование), можно выполнять по-
INMOS была британской полупроводниковой компанией, которая произвела в 80-х инновационную
архитектуру микропроцессора, предназначенную для параллельной обработки, названной транспьютером. Позже
INMOS стала частью SGS-Thomson, затем STMicroelectronics.
2) OCCAM — параллельный язык программирования, который называют в честь Уильяма из Ockham,
известного из-за Бритвы Оккама. Это — собственный язык программирования транспьютера INMOS.
78