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

& в Iii J ..

лаишпэдскиа ордена лепила и ордена (шушчскол ришции

ЗШОТОТЕШИЕШМ ИНСТИТУТ ¡ГШП1 В.И.УЛШНСЕА Ш-ШИА)

На прапад рукописи

МИХАЛЕВ Авдро!1 Геннадьевич

У£К №I.S2G.3

метода иерархической верикпслции мироигогранм

Специальность 05.13.13 - Вычислительные машнп, комплексы, систеин и сети

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

Ленинград - IS90

у , ,

- 'S £ J ^

Работа выполнена в Ленинградской ордена Ленина и ордена Октябрьской Революции электротехнической институте те ни В.И.Ульянова (Ленина).

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

доктор технических наук профессор Плотников A.B. Официальные оппоненты:

доктор технически наук профессор Неыолочнов О.Ф. каццвдат технических'наук ст. науч. сотр. Никищенков С.А.

Ведущая организация - Ленинградское научно-производственное объединение "Электрошаш".

Защита состоится " 20 " 1990 г. в ' часов

на заседании специализированного совета К 063.36.12 Ленин- . градского ордена Ленина и ордена Октябрьской Революции электротехнического института имени В.И.Ульянова (Ленина) по адресу: 197022, Ленинград, ул. Проф.Попова, 5.

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

Автореферат разослан ir?0 г. .

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

Анисиырв A.B.

ОЕ^АЯ ХАРАКТЕРА !С'Г! ПСА РЛШ'Ш •

Актуальность проблем. СовромешиГ, этап развития, науч-но-технпческого прогресса отличает необходимость интснагв-ного развития вычислительной техники, повипения со производительности, роста объемов производства средств вычислительной техники наряду с пошлиенкем качества ' рокзводиу.ого оборудования. В этих условиях особую остроту приобретает вопросы обеспечения надежности функционирования средств выделительной техники. При производстве СШ широко используется микропрограммное управление. Обеспечение правильности микропрограмм является необходим«« условие» издегягаго функционирования ЭШ как слояшой снстеш в целой. Такая необходимость возникает по той причине, что микропрограммы - один из низших уровней в иерархической организации ЗШ и ошибки, допущенные на этом уровне, оказывают серьезное влияние на надежность всей системы.

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

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

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

трудно осуцестшшо. Поэтому на практике приходится решать задачу отпевания шипшального поданояества тестов, выбранных по какки-лио'о критериям, чтобы вреия тестирования оказалось приеллешли, В результате этого неизбе.ию снижается достоверность получаемых результатов проверки. Строго говоря, в этом случае теряется гарантия правильности ([ункционирования шк-ропрогрш&ш, вследствие иазногзюсти проявления ошибочно;'! ситуации при неисследовашшх входных воздействиях.

Третий подход заключается в. использовании формальных математических истодов доказательства корректности шшропрог-раиш относительно ее функциональных спецификаций.' В пользу итого подхода говорит прежде всего тот (Такт, что при его использовании гарантируется правильность функционирования микропрограммы в диапазоне возможных значений входнцх данных, ограниченном функционально:: спецификацией. Ые'ида, использующие процедуру йориального доказательства правильности, объединены по^ названием методов вери-Т икацни.

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

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

Для достижения поставленной цели в ¡аО'ото решались следующие задачи;

- исследование существугаярк подходов к организации процесса верификации ишропрограш и анализ его специфики;

- выбор перспективного метода варкЛикацин программ и анализ возможности его приложения в области микропрограммирования;

- разработка методов вари;Т.икацпн микропрограмм, учитывающих специфические особенности микропрограммирования;

- разработка алгоритмов и.программ верн'икапии микропрограмм.

Метода; исследовании. /да решения поставленных задач в работе используются положения и метода математической логики, теории вцчиелителыз.'Х структур, теоретического программирования; в работе сочсгаптся фогмалыагй н содер:.-ателыз;;1 подход.

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

- предложена методика алгебраической веригикации, отл!гча»-шаяся возможностью формирования корректной микропрограммной реализации по эданоЛ алгоритмической спотгТ'Икапти Методика позволяет исключить этап доказагсльЬтва полученноЛ микропрограммной реализации.

Практическую ценность работы представляют.'

- разработанные методика и метод иерархической верификации;

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

Вне-пение результатов рлботт?. Осмоошго рсзул..гатк работы использовали в хоздоговорно." ¡лучно-нсследов.тгсльсхой работе, 1л;пол1ШК1!оГ: на ка'едрэ вычислительной техники Ленинградского электротехнического института имени Б.',!.Ульянова ■ (Ленина) и связанной с разработке)" программного обеспечения для диагностирования г,и'ро-вп-: модулей. Разработанные метод*» верификации и их нрогра'глая поддержка используется такте при создании си'стеш пропотаи правильности процедуршх :пи-саяиП программно - аппаратных комплексов.

' -Апробация рабогн. Основные положения диссертационно^ работы докладывались и обсугдались на сло,"уп"1С конференциях: .

- Всесоюзной конференции "Применение и реализация языка программирования Ада" (г. Рига, 1987 г.);

- Всесоюзной конференции "Перспективы развития техники радиовещательного приема, радиовещания, звукоусиления и акустики" (г. Ленинград, J988 г.);

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

Ата, 1988 г.);

т республиканской конференции ''Авточатизация технической подготовки и управления производством в приборостроении и машиностроении" (г. Чебоксары, 1968 г,);

- республиканской конференции "Повышение качества программного обеспечения ЭШ" (г. Севастополь1968 г.);

- XLiü областной конференции по узловым проблемам радиотех- . ншш, электроники и связи (г, Ленинград, Г96С г.);

г Xtl и JIU научно-технических конференциях профессорско-! преподавательского состава ЛЭТЙ имени В.И.Ульянова(Ленина) . (г. Ленинград, 1986 г.).

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

Структура и объем -работы» Диссертационная работа состоит из введения, четырех разделов с выводами, заключения» списка литератур« из 102 наименований И приложения..Работа содертит 110 страниц основного текста, 7 иллюстраций и 4 таблицы,

\ OCHOEHOS .СО^ЭДМЕ >А6(Ш1

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

. В. первом разделе диссертационно!: работы рассматривается

• место" верификации в жизненном цикле «икропрограйниого обеспечения, проводится срашеиие иетодоц-■ верификации с (/.етодани тестирования, анализируется специфика организации процесса

• ввря^инадш.иикропрограглл,• узбчняюг'ся- зедачи исследования.-. , .;

Тер*11™ "вериЗ.икация" имеет ста; с л установления с помощь» формальных математических методов соответствия описания реализации требуемого ачгоритма на языке микропрограммирования" его Лункциональной спецификации, Исходными данными для верификации микропрограмм является, во-первцх, спецификация микропрограммы, построенная по представленитд о ее делаемом поведении, и, во-вгорпх, сама микропрограмма. Метода верификации устанавливают условия, при которых микропрограмма соответствует своей Функциональной.спецификаций.

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

• Из-за схояести методов разработки микропрограмм к программ,! одним и'з возмо.т&х путей решения зада1?!! создания корректного микропрогр.1!.с'jtoго обеспечения является перенос соответственно: методов из области программирования в сФеру микропрограммного управления. Однако, микропрограммирование . обладает .специ''ическк.1иг;0с0бешюс.тпыи, анализ которых приводит к н.овш, характерна.! для этой области, методам обеспечения правильности.. 'Cncnîi''i-геа постановки задачи герн'и-кащш микропрограмм волана тем,, что б настоявшее время- мик-. ропрограммирование- используется в двух основшх направлениях:

- реализация алгоритмов управления,-ранее реализуемых программно; •' -эмуляция.. ■

Близость сеыантик програш и микропрограмм, а также лидирующее положение методологии программирования обуславливав? перенос в область микропрограммирования методов проектирования, испольэуешх в сг-ере разработки программного обеспечения. Так, в среде разработчиков микропрограмм все активнее используются языки микропрограммирования высокого уровня (ЯШШУ), заимствующие из языков программирования управляющие конструкции, присущие шсокоуровневш языкам. Такая тевденция создает предпосылки для аксиоматизации языков микропрограммирования и использования в микропрограммировании техники верификации програш, В это и случае цикропрог-раша снабзсается функциональными спецификациями, выраженными в логике предикатов первого порядка, и проводится доказательство правильности одним из известных в программировании методов верификации.

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

В качестве спецификаций в этом случае выступает, исходный алгоритм, выраженный в терминах эмулируемой ЭШ (алгоритмическая спецификация) и требуется доказать, что он корректно реализован в виде микропрограмм.

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

Во-первых, тенденция использования микропрограмнирова-

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

Во-второе, широко практикуемое прнткн'ле :.^лцог,гогр»"м-мпруемьх устройств для онулаиии ЭЗГ.5 ставит задачу поиска истодов доказательств правильности микропрогрЕИслюР. реализации относительно алгоритмической спецп'икации, то ость когда делаемое поведение кикропрогрокш представлено не как совокупность услови!;, которым долгий удовлетворять входные и виходше данкне ц-нкроярограинн, а в виде алгоритма обработки команд эмулирует;: £3.1.

Во втором разделе диссертационной работы исследуется применение метода верификации алгоритмов Э.£еР.кстри-Д.Гриса при верификации микропрограмм. Метод Э.ДеЯкстрц-Д.Гриса основан на тактике обратного прослеживания и понятии слабейшего предусловия. Для любого оператора Л и любого предиката Я , который олиенвзэт ожцдаеь«кй результат вкполнения этого оператора, слабейшее предусловие представ-

ляет собой млояеетво всех состояли;':, для коток г,: штюлнолт^ оператора $ , начашееоя в таком состоянии, обязательно закончится через конечное время в состоянии, удовлетворял!¡ем постусловию Я .

Анализ конструкциГ. правления я структур даншх наиболее риспр'осгранспшгх ягпков микр/опрограчмиропанил л:сокого уровня позволяет сделать к:вод, что тгаэмо.-шости истода о.Дейнстрн-Д.Грнса полностью покгтег.эт спсцитш:у Я ¡ПЗУ и позволят- строить эМектиЕНке сясгоин юври^икаиаи илкропрог-рамм, представяешэлс на таких лггках. В диссертационной работе в .начест-пе основт'Л проблем:, пари"«нации микропрограмм в! делена задача нерарличоско:": вер:г/шса;ии.

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

- уровень гаифопрограишфуемоР. ' »гашиш (игструиепталытя

- в -

шина);

- уровень эмулируемой ЭШ (целевая машина).

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

Задача иерархической верификации микропрограмм ставилась, например, в работах Леви, Маркуса с соавторами. Ими была создана система -32>1/,5> , в которой использовался метод индуктивных утверждений Р.<1лойда. Но метод Р.Флойда не обладает преимуществами аксиоматической логики Хоара и метода обратного прослеживания, и поэтому проигрывает, в трудоемкости проведения верификации и сложности построения систем верификации на его основе.

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

Исходными данными для выполнения действий по предлагаемому методу являются:

- описание алгоритма обработки команда на уровне целевой папины;

- микропрограмма, которая является описанием алгоритма об-, работки команд на уровне инструментальной машины}

- таблица отображения объектов целевой машины (ЦМ) в объекты инструментальной машины (ИМ). Таблицей отображения определяется какими объектами микропрограммного уровня реализуются структурние единицы Ц!.5.

На первых этапах применения метода осуществляется доказательство правильности алгоритма обработки команд ЦМ. Для . этого:

- формулируются (Ьункциональние спецификации алгоритма обработки коыавд ЦЕЛ а

- вычисляется слабейшее предусловие алгоритма;

- проверяется соответствие вцчислешгого слабейшего предусловия и заранее сформулированного предусловия алгоритма.

В случае обнаружения ошибок в описании алгоритма или его функциональной спецификации, осуществляется их коррекция

и повторенне перечислении действий.

Следующий этап выполнения метода - получение спецификаций для микропрограмм;. Спецификации этого уровня дол::Лш быть адекватны спецификациям с учетом таблицы отображения. Для этого применяется функция тар отображения логических в! хранений, составлявших спецификации в логические выражения, определяющие спецификации микропрограммы. В об;;;ем случае применение функции тар означает контекстно-зависимую подстановку в логическое выражение ¡идентификаторов объектов микропрограммного уровня вместо ндента" икаторов уровня описания 1Щ.

В таком применении логические вградения В1 ¡ступают в роли средства, позволягацего вкразить в единообразной форме требования, общие для обоих уровпе'1 описания. Тем самим достигается соответствие микропрограмм требованиям, которгм удовлетворяет алгоритм ¡"ункционнрования IV,I. После перевода функциональних спецп • лкцци:: на уровень Ш проводится верификация микропрограмм» по методу Э.Дейкстрн-Д.Гриса. Успешное окончание вера'икации показывает корректность микропрограммы относительно описания алгоритма Функционирования ЦМ.

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

Однш из вадних понятий иерархической верификации является понятие уровне!! абстракции и декомпозиции. Применительно к верп'икации в работе дастся следующее трактование отих терминов.

Анализируемое проектное решение разбивается на уровни абстракции и декомпозиции в соответствии с многоуровневой структурой процесса проектирования. Эту структуру можно рассматривать как по вертикали, ■ так и.по горизонтали. Уровни по вертикали (от уровнч постановки задачи с постепенной ее конкретизацией до уровня кодирования) являются уровнями абстракции. Уровни, различающиеся по детальности описания в рамках одного уровня абстракции - уровни декомпозиции. Уровни

абстракции.различается ие^ду собоГ: уровнями объектов, используемых при описании проектного решения в ранках, каедого из них, то есть уровень абстракции задается типами дашшх, используемых в описании. Изменение уровня абстракции обязательно приводит к изменению используеш:х типов данных. Если проектное решение разбивается на отдельные компоненты без изменения типов данных, следует говорить об уровнях декомпозиции.

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

Определяя понятие "тип данных", примем формулировку, ■ предложешзую в работах А.В.Замулша: тип даншгх определяет множество значены!! посредством множества операций. Корректное использование операций предполагает описание их синтаксиса и семантики на некотором формальном язкчее. Наибольшее распространение в качестве Нормального обосногания и. инструмента спецификация типов .данных получил алгебраически;'; подход. Основные понятия отого подхода' связаны с понятиями алгебра, ее сигнатуры и основы,

Терлшюы "основа" определяется множество дашщх, принадлежащих специфицируемому типу. Сигнатура 21 является формальной записью синтаксически свойств операций, допустимых над данными, принадлегдщт*. основе алгебры.-Задание семантики операциям, определяема! сигнатуроГ. 2 , приводит к 2-алгебре Л.

Опираясь на алгебраическое обоснование концепции типов данных, можно утверждать, что соответствие двух алгоритмов, представленных на разных уровнях абстракции, иогзет быть достигнуто соблюдением определенного соответствия-ые:эду двугл алгебрами, которые являются /термальными записями свойств соответствую^« да.?, типов дашшх. Исходя из общей проблемы. создания корректного микропрограммного обеспечения, при иерархической разработке микропрограмм целесообразно поставить задачу получения корректно!! микропрограммы. по образу, .

в качестве которого выступает исходний алгоритм-спецификация.

Доказав известными методами (для это» цели предлагается использовать метод верификации Э.Депкстры-Д.Гриса) правильность алгоритма на верхнем уровне абстракции, где он имеет менее сложную запись, становится возможным получение корректной микропрограммы без применения на микропрограммном уровне традиционных методов верификации. Ста посылка ле.тлт в основе предлагаемо/i в диссертационной работе методики алгебраической верификации микропрограмм. Исходил.« данными являются: алгориты-спецн"лкацил, записанный в соответствии с (Термальными правила!,¡и языка верхнего уровня абстракции; описание языка микропрограммирования, на котором ведется разработка микропрограммно!! реализации, и соответствующий шсшему уровню абстракции.

Пусть имеется ZI-алгебра AI, определяющая уровень спецификации, и алгоритм' «S(ZI -AI), представляющий собой собственно алгоритм-специ'-икацда. Пусть проведено доказательство ,правильности этого алгоритма относительно предусловия Q ' и постусловия Я , то есть истинно утверждение

(Q(SM/J} S(Zi-Ai) [R(Zl-Ai)}

Пусть имеется так;яг ¿2-алгебра А2, определяющая уровень микропрограммной реализации.

Лля успешного пу.плспошш методики необходимо установить определенное соответствие ысццу алгебрами AI и А2, обеспечивающее переход от алгоритма-специ'икации к алгоритму- реализации. В общем случае возмогло наличие однозначного соответствия, удовлетворяющего, например, определениям гомоморфизма,. изоморфизма мезду двумя алгебрами или редунта алгебры. Однако, к.чк правило, однозначное соответствие мезду операциями и данными двух разных уровне;! абстракции зафиксировать не удается, что подтпорлдается, в частности, попытками применения концепции алгебраического подхода при верификации трансляторов.

По этоИ причине необходимо введение некоторой промежуточной алгебры Zl'-AI, которая получается из алгебры ZI-AI путем выполнения определенных преобразований. В ка-

честве таких преобразований может выступить изменение арности некоторых операций и, возмогло, добавление новкх знаков операций. Скисл выполнения подобных преобразований, состоит в стремлении получить из алгебры ZI-AI алгебру Zl'-AI, в которой при прекних основах изменению подверглась только . сигнатура. Кроме того, к алгебре ZI -AI предъявляется еще одно требование: она долгла быть связана с результирующей алгеброй Z2-A2 взаишо-однозначнш соответствием, то есть преобразование Zl'-AI - Z2-A2 должно выполняться' при сох-' ранении сигнатуры, только изменением основ. Если использованные преобразования позволяют достичь искомого соответствия, возможно выполнение следующего этапа методики.

Полученные соответствия допускают преобразование алгоритма 5l ZI-AI) в алгоритм «SlZl'-AI) с учетом соотношений между ZI-AI и EI'-¡VI. В свою очередь, соблюдая соответствие между Zl'-AI и Е2-А2, алгоритм • £( XI '-AI) преобразуется в £(. Z2-A.2]. Последний, алгоритм сохраняет ■'. структуру и функций исходного- мгоритма-споцификацпи, но * . уне оказивается запнсашпхи с применением типов данных, используемых в языке микропрограммирования. Таким образом, в результате действий, обусловленных г.олучешшыи соотнове-1 ниями мезду исходной, промвя^угочной и результирующей алгеб-. рами, итоговая шкроярограшла оказывается сконструированной.: по своей спецификации. То. есть справедливо соотношение:

(О №-Ai)) 5(ZZ -42) ¡Rfn-Af)}

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

' В четвертой разделе диссертагионкоГ работ!' рассмотри- • • вается организация систем; cepir икании микр0прагп:>!.а£, рогш.и- ■• зуюцей метод'.'вери*икации Э.Дейкстр.'-Д.Грнса. Рассмотрена' реализация программной систем»; позволяйте? прсво.-чгзь верификацию .ациклических ¡.'.икропрограм.:, •продстпвлс^'З'Х' па'под- -' . множество языка щкропрогр^л:ирбшшш- впе.окогр уровня. МШШ1У. Основидаи .кошоиеотрзли' спст.еж являпт-ся пт.огга;.с.х!'. начисления слабеПшего,-предусловия опс-рттора.Я*.;РХУ и ynpor;e- .

кия логических выражений. Описывается каздый из компонентов системы, приводятся оценки возмо.тностей програм; ¡ной системы верификации. Данная программная система написана на языке программирования Паскаль и работает под управлением операционной системы PC-DOS версии 3.30 на персональных компьютерах, совместимых с 1Ш PC.

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

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

''.",■ \ ССНОВШЕ ВИВ0Д1 И РЕЗУЛЬТА'Ш РАЮТЫ

В диссертационной работе получены следующие основные научше и практические результаты:

1. Показана ■ возможность' применения метода Э.ДеПкстры -Д.Гриса верификации алгоритмов для доказательства правильнос-тимнкропрограмм, представленных на. языках микропрограммирования' высокого уровня. '."..•'•.,•

2. В качестве основной проблем! верификации'микропрограмм выделена задача иерархической верификации.

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

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

4. Предложена методика алгебраической верификации, отличающаяся позлюжносз ьо (1хрмирсранил корректной микрс'программ-ноч реализации по заданной алгоритм 1ческс" спецификации. Методика позволяет исключить :эгап доказательства полученной микропрограммно!} реализации.

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

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Аникин A.B., Шхалев А.Г., ХохловскиР В.Н. В змояностн языка Ада как языка спецификации вычислительных систем // Применение и реализация языка програмлирорения Ада:Тез. докл. Всесоюзно? науч. конф.- Рига: ЛГУ, 1987.- С.76-77.

2. Михалев А.Г., Хохловский В.Н. Мэтоды герифлкации при автоматизации проектирования микропрограгнируемых устройств// Автоматизация техн. подготовки и управления пр-вом в приборостроении и машиностроении: Тез. докл. респ. нау«н"-практи-ческой конф.- Чебоксары: ЦНТИ, 1988.- С.59-63.

3. Аникин A.B., Шхалев А.Г., Хохловский В.Н. Верификация проектов цифровых устройств- альтернатива их тестированию // Изв. ЛЭГИ: Сб. науч. тр. / Ленингр. электротехи. ин-т им. В.И.Ульянова(Ленина).- Л., 1968,- Вып.394.-С.33-37.

4. Михалев А.Г., Хохловский В.Н. Использование формальных методов при доказательстве правильности проектов цифровых устройств // Перспективы развития техники радиовещатель-, ного приема, радиовещания, звукоусиления и акустики: Тез. дока. ХХП Всесоюзной научно-технической кенф.- Л.,'1988.'-

С. 177

' 5. Михалев А.Г., Хохловский В.Н. Доказательство правильности микропрограмм // Проблемы вычислительной математики и автоматизации науч. исслед.: Тез. докл. П Респ. конф.- Алма-Ата: Изд-во "Наука", 1988.- Т.З.- С.60'.

6. Аникин A.B., Михалев А.Г., Хохловский В.Н. Верификяиия проектов вычислительных устройств на основе определения слабейших предусловий // Электронная техника. Сер. Упр. качеством, стандартизация, метрология, испытания.- 1988,- Вып.5(132). -С.58-69.

?. Шхапев А.Г., Плотников A.B., Хохловский В.Н. Два подхода к организации процесса верификации микропрограмм // Проектирование вычислитеиьимс средств: Трз. докл. Веееевзн. тщпн.~ техн. нснф.- Каунас, I9Ö9.- С. 10-11.

Подп. к печ. 16.02.90. M-I5526 Формат 60x84 I/I6 Офсетная печать. Печ,л. 1.0; уч,-иэд.л. 1.0, Тираж 100 экз. Зак. № ВЪ . Бесплатно

Ротапринт ЛЭТИ 197022, Ленинград, ул.Проф.Попова, б