Технологии разработки надежного программного обеспечения

Рекомендации по разработке спецификации требований

При разработке спецификации требований применяется структурная методология, а также формальные и полуформальные методы. Существует ряд структурных методологий. Для информационноуправляющих систем наиболее интересны методологии MASCOT, JSD, real-time Yourdon, которые ориентированы на управление производственным процессом и применение в режиме реального времени (что особенно важно для безопасности критически важных приложений).

Структурированные методы по существу «думающие инструменты», целью которых является систематическое понимание проблемы и разбиение ее на составные части. Их главные особенности следующие:

• • логический порядок мышления, разбивающий большую проблему на управляемые стадии;
• • идентификация полной системы, включая окружающую среду, а также необходимую систему;
• • разложение данных и функций в требуемой системе.

Формальные методы обеспечивают средства разработки описания системы на некоторой стадии разработки ее спецификации, проекта или кода. Получающееся описание принимает математическую форму и может быть подвергнуто математическому анализу, чтобы обнаружить различные классы противоречивости или некорректности. Кроме того, описание может в некоторых случаях быть проанализировано машиной с точностью, подобной проверке синтаксиса исходной программы посредством компилятора. Формальный метод в общем случае предлагает систему обозначений (обычно некоторую форму используемой дискретной математики), а также технический прием для получения описания в предлагаемой системе обозначений. Формальный метод предлагает различные формы анализа для того, чтобы проверить описание для различных свойств корректности. К формальным методам относятся CSP, OBJ, LOTOS и др.

Метод CSP. С помощью метода CSP система может быть смоделирована посредством составляющих ее последовательных или параллельных независимых процессов. Процессы могут обмениваться сообщениями (синхронизировать или обмениваться данными) через каналы, связи. Обмен данными имеет место только тогда, когда оба процесса готовы. Относительный выбор времени событий также может быть смоделирован.

Метод CSP обеспечивает язык для спецификации систем процессов и доказательство того, что выполнение процессов удовлетворяет их спецификации, описанной как трассировка — разрешенная последовательность событий.

Метод OBJ является алгебраическим языком спецификации. Пользователи определяют требования в терминах алгебраического уравнения. Спецификация OBJ и последующее пошаговое выполнение поддается одним и тем же формальным методам доказательства, как и другие формальные подходы. Кроме того, так как конструктивные аспекты спецификации OBJ являются выполнимыми на аппаратных средствах, аттестацию системы можно выполнять непосредственно из спецификации, что позволяет конечным пользователям предусмотренной системы получать представление о возможной системе на стадии разработки спецификации системы.

Метод OBJ применим только к последовательным системам или к последовательным аспектам параллельных систем. Данный метод широко используется для спецификации как малых, так и крупномасштабных промышленных приложений.