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

г'1 Ь Ун

' 3 РОССИЙСКАЯ АКАДЕМИЯ НАУК

ИНСТИТУТ ПРОБЛЕМ УПРАВЛЕНИЯ

Ц ; -

О Я На правах рукописи

¡ л

ПРАВИКОВ Дмитрий Игоревич

УДК 681.3.066

Разработка и исследование методов создания корректных алгоритмов функционирования специалиэирванных операционных систем.

Специальность 05.13.11 - математическое # программное

обеспечение вычислительных машин, комплексов, систем и сетей.

АВТОРЕФЕРАТ диссертации на соискание учёной степени кандидата технических наук

РОССИЙСКАЯ АКАДЕМИЯ НАУК ИНСТИТУТ ПРОБЛЕМ УПРАВЛЕНИЯ

На правах рукописи

ПРАВИКОВ Дмитрий Игоревич

УДК 681.3.066

Разработка и исследование методов создания корректных алгоритмов функционирования специализирванных операционных систем.

Специальность 05.13.11 - математическое и программное

обеспечение вычислительных машин, комплексов, систем и сетей.

АВТОРЕФЕРАТ диссертации на соискание учёной степени кандидата технических наук

Работа выполнена в Институте проблем управления (автоматики телемеханики) РАН.

доктор технических наук, профессор Волков А. Ф. доктор технических наук,

профессор Трахтенгерц -3. А__

кандидат технических наук, доцент Гаранина О. И.

Ведущее предприятие - ЦНИИ <Граниг»,

г.Санкт-Петербург

Защита состоится ¿^¿^о^^р 1994 года в_ часов не

заседании специализированного совета Л 002.68.01 Института проблем управления РАН по адресу: 117342, Москва, Профсоюзная ул. , 65.

С диссертацией можно ознакомиться в библиотеке Института проблем управления.

»

Автореферат разослан « ^-^¿^Р_1994 года.

Научный руководитель

Официальные оппоненты

Учёный секретарь специализированного совета кандидат технических наук

Юркевич Е.I

ОБШАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы. Одной из основных черт современного разви-я техники является широкое использование автоматизированных и томатических систем управления производственно-технологическими оцессами и техническими объектами. Основу таких систем составля-средства вычислительной техники, объединённые 'в развитые специ-изированные многомашинные .вычислительные комплексы (СМВК). При-нение вычислительной техники в системах управления различными ъектани в режиме реального времени предъявляет жёсткие требова-я к качеству аппаратуры и программного обеспечения (ПО). Учиты-я устойчивую тенденцию к повышению доли затрат на ПО, с одной ороны, и большое количество апробированных методов построения дёжной( аппаратуры, с другой стороны, можно сделать вывод о том, о в ближайшей перспективе качество ПО будет определять надёж-сть функционирования СМВК и всей системы управления в целом.

Центральное место среди ПО СМВК управляющих систем занимают ерационные системы (ОС) - по оценкам, приводимым в отечественной тературе, на их долю приходится до 50% затрат от общей стоимости , и именно ОС в основном определяют эффективность использования ВК. Поскольку неправильное функционирование ОС способно парали-вать работу всей- системы управления, то требования, предьявляе-е к её качеству, выше, чем к прикладному программному обеспече-ю.

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

В настоящее время хорошо изученными являются методы построе ва коРРектности алгоритмов относительно заданны спецификаций. Но вместе с тем, на практике при ссгствгвленки—савил. фикаций и преобразовании алгоритмов в программы, в основном ис пользуются эвристические методы, из-за чего полученные алгоритмы программы могут не соответствать техническому заданию.

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

Целью диссертационной работы является разработка и исследова ние методологии, методов и средств создания корректных алгоритмо специализированных операционных систем и их эквивалентного преоб разования в программное- обеспечение для многомашинных вычислитель ных комплексов реального времени.

Для достижения поставленной цели в диссертационной £аботе_.ре шены следующие основные задачи:

- проведён анализ процесса разработки ОС;

- определён подход к формализации первичных описаний ОС;

- разработана модель динамики обобщённого вычислительного процесса (ВП) в СМВК;

- разработаны методы построения и анализа модели динамики обобщённого ВП в СМВК;

- разработана процедура построения спецификаций базовых про цедур ОС на основании анализа модели динамики обобщенного ВП СМВК;

- определён подход к синтезу и анализу алгоритмов отдельны базовых процедур ОС;

- определён подход к преобразованию алгоритмов в программы на языке низкого уровня;

- разработана человеко-машинная процедура преобразования алгоритмов базовых процедур ОС в программы на языке низкого уровня.

Методы исследования. Разработка и исследования методов создания корректных алгоритмов специализированных ОС и их эквивалентного преобразования в программное обеспечение выполнены с использованием аппарата математической логики, теории множеств, теории автоматов, сетей Петри, исчисления предикатов, теории алгоритмов и методов системного программирования.

Научная новизна диссертационной работы заключается в следующем:

- (разработана методология проектирования ОС СМВК заданного класса, обеспечивающая корректность программ относительно эскизного проекта ОС;

- разработана модель динамики обобщённого ВП в СМВК заданного класса;

- в рамках разработанной модели формализовано понятие корректности разрабатываемой ОС СНВК;

- разработана процедура получения спецификаций базовых процедур ОС с использоданием а качестве исходных данных модели динамики обобщённого ВП в СНВК;

- проведён анализ влияния предложенной методологии на процесс разработки ОС СНВК.

Практическая ценность. Разработана методология проектирования ОС СМВК, которая охватывает все стадии проектирования, начиная от получения технического задания и кончая выдачей текстов программ отдельных процедур ОС на языке низкого уровня. Данная методология позволяет повысить качество разрабатываемого программного обеспе-

Разработанный препроцессор метаязыка макро-11, который явля ется составной частью человеко-машинной процедуры преобразован« алгоритмов в программы, может применяться независимо от предла женной методологии для упрощения кодирования как системного, так прикладного ПО.

Внедрение. Результаты работы использованы в НИР «Лабиринт» ОКР «ЗБ-15», .проведённых Институтом' проблем управления в интереса ЦНИИ «Гранит», что подтверждается актом о внедрении.

Апробация работы. Основные результаты работы докладывались ь секции учёного совета ЦНИИ «Гранит», Ленинград 1990, и на межрес публиканской конференции молодых ученых и специалистов «Информати ка. Роботизация. Автоматизация.», Минск 1990.

Публикации. По теме диссертации автором опубликованы 3 печат ные работы.

Объем и структура диссертационной работы. Работа состоит V введения, четырех глав, заключения и изложена на 115 страницах ма шинописного текста; .дополнительно содержит 2 страницы рисунков список литературы из 55 наименований и 3 приложения.

СОДЕРЖАНИЕ РАБОТЫ

Во введении обоснована актуальность темы диссертационной ра боты, дана формулировка цели работы и общая характеристика пол> ценных результатов.

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

Основой управляющих систем реального времени специального на-начения является специализированный многомашинный вычислительный омплекс. Для исследования в работе был выбран определённый класс МВК: вычислительный комплекс, состоящий из ряда одинаковых микро-ВМ, соединенных параллельными магистральными связями (рис. 1). временным параметром, определяющим конкретные реализации комплек-ов рассматриваемого класса, является количество микроэвм. Входные выходные данные поступают в микроэвм через параллельную магист-аль, поэтому обмен данными с внешними устройствами идентичен об-ену между микроэвм. Возможные конфликты, возникающие при взаимо-ействии через общую шину разрешаются арбитром шины. Синхронизация аботы комплекса осуществляется через сигналы таймера, одновре-енно по'ступающие на все микроэвм.

рис. 1.

В СМВК осуществляется периодическое решение некоторого задан-эго набора связанных между собой функциональных задач (ФЗ), рас-эеделённого по микроэвм комплекса.

Центральное место среди ПО СМВК занимает операционная систе-1, которая реализует следующие основные функции:

1. распараллеливание вычислительного процесса, диспетчериза-1Я задач, организация синхронизации между ними;

2. управление устройствами, входящими в состав СНВК, и обме информацией между ними;

3. управление памятью.

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

Особенностью рассматриваемого СНВК реального времени являете заданность перечня решаемых ФЗ, организация вычислительного проце сса в реальном времени и специализация архитектурных принципов по строения СНВК.

В диссертации принят подход, согласно которому качество О СМВК обеспечивается в процессе её разработки, которая должна вес тись с применением формальных методов.

По существующим стандартам, в процессе разработки любого П можно выделить три основные фазы: 1) анализ и спецификация требо ваний, 2) проектирование, 3) реализация.

Анализ возможных ошибок, возникающих на каждой стадии, пока

I

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

С понятием специфицирования ПО связано понятие корректности означающее соответствие представления программы после завершени очередной фазы разработки своей спецификации.

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

- быть формальным;

- позволять проверять непротиворечивость и полноту требована

к ОС СНВК;

- служить основой для формализованного получения спецификаций алгоритмов ОС.

В качестве такого описания ОС была выбрана модель динамики ВП в СНВК.

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

В заключение сформулированы цель работы и задачи, которые не- |

I

обходимо решить для достижения поставленной цели.

Вр второй главе излагаются модели динамики частного и обобщённого ВП в заданном классе СНВК, даётся процедура построения обобщённой модели, предложены методы её анализа. Приведена процедура получения спецификаций базовых процедур ОС на основании изучения модели, определён подход к проектированию алгоритмов по по!

лученным спецификациям. |

Для создания обобщённой модели определены статическая и дина- | мическая составляющие частной модели динамики ВП в СМВК, проведён анализ модели динамики частного ВП.и .на её основе построена мой'ель динамики обобщённого ВП; выбран формализм представления модели в случае конкретной реализации, дана процедура построения моделирующей сети Петри. Приведён пример построения модели для типичной ОС.

Пусть - множество микроЭВН СНВК, где J - множество

номеров микроЭВН. С точки зрения проектирования ОС каждая микроЭВН представляет собой набор физических ресурсов ^ = | 1еЬ}, где Ь -множество номеров физических ресурсов в одной микроЭВН. Для каждого физического ресурса г^еИ введём множество состояний кото-

рые соответствуют со екта.

стояниям физического ресурса из эскизного про-

•Как было отмечено, микроэвм идентичны между собой и в кажду*

гичная—0£^—Из—этдаг-о—следует^—что—набору

„ = и множества их состояний различных кикроЭВ2 физических ресурсов и множества их и

^ - тъ _г> Положи]

также идентичны между собой: О, ^ j

К =И и 0,«П|=01. Исходя из идентичности микроэвм и ОС, для построения модели, без потери общности, можно принять 1Л = 1.

Обозначим через П={лк|к£К> некоторый фиксированный перечен реализуемых ФЗ. где К - множество номеров ФЗ. Обозначим через о =(Я.Й) - граф задач, где ИйЫ! - множество информационных связе „ежду ФЗ. Как отмечено в первой главе, 0 задает частично упорядо. ченную последовательность решения задач. Поскольку перечень зада' фиксирован, то определим моделируемый ВП как частный. Для каждо задачи тг^П введем множество состояний С, отвечающее определенны

в эскизном проекте возможным состояниям ФЗ.

Определим, что пространство состояний ВП в микроЭВМ есть де картово произведение множества состояний ФЗ и физических ресурсов

• С хС х. . .хС^хР^О^. . .

Введем переходы межд^ состояниями задач и ресурсов. Возможны переходы для каждого состояния ФЗ и каждого состояния физически ресурсов задаются с помощью графа переходов на основании данных полученных из эскизного проекта. Обозначим через СсСЛ граф пе реходов для множества состояний ФЗ я,, а через Б.сО.хО, - граф пе реходов для множества состояний физического ресурса г,.

Переходы между состояниями ВП могут совершаться при наступле „ИИ событий, множество которых оговаривается также на стадии эс кизного проекта. Данное множество состоит из двух непересекаюшихс подмножеств, одно из которых описывает внешние события, а другое

внутренние. Внешние события - это сигналы, поступающие в микроэвм извне и требующие обработки со стороны ОС. Внутренние события означают либо эапрос к ОС со стороны ФЗ на выполнение некоторых действий (например, передача сообщения), либо образование некоторых условий, от которых зависит поведение ОС. Определим, что в один момент времени может произойти только одно событие.

Замечание: Несмотря на то, что модель строится для одной микроэвм, благодаря введению внешних событий она описывает взаимодействие микроэвм между собой.

Обозначим через I множество внешних событий. Дополним это множество специальным событием которое означает отсутствие

внешних событий. Для описания динамики модели ВП введём функцию отображения 0

6:1хС хС х. . .хС хЭ хЭ X. . . хБ -*С хС х. . .хС хО хВ х. . . хО , 12 к 1 2 I. 1 2 к 1 2 С

где К - число ФЗ, а Ь - число физических ресурсов. Если зафиксировать некоторое входное событие 1е1, то при 1=1° отображение 0

описывает поведение системы в зависимости от внутренних событий, . .о

при 1*1 - - от внешних.

Таким образом, модель динамики частного ВП в СМВК описывается четверкой

<С, 5, I, е>, где С = С хС2х. . .хС^ 5 = 01х02х. . . хй^.

Проведём исследование модели динамики частного ВП. Множества состояний задач С^ изоморфны для всего множества задач и графы переходов С^ изоморфны друг другу с точностью до обозначения. Из этого следует, что в терминах теории автоматов изоморфные состояния всех задач образуют класс состояний. Физический смысл класса состояний заключается в том, что разные ФЗ, находящиеся в состояниях, принадлежащих одному классу, обрабатываются

ОС одинаковым образом, а значит, мощность класса не имеет принци пиального значения для функционального проектирования ОС. Из пос леднего утвеждения следует, что для построения модели динамики Е можно ограничиться одной ФЗ. Будем считать такую задачу типичнс или обобщённой ФЗ, которой присущи все особенности ФЗ, влияющие i проектирование ОС. Тогда описание таких особенностей задаст некс торый обобщённый класс задач, решаемых в СМВК и, в конечном итоге определит особенности ВП. Соответственно множество достояний обоб щённой задачи не будет зависеть от конкретного прикладного ВГ т. е. будет являться общим для определённого класса наборов задач.

При уменьшении множества ФЗ до одной задачи модель динамиь ВП будет задана как следующая четвёрка:

<с, Б, I, е>,

где С - множество состояний обобщённой задачи. Переходы этой зада чи из одного состояния в другое будут задаваться обобщённым графе переходов С;

в - функция отАбражения:

в: IxCxD *D х. . . xD -»CxD xD x. . . xD ,

12 L l 2 L

L - число физических ресурсов.

Основным преимуществом при переходе от частного ВП к обобшёь ному ВП является существенное снижение размерности модели.

В качестве формализма для реализации модели предложено вы£ рать сети Петри, приведено обоснование такого выбора. Пpoвeдe^ модернизация классического аппарата теории сетей Петри путём вве дения разноцветных фишек и соответствующего правила срабатываш переходов. Смысл введённого правила заключается в тон, чтобы пр срабатывании перехода сохранялся цвет фишек. Сохранение цвета поз волит проследить трассу фишки при её перемещении по переходам.

В диссертации предложено проводить построение моделирующб

сети Петри в два этапа.

На первом этапе построения моделирующей сети Петри вводятся состояния сети, отвечающие статической составляющей модели. Вводятся переходы между состояниями, соответствующие отображению 0 при 1=1°. Вводятся фишки, отвечающие физическим ресурсам и ФЗ.

На втором этапе построения моделирующей сети Петри вводятся состояния сети, отвечающие внешним событиям. Вводятся состояния сети, соответствующие внешним событлям. Вводятся фишки в количестве, равном числу внешних событий. Вводятся переходы между состояниями, соответствующие отображению 0 при 1*1°. Всем введённым фишкам присваивается цвет. Фишки, отвечающие ФЗ и физическим ресурсам, помещаются в исходные состояния.

| После построения доказывается корректность полученной сети Петри, т.е. доказывается, что для любого момента времени в ней:

1. сохраняется количество фишек, отвечающих ФЗ и физическим ресурсам;

2. при любой маркировке сети не существует тупиковых ситуаций, т. е. , либо имеется работоспособный переход, либо имеется «потенциально > работоспособный переход, приобретающий работоспособность после наступления соответствующего внешнего события.

Доказательство корректности проводится посредством изучения ■ множества достижимости сети Петри, т. е. изучения всех маркировок сети, которые возможны при работе сети Петри, исходя из фиксированной начальной маркировки.

В диссертации разработана следующая процедура получения перечня базовых процедур ОС на основании изучения моделирующей сети Петри:

1. Рассмотрим множество состояний внешних событий. Зададим, что каждому внешнему событию соответствует своя процедура обработ-

ки. В моделирующей сети Петри базовой процедуре, обрабатывающей 3-тое внешнее событие соответствуют переходы, для которых позиция, соответствующая з-тому событию, является входной.

2. Удалим из списка переходов все переходы, соответствующие модулям обработки внешних событий.

3. Рассмотрим множество состояний ФЗ. Зададим, что переход задачи из ^того состояния осуществляет одна процедура ОС, которой соответствуют все переходы, для которых }-тое состояние является входным. Из-за выполнения шага 2 в перечень переходов не- войдут переходы, обслуживающие внешние события.

На рис. 2 представлен пример моделирующей сети Петри для типичной ОС. Для неё доказано утверждение, что при любой допустимой маркировке сети Петри работоспособен не более, чем один переход. Если работоспособного перехода нет, то он появляется после появления фишки в состоянии 7. Также доказано, что при любых срабатываниях переходов сети всегда сохраняется число фишек, соответствующих ФЗ и физическим ресурсам.

Для данной сети Петри был получен список базовых процедур.

1. Процедура частотной обработки; ей соответствуют переходы 2е, 3е, 7*. 7е.

2. Процедура «генер'атор»ей соответствует переход О. . -

3. Процедура «диспетчер»; ей соответствуют переходы 1°, 1*.

4. Процедура «приёмник»; ей соответствуют переходы 2*. 2е.

3. Процедура «передатчик»; ей соответствует переход 3*.

6. Процедура «завершение задачи»; ей соответствует переход 4.

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

пред- и постусловия работы базовой процедуры.

В результате, предусловие и постусловие образуют для каждого алгоритма спецификацию, основное преимущество которой заключается Тз ее—формальшш_^_аписи. Поэтому дальнейшая разработка алгоритма может проводиться формальными методами. ~~ ~ ----——__

Для описания логики работы базовых процедур предложено использовать форнальный язык, основанный на языке разработки алгоритмов Дейкстры (ЯРА), проведена его необходимая модернизация.

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

В третьей главе разработана человеко-машинная процедура преобразования алгоритмов в программы на языке низкого уровня. В ходе решения данной задачи разработан метаязык для макро-11, который был выбран в качестве примера, разработаны процедуры преобразования алгоритма Ь программу на метаязыке макро-11 и разработан-препроцессор, реализующий трансляцию с метаязыка в ассемблер макро- 11.

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

Для преодоления семантического разрыва между языком разработки алгоритмов и языком низкого уровня в диссертации принят подход, связанный с введением промежуточного метаязыка. При использовании метаязыка процесс преобразования алгоритма в программу состоит из двух этапов: из алгоритма в метаязык и из метаязыка в программу. Главное преимущество введения метаязыка заключается в том, что процесс преобразования на каждом из этапов можно проводить на основе строгих правил и, тем самым, обеспечить однозначность преобразования алгоритма в программу. Однозначность преобразования, в свою очередь, обеспечивает корректность программы на языке низкого уровня.

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

1. Функциональные операторы, т.е. кие-либо действия над областями данных так и в регистрах общего назначения, а да.

2. Операторы передачи управления, относят операторы условного и безусловного ветвления, вызова и возврата из подпрограмм и прерываний.

Все специфические преимущества языка низкого уровня заключены в его функциональных операторах, поэтому они выбраны в качестве функциональных операторов метаязыка. Для организации передач управления функциональные операторы в метаязыке дополнены операторами управления высокого уровня, реализующими конструкции ветвления и организации циклов, причем данные конструкции высокого уровня совпадают по организации с аналогичными конструкциями языка разработки алгоритмов.

операторы, выполняющие ка-как в оперативной памяти, также операции ввода-выво-

К . этой группе операторов

На основании изложенного подхода в главе разработан синтаксис метаязыка.

Для установления взаимооднозначного соответствия между операторами метаязыка~и—операторами языка разработки алгоритмов проведён анализ соответствия фуш<цисшальных~~о^^ операторав_о£^ ганизации ветвления и циклов.

В принятом языке разработки алгоритмов единственным функциональным оператором является оператор присваивания. Этот оператор служит либо, для инициализации переменной, либо для изме"нения ее значения и имеет следующую форму:

<переменная> := f(х , * , ..., х , с. с , . .., с ),

12 п 1 2 m

где <переменная> - имя некоторой переменной, значение которой определяется оператором присваивания;

- имя переменной, значение которой определено ранее, i = 1 ... п; с^ - константа, j = 1 ... т.

Инициализация переменной на этапе трансляции производится директивами макроассемблера ..BYTE или .WORD. В тексте программы инициализация переменных с помощью данных директив должна иметь следующий вид:

<имя переменной>: .BYTE сначальное значенле> либо

<имя переменной>: .WORD «¡начальное значение>

Директива .BYTE используется для описания и инициализации переменной, для хранения которой отводится байт; соответственно директива .WORD используется для описания и инициализации переменной размером в слово.

Инициализация переменной, а также изменение её значения в ходе выполнения программы производятся с помощью команды MOV (для

переменных, описанных с помощью директивы .WORD) либо команды MOVB (для переменных, описанных с помощью директивы .BYTE).

В тексте программы данная команда должна иметь следующий синтаксис:

MOV(В) <источник>, <имя переменной:», где <источник> может быть либо непосредственным операндом (константой) , либо другой переменной.

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

Если выразить вышесказанное формально, то команду MOV(B) можно соотнести со следующими формами оператора присваивания языка разработки алгоритмов:

<переменная1> := <константа>,

либо

«переменная^ := <переменнаяг>, Логические и арифметические команды ассемблера соотносятся следующими тремя формами:

«переменная^ := f(«переменная^), «переменная^ := И «переменная^», «константа»), «переменная^ := £{ «переменная^, <переменнаяг>). В работе показано, что любой оператор условного ветвления можно представить в виде композиции элементарных операторов условного ветвления, которые имеют следующую структуру:

В -> о поп В - 51,2 П, где один из операторов может состоять из оператора «пропус-

тить».

Элементарному оператору условного ветвления ставится в однозначное соответствие следующая конструкция метаязыка:

[LONG]

SLr

$ELSE [LONG] SL

г

$ENDIF,

где <условие> - ключевое слове условия ветвления, AND и OR - вспомогательные конструкции для составления сложных логических выражений, LONG - ключ дополнительной возможности формирования перехода более, чек на 127 байт кода.

Базовой конструкции цикла, которая имеет следующий вид

do В - SL od

ставится в соответствие конструкция метаязыка DO-WHILE $DO

<вычисление условия> $WHILE <условие> [LONG] SL

$ENDDO [LONG],

где <условие> - ключевое слово условия ветвления, SL - список операторов.

На основании проведённого анализа была разработана методика преобразования алгоритма, записанного на языке разработки алгоритмов, в программу на метаязыке макро-11. Реализован препроцессор, осуществляющий трансляцию набора инструкций метаязыка в программу на языке макро-11.

В четвёртой главе проведён анализ использования модели функ-

ционирования СМВК и человеко-машинной процедуры преобразования алгоритмов в программы на языке низкого уровня. Сформулирована методология проектирования ОС, определены область и особенности её применения.

Методология предусматривает следующие основные этапы разработки ОС СМВК:

1. Изучение ТЗ.

2. Эскизное проектирование ОС.

3. Построение и анализ модели функционирования СМВК. Используя данные эскизного проекта, строится сеть Петри, реализующая обобщённую модель динамики ВП в СМВК, и анализируется её корректность. Процедура построения и анализа описана а главе 2 диссертационной работы.

4. Определение (на основании модели) перечня базовых процедур ОС и порядка их взаимодействия. Процедура выполнения данного шага также описана в главе 2. Результатом её выполнения является определение состава базовых процедур и порядка их взаимодействия.

5. Разработка спецификаций и алгоритмов работы каждой процедуры.

6. Доказательство корректности алгоритмов процедур.

7. Запись процедур на метаязыке. —

8. Трансляция кода процедур с метаязыка в язык низкого уровня с помощью препроцессора.

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

ных ошибок в программе. Сравнение полученных программ базовых процедур двух ОС выполнялось по методу высеивания ошибок (так называемый нетод «меченых рыбок») на одинаковом наборе ФЗ.

В резуль^ал^я_эксперимента на 100 внесённых ошибок для ОС, разработанной с применением методолоРйиГ^ыло-^ргщущено 2 ошибки, а для ОС, разработанной обычными методами - 3. Численные значения вероятности отсутствия ошибок для ОС, разработанной с применением методологии и без неё, составили 0, 97 и 0, 96 соответственно.

Одной из особенностей метода высеивания ошибок является то, что необходимое значение вероятности отсутствия ошибок может быть достигнуто за счёт увеличения количества высеиваемых ошибок. Так для ОС, разработанной обычными методами, значение О,97 было достигнуто при увеличении длины серии до 200.

Полученные данные, при выбранной методике эксперимента сравнения качества, говорят о лучшей тестируемости программ базовых процедур ОС, разработанной с применением предлагаемой методологии, т. е. о том, что применение методологии позволяет получать программы ОС, которые легче проверить.

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

Разработанная методология обладает рядом особенностей:

не предусматривает использования готовых алгоритмов или программ процедур. С одной стороны, это увеличивает время разработки каждой новой ОС, но с другой стороны, только при таком подходе можно получить ОС с гарантированными параметрами качества;

- обладает свойством целостности. Это значит, что она поддерживает все стадии проектирования и реализации ОС, начиная с получения эскизного проекта и заканчивая выдачей программ;

- обладает свойством взаимосвязанности проектирования и реализации. Выходные данные предыдущих этапов являются входными данными для последующих;

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

- обеспечивает корректность алгоритмов относительно сформулированного эскизного проекта и эквивалентность программ алгоритмам.

ЗАКЛЮЧЕНИЕ

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

Получены следующие научные и практические результаты:

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

2. В рамках разработанной модели формализовано понятие корректности разрабатываемой ОС СМВК.

3. Разработаны процедуры построения и методы анализа модели динамики обобщённого ВП в СМВК.

4. Разработана процедура получения спецификаций базовых процедур ОС на основе модели динамики обобщённого ВП в СМВК. _____5111роведён анализ разработанной методологии, определены область применения и особе mKycijTTie^

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

ОПУБЛИКОВАННЫЕ РАБОТЫ ПО ТЕМЕ ДИССЕРТАЦИИ "'1. Дагурова Н. В. , Бугаев В. А. , Правиков Д. И., Власов В. Е. , Гронда О.В. Статико-динамическое управление вычислительным процессом мультимикромашинных управляющих комплексов. // Мультимикропро-цессорные информационно управляющие системы. Межвуз. сб. науч. трудов под ред. A.M. Ларионова. - М. :МИРЭА, 1990 г.

I

2. Правиков Д.И. Об одном подходе к проектированию специализированных операционных систем.// Вопросы кибернетики. Устройства и системы. Нежвуз. сб. науч. трудов под ред. Н. Н. Евтихиева. - М. : МИРЗА, 1991-г.

3. Правиков Д. И. Применение циклического контрольного кода.// Библиотека информационной технологии. Вьш. 5. Сб. ст. под ред. Г. Р. Громова. - М. :ИнфоАрт, 1992 г.

Личный вклад диссертанта в работе [1], опубликованной в соавторстве, состоит в разработке подхода к созданию управляющих структур данных ОС, реализующей статико-динамическое управление.