Методика реализации программно-управляемого процесса разработки и верификации программных средств автоматизированных систем специального назначения

Введение

Высокая динамичность подготовки и ведения современных боевых действий обусловлива­ют необходимость всеобъемлющего и соглосованного использования в системе управления силами и средствами специального назначения комплексов средств автоматиза­ции (КСА), систем связи и передачи данных (ССПД), построенных на основе современ­ных информационных и телекоммуникацион­ных технологий. Предприятия оборонно-про­мышленного комплекса (ОПК) Российской Федерации, осуществляющие разработку та­ких сложных программно-технических сис­тем (СПТС), должны учитывать следующие существенные особенности систем и процес­са их создания:

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

Разработка СПТС представляет собой сложную и ресурсоемкую задачу, результат решения которой, к сожалению, не всегда удовлетворяет заданным требованиям и соответствует объему выделенных временных и финансовых ресурсов. При этом стоит от­метить тенденцию возрастания роли и значе­ния в обеспечении корректного и надежного функционирования СПТС их программной составляющей - программных средств сис­тем вооружения (ПССВ). В ходе применения СПТС подтверждено, что до 85...90 % отказ­ных ситуаций обусловлены ошибками в их программной составляющей.

О наличии серьезных проблем при соз­дании и внедрении СПТС красноречиво сви­детельствуют результаты анализа успешности выполнения как отечественных, так и зарубежных проектов по их созданию. В качестве примера приведем данные из отчета компании The Standish Group [1] о качестве реализации проектов по созданию информационных сис­тем (ИС), выполненных в США за последние 15 лет. Согласно этим данным, только 16,2 % проектов были завершены вовремя и в рамках первоначального бюджета. При этом 31,1 % проектов по созданию ИС провалились, в 52,7 % случаев возникли проблемы, из-за которых итоговый бюджет превысил первона­чальный в среднем в 2 раза, а сроки - в 3,3 раза, при этом было реализовано менее 75 % тре­буемого функционала. Основные причины этого - низкое качество исходного комплек­са требований к разрабатываемой системе, отсутствие автоматизированных средств их валидации, сопровождения и коррекции. Ак­туальность данной проблемы подтверждают приведенные в работе [2] данные: бюджет про­екта в случае внесения изменений в требова­ния возрастает более чем в 3 раза, а сроки ис­полнения - более чем в 2 раза.

Для решения указанных проблем в рам­ках системной и программной инженерии соз­даются новые более эффективные технологии, модели и средства автоматизированного проек­тирования, разработки и верификации СПТС. Процесс разработки СПТС состоит из трех основных этапов: обоснование требований, проектирование и реализация. Каждый из них в соответствии с методологией модельно-ори­ентированного подхода включает процедуру верификации соответствующего артефакта. По результатам проведенного анализа можно заключить, что в настоящее время достаточно успешно решены вопросы, связанные с автома­тизацией процессов генерации и верификации программного кода, создаваемого на этапе ре­ализации. В то же время на начальных этапах создания СПТС, в частности, на этапах фор­мирования комплекса требований и проекти­рования архитектуры системы, по-прежнему требуется существенное участие специалистов в области системной инженерии и информаци­онных технологий.

Подтверждением актуальности автома­тизированной поддержки процессов обоснова­ния требований и проектирования архитекту­ры служат данные о распределении стоимости устранения ошибок, внесенных и обнаружен­ных на различных этапах жизненного цик­ла (ЖЦ) СПТС. Например, в монографии из­вестного американского эксперта Б. Боэма [3] отмечено, что удельная стоимость исправления дефектов возрастает по экспоненциальному закону распределения по мере продвижения продукта к стадии эксплуатации. При этом затраты на исправление дефекта, внесенного на этапе обоснования требований, при его об­наружении на этапе проектирования возрас­тают в 5 раз, на этапе реализации в 10 раз, на этапе тестирования в 20 раз, а в ходе эксплуа­тации - в 100 и более раз (рис. 1).

В связи с этим, главной целью исследова­ний и работ, основные результаты выполнения которых представлены в данной статье, явля­лась разработка алгоритмического, програм­много и методического обеспечения процес­сов построения и верификации формальных моделей комплекса требований и архитектуры программных средств (ПС), предназначенных для использования в КСА и ССПД автомати­зированных систем специального назначения (АССН). Их использование позволит снизить затраты на поиск и устранение дефектов, вно­симых на этапах формирования требований и проектирования архитектуры, и существен­но повысить качество (функциональную кор­ректность, надежность, производительность, защищенность, совместимость) разрабатыва­емых систем благодаря реализации програм­мно-управляемого процесса их разработки и верификации.

Обзор современной нормативно-методической базы и научных публикаций в области разработки и верификации СПТС

Наиболее важными нормативно-методиче­скими документами в этой области, по мне­нию автора данной статьи, являются специ­фикации и модели, разработанные под эги­дой международной организации Object Management Group (OMG), с которой сотруд­ничают более 800 научно-исследовательских и государственных организаций (INCOSE, EURESCOM, DISA, NIST, NASA и др.) и про­мышленных компаний (AT&T, IBM, Oracle, Microsoft, Cisco Systems и др.). В настоящее время на сайте организации [4] опубликовано более 230 методических документов и специ­фикаций. В контексте рассматриваемых в настоящей статье вопросов наиболее важны­ми из них являются следующие: Meta Object Facility (MOF), Unified Modeling Language (UML), XML Metadata Interchange (XMI), Sys­tem Modeling Language (SysML), Object Con­straint Language (OCL), UML Testing Profile (UTP), Action Language for Foundational UML (ALF), Semantics of a Foundational Subset for Executable UML Models (FUML), Requirements Interchange Format (ReqIF).

Приведенные выше документы состав­ляют научно-методическую базу системной и программной инженерии, они активно исполь­зуются на практике, постоянно дополняются и совершенствуются. В России активные иссле­дования в этой области ведутся в Институте систем программирования им. В. П. Иванни­кова, на факультете вычислительной матема­тики и кибернетики МГУ им. М. В. Ломоно­сова, в Санкт-Петербургском государственном университете, Новосибирском государствен­ном техническом университете, Военно-кос­мической академии имени А. Ф. Можайского и др. Ниже приведен краткий анализ наибо­лее интересных, с точки зрения автора, науч­но-технических публикаций и работ.

В первую очередь следует представить монографии и практические руководства.

В фундаментальном труде известного серб­ского ученого и эксперта в области MBSE, профессора Белградского университе­та Д. Милисева (Dragan Milicev) [5] изло­жены принципы и методы применения для промышленной разработки СПТС совре­менных информационных технологий, ос­нованных на объектной парадигме и модельноориентированном подходе, и, что особенно ценно в контексте исследуемых в настоящей статье проблем, даны рекоменда­ции и примеры использования для этих це­лей фундаментальной части языка модели­рования UML - Foundational UML (FUML). На его основе создаются и верифицируются исполняемые формальные UML-модели. Так­же отметим монографию [6], разработанную С. Фриденталем, А. Муром, Р. Штайнером, которые являются активными участниками разработки целого ряда методических документов и спецификаций OMG и применяют свои знания на практике в Lockheed Martin и Raytheon Company. В ней в сжатой форме с примерами изложены не только приемы и способы применения конструкций и механиз­мов языка SysML, но и дано объяснение его философии и принципов.

Следующую группу образуют публика­ции, посвященные решению частных задач разработки и верификации СПТС. Диссертаци­онная работа сотрудника НГТУ А. В. Маркова посвящена вопросам автоматизации процессов проектирования и анализа программного обе­спечения с использованием языка UML и сетей Петри [7]. В работе дано описание методики проектирования программного обеспечения с использованием UML-диаграмм последова­тельности в формате .xmi и представлен способ их автоматической трансляции в формат .cpn, используемый для описания сетей Петри. Ре­зультатом применения этой методики являют­ся иерархические сети Петри, в ходе анализа которых осуществляется верификации проекта программного обеспечения (ПО), представлен­ного в виде UML-диаграмм. Наиболее ценны­ми для практики представляются следующие изложенные в данной работе решения:

• алгоритм преобразования UML-диа­грамм в сети Петри;
• алгоритм и правила реализации инвер­сии в сетях Петри для проверки достижимости выбранного состояния сети;
• алгоритмическое и программное обе­спечение для построения и анализа сетей Пе­три с целью выявить и устранить дефекты соз­даваемого ПО.

Полезная и ценная информация содер­жится в обзоре современных методов автома­тической генерации тестов [8]. В работе дано описание следующих методов:

• структурного тестирования с помощью символического выполнения (structural testing using symbolic execution);
• тестирования на основе моделей (model-based testing);
• комбинаторного тестирования (combi­natorial testing);
• выборочного тестирования (random testing);
• поиска на основе тестирования (search- based testing).

В статье [9] описан способ проектиро­вания и моделирования бизнес-процессов, реализуемых в парадигме сервисно-ориен­тированной архитектуры (Service Oriented Architecture, SOA), с помощью диаграмм актив­ности, для верификации которых предложено использовать аппарат цветных сетей Петри (Colour Petri Net, CPN).

В работе [10], подготовленной специа­листами Шанхайского университета, описан подход к верификации крупномасштабных веб-проектов посредством разработки и ана­лиза исполняемой модели соответствующего программного обеспечения. Для построения исполняемой модели разработан метод, в кото­ром в качестве исходных данных используются динамические диаграммы последовательно­стей (Live Sequence Charts, LSCs). UML-мо­дель, представленная с помощью LSCs-диа­грамм, преобразуется в символьный конечный автомат. Сценарии тестирования создаются путем обхода автомата методом «поиск в глу­бину» (Depth-first search, DFS).

В статье [11] описаны два метода реали­зации автоматической проверки нагруженных систем реального времени с использованием сценариев. В первом случае система моделируется как сеть временных автоматов (ВА). Во втором - с помощью набора диаграмм динамических последовательностей (LSCs) и требований в виде отдельной анализируемой LSC-диаграммы. Автором статьи разработаны временные (темпоральные) расширения для подмножества ядра языка LSC и определена его семантика на основе трассировки. Ана­лизируемая LSC-диаграмма транслируется в ее поведенческий эквивалент в нотации диаграммы ВА. Верификация корректности модели осуществляется посредством модели­рования диаграммы ВА в режиме реального времени с использованием аппарата темпо­ральной логики (Computational Tree Logic, CTL) с последующим сравнением получен­ного результата с эталоном. Оба метода ре­ализованы с помощью средств инструмента UPPAAL.

В работе [12] описан способ генериро­вания модульных тестов (unit case) на основе модели архитектуры, представленной в фор­ме UML-диаграмм активностей. Построение тестов осуществляется с помощью решателей SMT/SAT, которые анализируют управляющий граф программы, записанной на математиче­ском языке программирования AMPL. Особое внимание уделено смешанному целочисленно­му нелинейному программированию и постро­ению логических формул (Object Constraint Language, OCL) для ограничений.

В статье [13] для установления и син­хронизации связей системных требований с элементами дизайна предложено применять поведенческие SysML-диаграммы. Для реали­зации автоматической верификации проекта в виде комплекса SysML-диаграмм приведены следующие операции:

• преобразование SysML-диаграмм ак­тивностей в сети Петри, представленные на языке Petri Net Markup Language (PNML);
• математический аппарат и инструмен­тальные средства анализа сетей Петри CPN Tools и SPIN;
• алгоритм верификации присутствую­щих в SysML-диаграммах деятельности вре­менных требований, представленных в виде формул линейной темпоральной логики (Linear Temporal Logic, LTL), с помощью разработан­ного автором данной работы языка (Active Temporal Requirement Language, AcTRL).

В статье [14] для создания средств ди­намической верификации и валидации про­ектных поведенческих моделей предложено использовать исполняемые предметно-ориентированные языки моделирования (executable Domain-Specific Modeling Languages, XDSML). С помощью созданных на их основе средств можно осуществлять мониторинг состояния анализируемых моделей посредством по­строения и управления трассами их испол­нения в среде виртуальной машины XDSML. Данный метод имеет более высокую произ­водительность по сравнению со стандартной UML-метамоделью благодаря возможности ис­ключать из обработки избыточные данные [14].

По результатам анализа публикаций и представленных в них решений можно заклю­чить, что основные усилия исследователей направлены на разработку методов и средств автоматизированной генерации и верификации программных реализаций СПТС, в меньшей степени - на автоматизацию разработки и ве­рификации проектных решений. Практически отсутствуют решения для автоматизированно­го формирования и верификации комплекса требований. В качестве основных математи­ческих моделей и построенных на их основе средств для автоматической верификации ис­пользуются математический аппарат и алго­ритмы анализа сетей Петри, решатели задач SMT/SAT, различные вариации исполняемых языков моделирования xUML, а также пред­метно-ориентированные языки моделирова­ния XDSML.

Обоснование проблемных вопросов и способов их решения

В настоящее время наиболее эффективным для создания СПТС является подход, основан­ный на методологии модельно-ориентирован­ной системной инженерии (МОСИ) (Model- based systems engineering, MBSE) [15], вклю­чающий три базовые технологии: разработку на основе моделей (Model driven development, MDD); архитектуру на основе моделей (Model driven architecture, MDA); тестирование на ос­нове моделей (Model based testing, MBT). В хо­де реализации данного подхода предполага­ется, что создаваемые и используемые на всех этапах ЖЦ системы артефакты (комплекс тре­бований, технический проект, программные и технические реализации, средства верифика­ции и тестирования) представляются в виде формальных моделей. Благодаря этому может быть реализован программно-управляемый процесс создания ПССВ.

Процесс создания ПССВ по методоло­гии МОСИ схематично представлен на рис. 2. Он включает три этапа, на которых создаются модели трех типов:

• модель анализа (формальное представ­ление комплекса требований к системе);
• модель архитектуры (формальное пред­ставление технического проекта);
• модель реализации (формальное пред­ставление программной реализации).

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

Для синхронизации и обеспечения пря­мых и обратных связей между всеми моделями (артефактами жизненного цикла разрабатыва­емых систем) должны быть разработаны мето­ды и алгоритмы автоматической трансформа­ции и синхронизации моделей разных уровней. Формально-математической основой MBSE являются языки визуального проектирования и моделирования: MOF, UML, SysML, FUML, AFL, ArchiMate, AADL, SDL, Modelica и др. Технологическую базу составляют такие ин­струментальные средства, как IBM Rhapsody, Magic Draw, Sparx Enterprize Architect, Eclipse Papyrus, MASIW и др.

В настоящее время технологии и средства МОСИ применяются при создании систем и комплексов, используемых в авиационно-кос­мической, автомобильной, кораблестроительной, микроэлектронной, энергетической, военной и других отраслях. Благодаря их ис­пользованию были достигнуты определенные успехи в части повышения производительно­сти труда разработчиков СПТС, улучшения их качества и сокращения сроков создания.

В то же время кардинальным образом улуч­шить ситуацию пока не удалось. Основными сдерживающими факторами достижения каче­ственных улучшений в решении данных задач являются:

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

Таким образом, для преодоления пред­ставленных выше проблем и реализации программно-управляемого последователь­но-итерационного процесса разработки и ве­рификации моделей анализа и архитектуры

ПССВ в соответствии со схемой (см. рис. 2), необходимо разработать алгоритмическое и программное обеспечение:

• построения формального описания требо­ваний к системе (модели анализа) на основе ис­ходной неформальной формы их представления;
• поддержки процесса проектирования ПССВ в виде связанного набора исполняемых FUML диаграмм - модели архитектуры;
• автоматизированного построения и вы­полнения тестовых сценариев верификации моделей анализа и архитектуры.

В качестве единой концептуальной, язы­ковой и инструментальной среды разработки и верификации моделей анализа и архитектуры ПССВ предлагается использовать языки мо­делирования UML, FUML и ALF, абстрактный язык описания метамоделей MOF (MetaObject Facility) и протокол обмена метаданными XMI (XML Metadata Interchange).

В следующих разделах представлено описание разработанных автором статьи спо­собов и алгоритмов решения данных задач.

Алгоритм построения формальной модели требований на языке FUML

Схема алгоритма построения формальной мо­дели требований (модели анализа), предна­значенного для реализации процедуры № 1 (см. рис. 2), представлена на рис. 3. Алго­ритм заключается в построении набора свя­занных между собой FUML-диаграмм вари­антов использования (ДВИ) - d _ uc, обзор­ных диаграмм взаимодействия (ОДВ) - d _ io, диаграмм классов (ДКл) - d _ class, диаграмм требований (ДТр) - d _ reqs, диаграмм параме­тров (ДПар) - d _ pars.

Опишем диаграмму i-го варианта ис­пользования, представляющего собой функ­циональное требование:

где а_к - пользователь или внешняя система, инициирующие исполнение функции (вари­анта использования) f_i;

f_i - функция системы, реализующая вари­ант использования uc_i;

b_j - компонент (модуль, блок, класс) сис­темы, реализующий функцию:

f_i (input, operation, result),

где input - входные данные;

operation - алгоритм или программа, реа­лизующие выполнение функции f;

result - результат выполнения функцииJ_i.

Для каждого варианта использования разрабатывается обзорная диаграмма взаимо­действия d_io:

Здесь  описывает алго­ритм реализации функции j-м блоком (клас­сом) проектируемого программного средства, который включает описание основного  и альтернативных потоков 

Альтернативные потоки описывают рабо­ту программ при возникновении нештатных си­туаций, например, ошибочных действий поль­зователя, непредусмотренных воздействий со стороны внешней среды и др. Основные и аль­тернативные потоки могут иметь подчиненные потоки, которые в ОДВ представляются с по­мощью фреймов с приставкой ref_. Подчинен­ные потоки ОДВ отражают функционирование программы с точки зрения пользователя и мо­гут быть формализованы с помощью диаграмм активностей, диаграмм последовательностей, машин состояний или коммуникаций. Для зада­ния порядка и возможности реализации тех или иных потоков применяются пред- и постусло­вия. Для построения обзорных диаграмм взаи­модействия используются:

• узлы управления node controlтипа de­cision node, merge node, fork node, join node, interaction, interaction use;
• узлы данных node object;
• ссылки на диаграммы активности ref_act;
• ссылки на диаграммы последователь­ности refseq;
• ссылки на диаграммы машин состояний refsm;
• ссылки на диаграммы коммуникаций

Детальные описания алгоритмов реали­зации функции с системной точки зрения как основного, так и альтернативных потоков раз­рабатываются на этапе проектирования ПССВ. На обзорной диаграмме взаимодействия могут также применяться псевдоузлы, соответствую­щие началу алгоритма initial node, завершению потока управления flow final node и алгоритма activity final node, а также временные ограниче­ния duration constraint, time constraint.

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

где r₁^f - требования к оперативности испол­нения функции f;

г₂^f - требования к производительности (например, объемы хранимых, обрабатывае­мых и передаваемых данных, количество поль­зователей, количество и размеры запросов в единицу времени и др.);

r₃^f - требования к надежности (коэффи­циент готовности, время безотказной работы, время восстановления и др.);

r₄^f - требования к защищенности.

Для каждого функционального блока и информационного объекта программы разра­батывается конструкция class, в которой зада­ются атрибуты, операции (методы), ограниче­ния и семантика. Наборы взаимодействующих классов объединяются в диаграммы классов dclass. Формально диаграмма классов может быть описана так:

d_class = (class, interface, features, relations),

где class - имена классов;

interface - интерфейсы, описывающие сигнатуры операций (входные и выходные параметры), за реализацию которых отвеча­ют соответствующие классы. Связь класса с соответствующим интерфейсом описыва­ется посредством отношения realization или dependency;

features - атрибуты класса, которые могут включать ограничения на значения атрибутов constraint;

relations - отношения ассоциации (associ­ation), обобщения (generalization) и зави­симости (dependency) между классами. Класс владеет (ownedAttribute) атрибутами (StructuralFeature) и может находиться в опре­деленных отношениях (association, generalisa­tion, ...) с другими классами. Атрибуты имеют определенный тип (DataType) и характеристи­ку множественности (MultiplicityElevent).

Фрагмент модели анализа программного обеспечения информационно-аналитического центра (ИАЦ), разработанной в соответствии с описанным выше алгоритмом, представлен на рис. 4. Данный фрагмент содержит основные элементы формальной модели требований к программному обеспечению ИАЦ, обеспечи­вающего реализацию функций сбора, анализа данных и подготовки решения. Основными элементами данной модели являются: диаграм­мы вариантов использования (d_uc), обзорная диаграмма взаимодействия (d_io), диаграмма требований (dreqs), диаграмма активностей (dact), диаграммы классов (d class), диаграм­ма параметров (d_pars). Они связаны между собой посредством отношений «удовлетворять требованию» (satisfy) и «включения» (include), а также через общие атрибуты.

Построенная таким образом модель ана­лиза требований подвергается процедурам ва­лидации и верификации. Процедура валидации заключается в оценивании комплекса требова­ний на предмет его полноты и корректности и выполняется как программными средствами, так и неформальной экспертизой специалистов в данной предметной области. При верифика­ции проверяются такие свойства модели, как непротиворечивость, системность, неизбыточность, безопасность, живость, отсутствие взаимоблокировок, невыполнимых операций и зацикливаний. Процедура верификации мо­дели требований осуществляется посредством ее исполнения и тестирования в среде вирту­альной машины FUML и анализа с помощью решателей SAT/SMT. Описание этих методов и средств представлено в следующих разделах.

Алгоритм проектирования ПССВ

Проектирование архитектуры ПССВ реали­зуется в соответствии с алгоритмом (рис. 5). В качестве исходных данных используется модель анализа, представленная обзорны­ми диаграммами взаимодействия d_io, диа­граммами требований к качеству реализа­ции функций d_reqs, диаграммами классов d class, диаграммами параметров d_pars, а также требованиями к технологиям разра­ботки и среде функционирования. На основе каждой d_io_i разрабатываются и детализиру­ются входящие в нее диаграммы активностей dact_i, последовательностей dseq, состояний d_sm и коммуникаций dcomm. Для реализа­ции процедуры верификации три последних типа диаграмм транслируются в диаграм­мы активностей и представляются на языке ALF (Action Language for Foundational UML). Каждая диаграмма активностей описывается с помощью узлов управления (node_control) типа decision node, merge node, fork node, join node, interaction, interaction use; узлов дан­ных (node object); пре- (pre) и пост- (post) условий.

На следующем шаге алгоритма на основе каждой d_io_i разрабатываются и детализиру­ются входящие в нее диаграммы активностей (dact), последовательностей (d seq), состояний (d_sm) и коммуникаций (dcomm). Затем для реализации процедуры верификации три последних типа диаграмм транслируются в диаграммы активностей и представляются на языке ALF (Action Language for Foundational UML). На завершающем шаге алгоритма вы­полняются доработка и корректировка диа­граммы классов (d_class) и диаграммы тре­бований (d regs) для их согласования с разработанными диаграммами активностей.

На рис. 6 приведена схема, иллюстри­рующая процедуру верификации формаль­ной FUML-модели архитектуры ПССВ по­средством ее исполнения в среде виртуальной FUML-машины, включающей три компо­нента: ExecutionFactory, Executor и Locus. ExecutionFactory (фабрика выполнения моде­лей) используется для создания экземпляров семантических классов visitor, соответствую­щих исполняемым элементам FUML-модели.

Класс Executor, представляющий собой абстракцию виртуальной машины для испол­нения FUML-модели, обеспечивает выполне­ние операций:

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

Выполнение FUML-модели осущест­вляется в конкретной виртуальной машине (Locus), являющейся абстракцией физическо­го или виртуального компьютера. Верифици­руемая в среде виртуальной FUML-машины модель архитектуры (см. рис. 6) построена из FUML-диаграмм классов и активностей и представлена на языке ALF. Модель архитек­туры ПССВ верифицируется на предмет удов­летворения основным требованиям:

• полноты реализации функциональных требований, определенных в обзорных диа­граммах взаимодействия d_io;
• полноты и корректности реализации нефункциональных требований, определенных в диаграммах требований d_reqs и диаграммах параметров d_pars;
• согласованности и непротиворечивости всех диаграмм модели;
• отсутствия избыточности.

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

Алгоритм разработки тестовых сценариев для верификации моделей анализа, архитектуры и реализации ПССВ Схема алгоритма разработки тестовых сцена­риев для верификации моделей анализа, архи­тектуры и реализации ПССВ представлена на рис. 7. Основными этапами реализации дан­ного алгоритма являются:

• построение по управляющим графам диаграмм активности графов тестовых сцена­риев (ТСц);
• описание ТСц на языке ALF;
• генерация ТСц для верификации моде­ли анализа;
• генерация ТСц для верификации моде­ли архитектуры;
• генерация ТСц для верификации моде­ли реализации.

На вход данного алгоритма может пода­ваться либо модель анализа, представленная в виде FUML обзорных диаграмм взаимодей­ствия, либо модель архитектуры, представленная в виде FUML-диаграмм активностей. На их основе строится соответствующий ве­рифицируемой модели граф ТСц, в кото­ром учтены функциональные и нефункцио­нальные требования к разрабатываемому ПССВ. Последние должны быть записаны на языке ограничений OCL (Object Constraint Language). Представленный на языке ALF ТСц передается на вход решателям SMT/SAT CVC-4 [16] и Z3 [17]. Эти решатели посред­ством символьного исполнения программ и процедур автоматического доказательства те­орем осуществляют обнаружение таких дефек­тов, как нарушение безопасности и живости, возможности взаимоблокировок и зациклива­ний, наличие тупиков, нарушение граничных значений переменных, и других ошибок про­ектирования и реализации. Для обнаружен­ных дефектов решатели SMT/SAT генерируют тесты (контрпримеры), с помощью которых разработчики могут установить и устранить причины этих дефектов и ошибок.

Заключение

В настоящее время для разработки сложных программно-технических систем активно при­меняются модельно-ориентированные техно­логии, методы и средства. При их использова­нии все артефакты жизненного цикла системы (требования, архитектура и реализация) долж­ны быть представлены в виде формальных мо­делей. На основе проведенного анализа можно заключить, что наибольшую трудность пред­ставляют задачи формализации и верифика­ции требований и архитектуры. Это обуслов­лено, во-первых, объективной сложностью задачи формализации изначально неформаль­ного представления требований, во-вторых, - отсутствием четких и конкретных правил и алгоритмов построения формальных моделей требований и архитектуры с помощью предла­гаемых для этого разнообразных языков и ин­струментальных средств.

Для преодоления указанных выше труд­ностей были разработаны следующие модели, алгоритмы и методики:

• графово-текстовая метамодель форма­лизованного представления комплекса требо­ваний к ПС АССН в виде фиксированного на­бора взаимосвязанных FUML-диаграмм;
• графово-текстовая метамодель форма­лизованного описания архитектуры ПС АССН в виде рационального набора взаимосвязанных FUML-диаграмм;
• алгоритмы разработки формальных мо­делей требований и архитектуры ПС АССН на основе разработанных для них метамоделей;
• алгоритмы верификации моделей тре­бований и архитектуры ПС АССН посредством их моделирования и анализа в среде виртуаль­ной FUML-машины и выполнения тестовых сценариев, построенных с помощью решате­лей SMT/SAT;
• методические рекомендации реализа­ции программно-управляемого процесса раз­работки и верификации ПС АССН с помощью разработанных моделей и алгоритмов.

В настоящее время сотрудники Военно­космической академии им. А. Ф. Можайского проводят работы по реализации описанных в статье моделей и алгоритмов в виде комплек­са программных средств. В качестве среды и прототипов используются инструментальные средства, библиотеки и приложения, реализо­ванные в рамках проекта Eclipse (EFM, GMP, Papyrus, Moka, ReqCycl, Titan) [18]. Примене­ние данного комплекса позволит реализовать программно-управляемый процесс разработки и верификации ПС АССН. Основными его до­стоинствами являются:

• использование единой модельно-язы­ковой и информационно-программной среды разработки и верификации формальных моде­лей требований, архитектуры и программной реализации ПС АССН, построенной на осно­ве технологий объектно-ориентированного анализа и проектирования, методов и средств дедуктивной верификации, языков и средств визуального моделирования FUML, XMI, ALF, VMFUML;
• реализация автоматизированных проце­дур верификации, валидации и коррекции ком­плекса требований и проектных решений как в случае обнаружения каких-либо дефектов, так и при изменении самих требований или условий эксплуатации АССН, что позволит улучшить экономические показатели в части снижения финансовых и временных затрат, связанных с выполнением дополнительных работ.