Введение к работе
Актуальность. Одной из основных проблем технологии программирования является проблема обоснования надежности программ на основе математического моделирования и математических методов. Эта проблема приобретает особое значение в связи с внедрением в практику параллельных вычислительных систем, информационно-вычислительных сетей и ввиду большой сложности создаваемых для них параллельных программ. Средства параллельной вычислительной техники активно применяются, в частности, при проведении научных исследований, характеризующихся большим размером обрабатываемых данных, требующих высокой скорости и надежности обработки.
Формальная верификация посредством формального доказательства позволяет устанавливать присутствие требуемых свойств программы для всех допустимых этой программой выполнений. Для асинхронных параллельных систем (АПС) она является почти единственным способом анализа требуемых свойств относительно заданных предусловий, из-за сильной недетерминированности таких систем.
Основным подходом к анализу корректности АПС является подход, при котором верифицируется не сама АПС, а ее спецификация (формальная модель). При этом осуществляется сведение анализа требуемых свойств АПС к исследованию свойств ее формальной модели, для которых уже известны методы анализа. Существует потребность в логической формальной модели, позволяющей верифицировать как трансформационные, так и реагирующие АПС, при этом устанавливать наличие свойств относительно заданных предусловий, а также исследовать АПС с произвольным числом состояний. Для такой модели должны быть разработаны методы верификации (методы по-спроения логических условий корректности). Наличие таких средств может служить основой для достаточно общего подхода к получению логических условий корректности АПС, т.е. для-сведения верификации к доказательству истинности логических формул. Таким образом, проблема разработки подхода к верификации АПС, предполагаю-цего выбор формальной модели и разработку методов ее верификации, является актуальной.
Целью работы является разработка подхода к ве-эификации (к построению логических условий корректности для загайного списка свойств) АПС, использующего в качестве формальной
модели L-программы, применявшиеся ранее для описания операционной семантики параллельных языков программирования.
Состояние проблемы. Часто, под верификацией трансформационных АПС понимается формальный анализ следующих свойств: частичная корректность в смысле Хоора; завершав-мость; отсутствие тупиков; а также тотальная корректность, определяемая пересечением всех вышеперечисленных свойств. Верификация реагирующих (реактивных) АПС состоит в исследовании таких их свойств, как свойства достижимости дедлоков и лайвлоков, справедливости, реагирования и родственных им свойств. Фундаментом верификации является логика, формальный язык логики, а также формальные модели и методы. Верификация трансформационных АПС обычно сводит анализ их свойств к доказательству истинности условий корректности в виде логических формул.
В отличие от последовательных программ проблема Еерифика-ции трансформационных АПС менее изучена, нет достаточно общего подхода к получению условий корректности АПС в связи с большим разнообразием типов АПС. Основой такого подхода для последовательных программ является логика Хоора, с помощью аксиом и правил вывода задающая определение семантики синтаксических конструкций языков щгаграммирования и метод генерации условий корректности. Но аксиоматика Хоора в общем случае не может служить основой для генерации условий корректности АПС, так как она ориентирована на семантику последовательных программ.
Основным подходом к обоснованию корректности реагирующих АПС, является подход, при котором исследуется (верифицируется) ее формальная модель. Самой абстрактной из изеєстшх формальных моделей являются системы переходов. Непосредственное применение систем переходов для анализа свойств АПС в общем случае невозможно из-за алгоритмической неразрешимости таких проблем, как проблема достижимости, проблема останова и др.
Представительными из числа широко распространенных формальных моделей являются сети Петри, взаимодействующие последовательные процессы Хоора, временные логики. Но, к сожалению, сети Петри и взаимодействующие последовательные процессы в общем случае не позволяют анализировать частичную корректность АПС, а также другие свойства относительно заданного предусловия. Это происходит потому, что предусловие может быть представлено мно-
кеством наборов данных (возможно бесконечным), а представление данных и их преобразования затруднено в этих моделях. Средства верификации на основе временных логик достаточно сложны в применении и используются для анализа реагирующих АПС (главным образом с конечным числом состояний).
Научная новизна. В результате проведенных исследований обосновано применение формальной модели L-програш для верификации АПС. При этом имеется в виду верификация, устанавливающая частичную корректность АПС относительно заданных пред- и постусловий, а также присутствие других свойств относительно заданного предусловия. На- основе L-программ разрабатывается единый подход к верификации как трансформационных, так и реагирующих АПС.
Для произвольной L-программы, рассматриваемой как система переходов, предложены алгоритмы построения логических формул, выражающих, отношение перехода Т, множества состояний post, непосредственно достижимых из заданного множества состояний, множества состояний pre, непосредственно предшествующих заданному множеству состояний, множества неподвижных точек хіх, множества заключительных состояний fin, множества состояний Ct, в которых возможен переход х, и другие.
С помощью этих формул, а также таких понятий, как инвариант и траектория, для L-программ формулируются логические условия корректности АПС.
В отличие от подхода на основе временных логик, который состоит в проверке свойств либо множества вычислений, либо дерева вычислений, предлагаемый подход заключается в проверке сеойсте пар состояний, связанных отношением перехода.
На основе L-прогрзмм, а также формулируемых для них условий корректности, для класса потоковых, аннотированных в смысле Хо-ора АПС получены алгоритмы построения условий корректности (корректность определяется как частичная корректность и нетупикс-вость) в виде логических формул первого порядка.
Практическая ценность. Результаты диссертации, полученные для L-программ,могут быть применены к конкретным классам АПС посредством сведения верификации АПС к верификации моделирующей L-программы. На этой основе могут быть получены алгоритмы построения условий корректности конкретных
классов аннотированных АПС. Причем такие условия корректности могут быть значительно упрощены по сравнению с общим случаем. Таким образом, эти результаты могут применяться при построении блока генерации условий корректности в автоматизированных системах верификации АПС из различных проблемных областей.
Предлагаемые методы позволяют устанавливать свойства не только отдельных АПС, но и целых их классов, а также исследовать АПС с произвольным числом состояний.
Для конкретного класса АПС, класса потоковых АПС, разработан логический язык спецификаций, открытый для введения новых понятий. На основе теоретических результатов диссертации полу-ченны алгоритмы построения условий корректности потоковых систем в виде формул первого порядка, разработанного языка спецификаций. При этом корректность определяется, как частичная корректность и нетупиковость
Публикации и апробация работы. По теме диссертации опубликовано 8 работ. Основные положения и результаты диссертации обсуждались на семинарах в ВЦ РГУ и на международных семинарах "їогтаї Models ot Concurrency: Logics and Semantics" (Переславль-Залесский, 1992) к "First Internati-nal Workshop on High Speed Networks Open Distributed Platforms" (Санкт-Петербург, 1995).
Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения, списка литературы (75 наименовний) и трех приложений. Осноеной текст занимает 133 стр.
