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

РГ5 ОД

На правах рукогт

МАЛИКОВА Лариса Вячеславовна

— РАЗРАБОТКА МАТЕМАТИЧЕСКОГО И ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ ДЛЯ ИССЛЕДОВАНИЯ ИСПОЛНЯЕМЫХ МОДУЛЕЙ С ИСПОЛЬЗОВАНИЕМ ТЕОРИИ АЛГОРИТМИЧЕСКИХ АЛГЕБР И УНИФИКАЦИИ АЛГЕБРАИЧЕСКИХ ТЕРМОВ --

Специальность 05.13.11 - «Математическое и программное обеспечение вычислительных машин, комплексов, систем и сетей»

Автореферат^

^диссертаций на соискание ученой степени - кандидата технических наук

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

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

Научный консультант:

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

Засл. деятель науки и техники, доктор технических наук, профессор Коричнев Л.П.

кандидат физико-математических наук, доцент Каширин И.Ю.

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

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

Ведущая организация: Московская государственная

академия приборостроения и информатики

Защита диссертации состоится 1 июля 1998г. в 10.00 часов на заседании диссертационного совета Д 063.92.03 в Рязанской государственной академии по адресу: 391000, г. Рязань, ГСП, ул. Гагарина, 59/1.

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

Автореферат разослан 1998 г.

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

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

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

В ходе работы были исследованы известные теоретические концепции анализа программ, в частности работы Р. Флойда, П. Наура, Ч. Хоара, Э. Дейкстры, Р. Андерсона, Ю.И. Янова, A.A. Ляпунова, В.М. Глушкова, Р.И. Подловченко, В.А. Евстигнеева, С.А. Нигияна, JI.O. Хачояна и др. Отмечено, что существующие теоретические формализмы анализа программ нельзя непосредственно использовать для анализа программ низкого уровня, поскольку они узко направлены, достаточно сложны, что не позволяет использовать их прикладным программистам, малоприменимы для автоматизации исследования программ, среди них не существует достаточно простого теоретического формализма, применение которого в чистом виде позволило бы исследовать исполняемые и объектные модули. При этом исследование программ, написанных на языках низкого уровня, не получило должной математической формализации, что привело к необходимости проведения исследований в этом направлении.

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

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

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

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

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

Научная новизна.

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

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

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

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

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

Результаты диссертации нашли отражение в реальной программе ЕТе$(, предназначенной для исследования свойств программ на языках низкого уровня.

Разработанные средства могут быть приняты за основу при создании спецпроцессоров ЭВМ и языкового инструментария низкого уровня.

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

Апробация работы. Основные положения диссертационной работы докладывались и обсуждались на Всероссийской научно-технической конференции «Современные информационные технологии в образовании», Рязань, 1996; Меж

дународном научно-техническом семинаре «Проблемы передачи и обработки информации в информационно-вычислительных сетях», Москва, 1997; 2-ой Всероссийской научно-практической конференции «Современные информационные технологии в образовании», Рязань, 1998; научно-технических конференциях профессорско-преподавательского состава Рязанской государственной радиотехнической академии, 1995-1998 гг.

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

Структура и объем диссертации. Диссертация состоит из введения, четырех глав, заключения, списка литературы и двух приложений. Основной текст содержит 162 страницы, в том числе 10 рисунков, 2 таблицы.

Список литературы содержит 82 наименования.

Основные результаты, выносимые на защиту:

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

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

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

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

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

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

В первой главе "Средства разработки и анализа программ для ЭВМ" выявляются основные проблемы и цели анализа программ, приводится обзор работ по теме диссертации, вводятся основные понятия и определения.

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

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

- сложность математических формализмов, требующих от программиста знания многих математических аппаратов, /

/

- возможность внесения ошибок на концептуально-логическом уровне проектирования,

- высокая трудоемкость применения методов повышения надежности,

- неполнота и неразрешимость многих формальных систем, используемых в качестве программных логик,

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

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

- сложность имеющихся формализмов не позволяет их реально применить в доказательствах правильности и оптимизации сложных программных систем.

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

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

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

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

Во второй главе "Формальный анализ программных модулей на уровне объектного кода" определяется формальная программная машина, выбранная в качестве базового математического аппарата для решения задачи анализа объектного кода программ.

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

Ть = <Мь КЬАЬРЬФЬ К>,

где М|. - алгебра элементов памяти с определенными на множестве ее элементов отношениями;

К[. - алгебра констант программирования;

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

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

Ф[ , - алгебры описания интерпретации соответствующих конструкций, исследуемых в 1?1. и А|________

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

ТА = <МА, Од, ФА>,

где МА - алгебраическая система элементов памяти,

Оа - алгебраическая система команд процессора (мнемокодов языка ассемблера),

ФА - интерпретация системы команд процессора.

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

МА = <Аш,От,КП)>,

где Ат - множество адресов элементов памяти,

С1т - сигнатура алгебры (набор операций, определенных на Ат),

11т - множество отношений над Ат.

Алгебраическая система элементов памяти позволяет описывать действия над элементами памяти или, более точно, над позициями исследуемого файла. Если сигнатура состоит из единственной операции «+», то любую область памяти - от отдельной ячейки памяти (байта) до сегмента и всей доступной области памяти - можно получить путем применения указанной операции ко множеству адресов базовых и производных элементов памяти.

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

Оа=<Ак, £}к, Як>,

где <АК, Ок> - алгебра команд (наборов команд или последовательностей команд) процессора,

Як - множество отношений системы команд процессора.

Алгебраическая система Од определяет как отдельные команды, так и их последовательности, составляющие конкретные программы.

Множество-носитель алгебры команд процессора представляет собой "базовые" и "производные" элементы объектного кода программы, т.е. множество-носитель алгебры команд процессора включает некоторое базовое подмножество А°ь элементы которого представляют собой отдельные байты и могут иметь значение от ОЬ до РРК. При этом базовый элемент из множества А0^ может являться, а может не являться командой процессора. Выделение подмножества А°к из множества-носителя Ак произведено с учетом характера исследуемой системы, а именно - программы низкого уровня.

Сигнатура Ок алгебры 0А представлена операцией «°» композиции команд процессора.

/ / /

Множество отношений системы команд процессора Лк представлено следующими составляющими:

"=" - отношение эквивалентности конструкций;

- отношение неэквивалентности конструкций; «>» и «<» - нестрогое вхождение одной конструкции в другую; «>» и «<» - строгие отношения вхождения; «<--»> - имеют общие составляющие; «1» - не имеют общих составляющих.

При композиции базовых элементов могут быть получены как отдельные команды, так и последовательности (наборы) команд.

ФА = < Аф, Оф, Яф > - алгебраическая система интерпретации: Аф - множество интерпретирующих элементов, Оф - сигнатура алгебры, Оф = {"}, где «°»- операция композиции. При интерпретации последовательности команд процессора могут возникнуть три случая:

1) выполнив команду, перейти на следующую;

2) выполнение команды определяет переход к последовательности команд, расположенных по заданному адресу, выполнение которых завершается возвращением к команде, следующей за исходной;

3) если признак результата удовлетворяет заданному условию, то перейти к команде по некоторому адресу, в противном случае выполнить следующую команду.

Алгебраическая система интерпретации ФА описывает интерпретацию команд процессора. Среди интерпретирующих элементов алгебры ФА определен базис:

Аф°={фо, ф1,ф2, Ф22>,

(Фо) = (Ф1) = (Ф2> = 2, (Ф 22) = 3.

Функциональный смысл элементов множества Аф° состоит в следующем: Фо'(™(0>фп0_ выполнить команду £ расположенную по адресу т( Г), а затем перейти к выполнению цепочки команд ф п}, где 1,^ = 0, 1, 2 ..., п = 0, 1,2, 22. Верхний индекс определяет порядковый номер интерпретирующего элемента, а нижний - функциональный смысл. На основе интерпретирующего элемента ф0 можно описывать безусловный переход. В этом случае первый аргумент равен ш( фп! * ) = е, что означает пустой оператор, а второй аргумент ф„ выполняет свою обычную роль, т.е. адресует цепочку команд, на которую необходимо перейти после обработки первого аргумента интерпретирующего элемента;

Ф11 ( т( ф„1^ ), ф„2к ) - выполнить цепочку команд ф „Л расположенную по адресу т( ф„/ ), а затем перейти к выполнению цепочки команд ф^, где ¡, }, к = 0, 1,2,..., п1, п2 = 0, 1,2,22;

Ф2' (т((ру'),т(ф2к))- если признак результата равен единице, то выполнить цепочку команд фи1, расположенную по адресу п^фь/); если же признак результата равен нулю, тогда перейти к выполнению цепочки команд ф„2 к, расположенной по адресу т( фп2к);

Ф221 (а, ш( ф„/ ), ш( фп2к)) - если выражение а принимает значение истина (а = 1), то выполняется цепочка команд ф„/, расположенная по адресу гп( ), а затем выполняется цепочка команд, на которую указывает аргумент ш( фп2к) интерпретирующего элемента ф22'; если же выражение а принимает значение ложь {а - 0), тогда сразу (не выполняя цепочки команд, расположенной по адресу т( фы )) осуществляется переход к выполнению цепочки команд фп2\ расположенной по адресу ш( фп2к). Интерпретирующий элемент ф22' является расширенной модификацией интерпретирующего элемента ф2'.

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

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

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

Для получения всех возможных трасс программы введена операция Ф(^п), позволяющая исходную программу Г разложить на п возможных трасс. Алгоритм действия операции Ф(Г,п) заключается в следующем.

1. Построить интерпретирующую последовательность, используя алгебраическую систему интерпретации команд процессора ФА = <АФ, С1Ф, Яф>.

2. Подвергнуть обработке полученную интерпретирующую последовательность с помощью алгоритма, получившего название Обрабполн.

3. Конец алгоритма действия операции Ф(£ п).

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

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

Операция Ф((", п), основанная на алгоритме Обраб_полн, позволяет получить формальную запись всех возможных трасс программы. Для получения ДНФ всех возможных трасс программы в виде

Ф^Г-Ч+Ь+Ь+.-.+Г»,

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

1) правило дистрибутивности (как слева, так и справа)

х*(у + 7) = х * у + х * ъ и

(у + г)*х = у*х + г*х,

где х,у,г- программные термы или группы программных термов;

2) правила поглощения х * х = {х}

и

X + X = X,

где х - программный терм или группа программных термов;

3) правило умножения на 1 х* 1 = 1 *х = х,

где х - программный терм или группа программных термов;

4) правило умножения на пустой оператор е х * е = х,

где х - программный терм или группа программных термов, е - программный терм, соответствующий пустому оператору;

5) правило внесения программного терма (группы программных термов) в тело цикла. Пусть х и у - программные термы или группы программных термов. Если х - у, тогда верно следующее:

Х*{У}=УЧУ} = {У}-

То есть, если программный терм (группа программных термов) х совпадает с телом цикла, который представлен программным термом (группой программных термов) у, тогда программный терм (группу программных термов) х можно внести в тело цикла, выполнив после этого операцию поглощения;

6) если известно условие продолжения цикла с предусловием, и оно не выполняется, тело цикла заменяется пустым оператором е:

^{х} = {е} = е,

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

е - программный терм, соответствующий пустому оператору;

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

{х}а=о = X,

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

8) если тело цикла (и с предусловием, и с постусловием) представлено пустым оператором, верно следующее:

где сг=1- условие продолжения циклов,

е-программный терм, соответствующий пустому оператору,

{}"- бесконечный цикл;

9) пусть есть программный терм (группа программных термов) х, который составляет тело цикла, и условие продолжения цикла а= 1. При этом х 1 а, то есть тело цикла х не влияет на условие продолжения цикла а. Тогда

^.{х} = {х}0=1 = (Г.

Использование операции 0*(f, п), где f - исходная программа, п - номер конкретной трассы, позволяет выделить отдельную трассу программы, что позволяет исследовать свойства отдельно взятой трассы программы, определить тупики на отдельных трассах программы, сравнивать возможные трассы программы и т.д.

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

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

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

у,(т) • х,(ш) • у2(ш) • х2(ш) •... ■ у„(ш), где у,(m) - обязательные составляющие, Xj(m), - необязательные составляющие.

Формула задает общий вид свойства программы. Рассмотрим наиболее характерные случаи формальной записи свойств программ:

(1) цепочка у^т) должна присутствовать, чтобы выполнилось свойство грограммы;

(2) цепочка Yi(m) должна отсутствовать, чтобы выполнилось свойство фограммы;

(3) цепочка у,(т) должна присутствовать перед (после) цепочка Yj(m), ггобы выполнилось свойство программы;

(4) свойство программы может быть задано в виде логической форму; Например,

где у;(ш), у,(т), ук(т) - цепочки операций,

V и л - символы операций дизъюнкции и конъюнкции соответствен!)

То есть, свойство программы выполнится, если выполнится или у;0 или у3(ш) и ук(т);

(5) свойство программы может быть задано выражением исчисления П] дикатов.

В диссертации рассматриваются примеры каждого из случаев (1)-(5).

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

При этом можно выделить три основных случая сходства термов ф< мальной структуры программы:

- классическое выделение унификатора,

- выделение унифицируемого каркаса,

- выделение термов программного инструментария.

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

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

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

Выделение термов программного инструментария является одной из фуг ций частичной унификации термов структур программ в том случае, если два пр

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

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

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

1) аксиома пустого присваивания

f=(x,x); = e;

2) аксиома о подстановке

f=(x, f,(...)); f=(y ,f3(... x ...)); в fl(y, fj(... f, (...) ..));

3) аксиома о перестановке независимых аргументов

fi (...) 1 fj (...) => fi (...); f/...) a f)(...); fj(...);

4) аксиома определения преобразующих операторов

f=(x, fi(...)) ±x = false илиf=(x, f,(...)) 1 x;

5) аксиома об эксплантации инвариантных аргументов

fx±fy => fx(. .fy...) = fy; fx (...e...);

6-7) аксиомы об условном операторе:

f=(Xi, false); Ыхь x,, xk) з f=(x, false); xk,

f-(x„ false); flf(x„ xk) = f-(x, false); e; = f_(x, false);

8) аксиома исключения единичного оператора:

fi(...); е; = е; $(...); = f,(...).

Если такая трансформация возможна, она выполняется, в противном случае принимается окончательное решение о несопоставимости.

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

Сертификационные испытательные лаборатории занимаются проверкой соответствия программного продукта, поступающего на рынок ПО, определенным стандартам. Например, Рязанский отдел Научно-информационного центра проблем интеллектуальной собственности (НИЦПрИС, г. Москва) использует следующие методики, в соответствии с которыми проводятся испытания.

1. Методика испытаний программных средств на соответствие реализаций основных функций документации.

Объединить полученные подстановки в единую композицию

Рис. 1. Алгоритм частичной унификации

Заменить не сопоставившиеся термы переменной

2. Методика испытаний программных средств на надежность.

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

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

В главе рассмотрены вопросы, касающиеся выполнения основных этапов исследования объектного кода программы, а именно:

a) получение начальных данных для исследования:

- начало загрузочного модуля,

- начало сегмента кода,

- начальные значения регистров;

b) эмуляция выполнения программы:

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

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

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

- выполнение различных переходов по тексту объектного кода программы: прямого внутри и между сегментами, и косвенного внутри и между сегментами,

- реализация обращений к подпрограммам и возврат из них.

Следует отметить, что теоретической основой разработки автоматизированной системы испытаний программных продуктов ETest послужила формаль-юя программная машина, ориентированная на исследование объектного кода трограммы. Алгоритмическая система элементов памяти используется для формального описания сканирования объектного кода программы. Алгоритмическая :истема элементов памяти МА предоставляет информацию (начало сегмента кода, гачало новой команды, начало подпрограммы и т.п.) алгебраической системе ко-данд процессора 0А. Алгебра интерпретации ФА используется для определения юзможных действий программы.

Архитектура системы ETest приведена на рис. 2.

Основной составляющей автоматизированной системы испытаний про-раммных продуктов, получившей название ETest, является программа-эмулятор Test, которая состоит из следующих подсистем:

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

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

TblMode выполняет реализацию способа адресации;

Автоматизированная система испытаний программных продуктов

ТЫОрег

ту iz

Table

С

\7

TblMod

К

Test

Т

CaseSeg

I I

Jl

zs

List

\ Испытываемый

и программный

продукт

□"

□ •

o-

Обозначения: основная часть

(подсистема) системы; вспомогательные части (подсистемы) системы; прямые двусторонние связи между подсистемами в системе;

косвенные двусторонние связи между подсистемами в системе;

прямые односторонние связи между подсистемами в системе.

Рис.2. Архитектура системы ЕТе&

Table выполняет настройку вспомогательных таблиц;

List - подсистема обработки динамических структур данных;

CaseSeg - подсистема, предназначенная для отслеживания префиксов сегментов.

Автоматизированная система испытаний программных продуктов реализована на основе системы программирования Borland С++ v3.1 с использованием эбъектно-ориентированных библиотек, поставляемых вместе с системой.

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

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

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

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

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

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

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

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

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

8. Получена базовая архитектура и основные принципы реализации тем исследования программ низкого уровня на основе анализа программной I темы ЕТеъг, реализованной с использованием результатов диссертации.

ОСНОВНОЕ СОДЕРЖАНИЕ ДИССЕРТАЦИИ ОТРАЖЕНО В СЛЕДУЮЩИХ РАБОТАХ

1. Маликова Л.В. Автоматизация испытания программных продуктов // временные информационные технологии в образовании: тез. докл. Всероссийс научно-практической конференции. Часть II. Рязань, 1996. - С. 11-13.

2. Баринов В.В., Коротаев А.Т., Маликова Л.В. Автоматизированное со: ние и сопровождение справочника испытания программных продуктов // Ин(] мационные технологии. Системы обработки и передачи информации. Межву: ский сборник научных трудов, Рязань, 1996. С. 107-109.

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

3. Маликова Л.В. Проблемы анализа исполняемых модулей // Информг онный бюллетень межвузовской научно-технической программы. Интеллекту: ная собственность высшей школы, М.: НИЦПрИС, 1996, №7. С.77-80.

4. Маликова Л.В. Программная реализация анализа исполняемых модуле Управление образовательным процессом в высших учебных заведениях: Мея зовский сборник научных трудов, Рязань, 1997. С. 38-42.

5. Калужин Р.В., Маликова Л.В. Системы гипермедиа и геоинформаци ные системы в образовании. И Управление образовательным процессом в выа учебных заведениях: Межвузовский сборник научных трудов, Рязань, 1997. С. 35.

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

6. Маликова Л.В. Некоторые проблемы анализа программных среден Проблемы передачи и обработки информации в информационно-вычислителы сетях: тез. докл. Международного научно-технического семинара. М.: 1997. 117-120.

7. Свидетельство об официальной регистрации программ для ЭЕ №950487. Программа для ЭВМ: Автоматизированная информационная сист< для исследования рынка интеллектуальной собственности. Зарегистрирован! реестре программ для ЭВМ.

8. Маликова Л.В. Понятие свойства программы при исследовании объе ного кода программы и алгоритм выделения команды в последовательности б // Современные информационные технологии в образовании: тез. докл. 2-ой В российской научно-практической конференции. - Рязань, 1998. С. 107-110.