Введение к работе
Актуальность темы. Постоянное развитие аппаратной и программной базы компьютеров, характерное для нашего времени, позволяет применять их для решения все более сложных типов задач. По мере усложнения создаваемого программного обеспечения растет значимость и необходимость в подсистеме спецификации как компонента среды разработк .
и программного обеспечения. Используя эту подсистему, заказчик и разработчик программного обеспечения могут формально описывать потребительские свойства программного обеспечения, проверять их непротиворечивость еще до начала реализации-,- а также контролировать соответствие реализации спецификации. Подсистема " спецификаций становится особенно необходимой при разработке распределенного программного обеспечения, поскольку в нем используются механизмы взаимодействия параллельных процессов с довольно сложной семантикой.
В настоящее время специфиация из вспомогательного средства превратилась-в отдельную дисциплину, для которой характерны свои собственные языковые средства и методы верификации. Основным компонентом системы специфиации является, как правило, тот язык спецификаций, ,. на котором записываются потребительские свойства программного -обеспечения. Этот язык должен, с одной стороны, быть достаточно удобным и понятным для программиста, реализующего специфицируемое программное обеспечение, а с другой стороны он должен быть достаточно мощным для того, чтобы выразить на нем основные интересующие заказчика свойства программного продукта. Язык должен также иметь формальную семантику, позволяющую проводить автоматическую верификацию записанных на нем свойств.
В настоящее время разработано большое количество языков, использующихся для спецификации свойств программ. Однако большинство из них не удовлетворяют перечисленным выше требованиям и
являются либо недостаточно выразительными, либо трудными для понимания. Для разработки языка спецификаций, удовлетворяющего этим требованиям, необходимы исследования, включающие в себя анализ существующих подходов, принятых в системах спецификаций, а также анализ математических формализмов, использующихся для записи и верификации свойсов программ.
Основные пели работы.
анализ существующих подходов и методов, применяющихся в теории и практике создания систем спецификаций программного обеспечения, особенно тех из них, которые используются для спецификации распределенных программ, то есть программ, состоящих из последовательных компонентов, выполняющихся параллельно, и взаимодействующих друг с другом;
анализ существующих формальных математических методов, использующихся для анализа поведения программ и пригодных для записи наиболее важных свойств распределенных программ и автоматической проверки их выполнимости;
разработка, на основе проведенного анализа, языка спецификаций свойств распределенных программ, который бы отвечал сформулированным выше требованиям;
создание модельной версии подсистемы спецификаций, основу которой составляет разработанный язык спецификаций и которая позволяла бы автоматически верифицировать записанные на этом языке свойства распределенных программ.
Научная новизна.
В диссертации на основе детального анализа проблематики построения систем спецификации свойств распределенных программ и выбора формализма, позволяющего автоматически верифицировать заданные на нем свойства распределенных программ, предложены новые методы решения основных проблем, связанных с разработкой языков спецификаций для поддержки разработки распределенных программ. Новизна подхода заключается в том, что на основе проведенного
исследования разработан язык спецификаций, для которого дано два формальных описания семантики: пользовательское - в терминах цепочек состояний, проходимых программой, и служебное - в терминах формул на языке темпоральной логики. Доказана эквивалентность этих двух описаний.
Практическая значимость. Работа выполенна на кафедре автоматизации систем вычислительных комплексов, в Лаборатории вычислительных комплексов в рамках прокта по созданию интегрированной среды разработки и анализа распределенного программного обеспечения DYANA и поддержана грантом РФФИ п 95-01-01590а. Реализованная подсистема спецификаций содержит транслятор с языка спецификаций в специальное представление, позволяющее автоматически выполнять верификацию, а также программные модули, осуществляющие проверку выполнимости спецификации и ее истинность для конкретной реализаіши распределенной программы на языке реализации системы DYANA. Язык спецификаций имеет синтаксис, сходный с языком реализации и не требует от реализатора никаких дополнительных знаний в области математики. Система DYANA с реализованной подсистемой алгоритмического анализа демонстрировалась на международной выставке CeBIT в Ганновере (Германия) в 1995 и 1996 годах. Внедрение работы планируется продолжить в 1996 году.
Полученные результаты позволяют качественно улучшить процесс создания распределенного программного обеспечения, создаваемого в системе DYANA, а именно формализовать его на самых ранних этапах проектирования, проверить непротиворечивость требований к нему и автоматически проверять соответствие программы спецификации на всех этапах реализации.
Достоверность результатов подтверждается успешным прогоном тестовых примеров, которые были разработаны для проверки системы спецификации.
Апробация и публикации. Результаты работы докладывались на межкафедральном семинаре на факультете вычилительной математики и кибернетики, на научных конференциях. По теме диссертации
опубликованы две работы, полно отражающие основные научные результаты диссертации. Прикладные результаты представлены также в ряде научных отчетов по НИР, ведущимся в Лаборатории вычислительных комплексов ВМК МГУ.
Структура и объем диссертационной работы. Диссертация состоит из введения, пяти глав, заключения, списка литературы (включающего 66 названий) и занимает 141 машинописную страницу.
