WWW.OS.X-PDF.RU
БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА - Научные публикации
 

Pages:   || 2 | 3 | 4 | 5 |   ...   | 6 |

«МЕТОД И МАШИНА ЛОГИЧЕСКОГО ВЫВОДА ДЛЯ ФОРМАЛЬНОЙ ВЕРИФИКАЦИИ ПАРАЛЛЕЛЬНЫХ АЛГОРИТМОВ ...»

-- [ Страница 1 ] --

Федеральное государственное бюджетное образовательное учреждение высшего

профессионального образования

«Вятский государственный университет»

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

Чистяков Геннадий Андреевич

МЕТОД И МАШИНА ЛОГИЧЕСКОГО ВЫВОДА ДЛЯ ФОРМАЛЬНОЙ

ВЕРИФИКАЦИИ ПАРАЛЛЕЛЬНЫХ АЛГОРИТМОВ

05.13.11 – Математическое и программное обеспечение вычислительных машин,

комплексов и компьютерных сетей;

05.13.15 – Вычислительные машины, комплексы и компьютерные сети Диссертация на соискание ученой степени кандидата технических наук

Научный руководитель кандидат технических наук, доцент Мельцов Василий Юрьевич Киров 2014

СОДЕРЖАНИЕ

ВВЕДЕНИЕ

1. ЛОГИЧЕСКИЙ ВЫВОД И ВЕРИФИКАЦИЯ ПАРАЛЛЕЛЬНЫХ

АЛГОРИТМОВ

1.1. Подходы к верификации

1.2. Формальная верификация алгоритмов и программ

1.2.1. Техника дедуктивного анализа

1.2.2. Техника проверки эквивалентности

1.2.3. Техника проверки моделей

1.3. Классическая схема верификации с применением техники проверки моделей

1.4. Обзор инструментальных систем формальной верификации

1.5. Применение логического вывода для сопоставления реализации и спецификации



1.6. Классификация методов логического вывода

1.7. Сравнительный анализ методов логического вывода

1.8. Выводы

2. ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ ПАРАЛЛЕЛЬНЫХ АЛГОРИТМОВ С

ПРИМЕНЕНИЕМ ТЕХНИКИ ПРОВЕРКИ МОДЕЛЕЙ И МЕТОДОВ

ЛОГИЧЕСКОГО ВЫВОДА

2.1. Алгоритм формирования базы знаний на основе структуры Крипке и формулы темпоральной логики

2.2. Постановка логической задачи формальной верификации

2.3. Метод логического вывода для проверки эквивалентности моделей алгоритма и спецификации

2.3.1. Унификация литералов

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

2.3.3. Процедура деления дизъюнктов

2.3.4. Метод логического вывода делением дизъюнктов на основе определяющего элемента

2.3.5. Схема процесса логического вывода

2.3.6. Оценка эффективности метода

2.3.7. Анализ особенностей структуры правил в базе знаний

2.4. Формирования модели алгоритма

2.5. Построение дерева грамматического разбора LTL-спецификации.................. 62 2.5.1. Алгоритм построения дерева грамматического разбора формулы темпоральной логики линейного времени

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

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

2.6. Выводы

3. КОМПЛЕКС И МАШИНА ЛОГИЧЕСКОГО ВЫВОДА ДЛЯ

ВЕРИФИКАЦИИ ПАРАЛЛЕЛЬНЫХ АЛГОРИТМОВ

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

3.2. Модель логического вывода

3.2.1. Анализ степени параллелизма используемого метода логического вывода

3.2.2. Древовидное представление модели логического вывода

3.2.3. Анализ особенностей модели логического вывода

3.2.4. Состояния процессов

3.2.5. Типы сообщений

3.2.6. Выбор модели вычислений

3.2.7. Характеристика модели логического вывода

3.3. Машина логического вывода

3.3.1. Структура машины

3.3.2. Формат фрейма процесса

3.3.3. Форматы служебных пакетов и сообщений

3.3.4. Форматы данных

3.3.5. Принципы организации работы процессора команд

3.3.6. Подпрограммы обработки процессов

3.3.7. Унификация литералов

3.3.8. Начальная инициализация и цикл работы машины

3.3.9. Формирование контрпримера

3.3.10. Особенности практической реализации машины

3.4. Выводы

4. ИССЛЕДОВАНИЕ АППАРАТНО-ПРОГРАММНЫХ РЕАЛИЗАЦИЙ

МАШИНЫ ЛОГИЧЕСКОГО ВЫВОДА

4.1. Аналитические оценки основных характеристик машины

4.2. Программная реализация машины логического вывода

4.3. Реализация группы исполнительных процессоров на GPU

4.4. Реализация блока унификации на ПЛИС

4.5. Оценка производительности реализаций машины логического вывода на тестовых примерах ИС SPIN

4.6. Рекомендации по выбору архитектурно-структурных решений машины логического вывода

4.7. Выводы

ЗАКЛЮЧЕНИЕ

Список использованной литературы

Приложение А. Базовые термины и определения, связанные со структурой Крипке

Приложение Б. Дополнительные сведения о темпоральной логике линейного времени

Приложение В. Спецификация требований к параллельным алгоритмам с помощью выражений LTL

Приложение Г. Пример формирования базы знаний

Приложение Д. Примеры выполнения операций и процедур МВОЭ

Приложение Е. Примеры верификации с построением схемы процесса логического вывода

Приложение Ж. Блок-схемы алгоритмов выполнения процедур метода логического вывода делением дизъюнктов на основе определяющего элемента





Приложение З. Пример построения дерев грамматического разбора формулы LTL

Приложение И. Пример оптимизации дерева грамматического разбора формулы LTL

Приложение К. Процедуры обработки акторов

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

ВВЕДЕНИЕ

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

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

Одним из актуальных направлений, в котором применение методов и машин логического вывода позволит получить более эффективные решения, является активно развивающаяся в последние годы (Ч. Хоар, Э. Кларк, О. Грумберг, Д. Пелед, Г. Холзманн, Дж. Куэйл, Ю.Г. Карпов, А.А. Шалыто и др.) формальная проверка корректности программ и алгоритмов (верификация). Отличительной чертой методов формальной верификации является возможность достоверного определения отсутствия или наличия ошибки в объекте исследования. Именно эта особенность позволила формальным методам занять важное место в анализе параллельных и распределенных программ, ход выполнения которых в значительной степени зависит от состояния вычислительной среды, а моделирование этой среды на этапе верификации не представляется возможным.

Наиболее перспективным разделом формального подхода принято считать технику проверки моделей, авторы которой (Э. Кларк, Э. Эмерсон и Дж. Сифакис) в 2007 году были удостоены премии Тьюринга. Однако, в работах Г. Холзманна, М. Варди и Ф. Шноебелена показано, что большинство подобных методов обладают экспоненциальной временной сложностью, а универсальный, основанный на автомате Бюхи, способ сопоставления модели объекта верификации и спецификации в виде формулы темпоральной логики линейного времени (LTL) не обладает достаточной производительностью.

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

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

Исследование выполнялось при содействии Совета по грантам Президента Российской Федерации для государственной поддержки молодых российских ученых и по государственной поддержке ведущих научных школ (проект СПОбъектом исследования являются специализированные методы и машины логического вывода.

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

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

Для достижения цели решаются следующие задачи.

1. Разработка алгоритма формирования базы знаний на основе модели алгоритма и TL-формулы, описывающей предъявляемые к нему требования, позволяющего свести задачу сопоставления к задаче логического вывода.

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

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

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

Области исследования. Задачи, решенные в диссертации, соответствуют областям исследования специальностей 05.13.11 – Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей (п.1 – Модели, методы и алгоритмы проектирования и анализа программ и программных систем, их эквивалентных преобразований, верификации и тестирования) и 05.13.15 –Вычислительные машины, комплексы и компьютерные сети (п.3 – Разработка научных методов и алгоритмов организации арифметической, логической, символьной и специальной обработки данных, хранения и ввода-вывода информации и п.4 – Разработка научных методов и алгоритмов организации параллельной и распределенной обработки информации, многопроцессорных, многомашинных и специальных вычислительных систем).

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

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

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

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

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

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

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

Практическая ценность исследования состоит в следующем.

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

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

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

На защиту выносятся следующие результаты.

1. Метод логического вывода делением дизъюнктов на основе определяющего элемента в логике предикатов первого порядка.

2. Архитектура машины логического вывода, реализующей метод логического вывода делением дизъюнктов на основе определяющего элемента в логике предикатов первого порядка.

3. Алгоритм формирования базы знаний на основе структуры Крипке и формулы темпоральной логики.

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

Внедрение результатов исследования. Полученные теоретические и практические результаты использованы в НИР «Разработка эффективной методики верификации параллельных алгоритмов и программ с использованием методов логического вывода» (стипендия Совета по грантам Президента Российской Федерации, проект СП-1891.2013.5), в НИОКР «Разработка программного комплекса для верификации параллельных алгоритмов» (грант Фонда содействия развитию малых форм предприятий в научно-технической сфере, проект №/17248), в НИР «Разработка интеллектуальной системы обработки знаний на базе специализированного СБИС-процессора с data-flow архитектурой» (МОН РФ, ВятГУ, №01201270376), в НИР «Разработка способа оптимизации выражений модальных логик на основе методов динамического программирования» (МОН РФ, ВятГУ, №01201452001). Полученные в диссертационной работе теоретические и практические результаты используются в рамках курсов «Технология разработки программного обеспечения» и «Интеллектуальные системы». Значимость практических результатов также подтверждается наличием актов о внедрении.

Апробация работы. Основные результаты исследования докладывались и обсуждались на Четырнадцатой национальной конференции по искусственному интеллекту с международным участием (Казань, КИИ-2014), Международной научной конференции МНСК (Новосибирск, МНСК-2011, 2012, 2013, 2014), третьей международной научной конференции «Информационные технологии и системы» (Челябинск, ИТиС-2014), Всероссийской ежегодной научнопрактической конференции «Общество, наука, инновации» (Киров, НТК-2011, 2012, НПК-2013, 2014). Проект «Программный комплекс для верификации параллельных алгоритмов» был отмечен дипломом лауреата на Всероссийском конкурсе прикладных разработок и исследований в области компьютерных технологий «Компьютерный континуум: от идеи до воплощения», проводимом компанией Intel и Суперкомпьютерным консорциумом университетов России.

Публикации. Результаты исследования представлены в 19 работах (из них 10 статей, 6 тезисов докладов). Четыре работы опубликованы в научных изданиях, рекомендованных ВАК. Получен патент на полезную модель и 4 свидетельства о государственной регистрации программ для ЭВМ.

Личный вклад. Все научные результаты, приведенные в диссертационной работе и сформулированные в положениях, выносимых на защиту, получены автором лично. Работы [2-7, 10-12, 17-19] опубликованы в соавторстве с научным руководителем, которому принадлежит формулировка концепции решаемой проблемы и постановка цели исследования. Основной объем работ по написанию программ, их отладке, тестированию и интерпретации результатов экспериментов выполнен автором. В работе [20] автору принадлежит разработанная структура блока управления процессором команд, форматы сообщений и команд.

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

Основная часть работы изложена на 164 страницах, содержит 34 рисунка и 11 таблиц.

1. ЛОГИЧЕСКИЙ ВЫВОД И ВЕРИФИКАЦИЯ ПАРАЛЛЕЛЬНЫХ

АЛГОРИТМОВ

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

1.1. Подходы к верификации

Одним из важнейших этапов жизненного цикла любого программного продукта является верификация. Задачей верификации является получение ответа на вопрос «Отвечает ли разработанный программный продукт установленным требованиям?» [22]. На данном этапе, как правило, проверяется корректность функционирования программного обеспечения, его соответствие формальным правилам и стандартам.

Современные подходы к верификации могут быть разделены на группы по трем признакам: форме представления объекта анализа, типу взаимодействия с объектом и принципу осуществления проверки (рисунок 1.1) [22].

Наряду с методами и средствами для верификации уже написанных программ существуют также средства для верификации графических (схемы) и абстрактных (псевдокод) описаний [63]. Важным преимуществом последних является отсутствие привязки к конкретному языку программирования.

Вследствие этого отпадает необходимость в анализе сложных синтаксических конструкций реальных языков. В процессе верификации на первый план выходит логическая составляющая (алгоритм), а не конкретный способ реализации, что представляется более правильным с точки зрения парадигмы инженерной деятельности. Тем не менее, необходимо принимать во внимание, что в процессе имплементации верифицированного описания под влиянием человеческого фактора в программу могут быть внесены ошибки [44]. Указанный недостаток может быть частично устранен путем автоматизации трансляции проверенного описания в программный код. Следует также заметить, что использование абстрактного описания является более гибким решением, чем применение графических способов записи. Очевидно, что далеко не во всех случаях возможно наглядно изобразить алгоритм даже средних размеров.

–  –  –

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

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

Динамический анализ предполагает выполнение объекта на реальном вычислительном устройстве, совмещенное с получением дополнительной информации о текущем состоянии этого вычислительного устройства (объем задействованной памяти, значение счетчика команд, глубина программного стека и т.д.). Такие сведения позволяют контролировать поток управления и определять причины возникновения различных ошибок [63]. Важной особенностью динамических подходов является необходимость грамотного подбора входных данных, позволяющего достичь максимально возможного покрытия описания.



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

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

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

По принципу осуществления процесса верификации могут быть выделены следующие группы.

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

Примерами таких подходов являются сквозной контроль, экспертиза защищенности, анализ свойств архитектуры [22].

Статический анализ и динамический анализ были рассмотрены выше.

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

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

Важной особенностью формальной верификации, позволившей ей стать одним из ведущих способов проверки корректности программ и алгоритмов, является (в противоположность более распространенному тестированию) возможность единовременного рассмотрения всех допустимых траекторий выполнения вычислений [20]. Глубина подобного анализа зависит только от степени детализации модели. Формальный подход хорошо зарекомендовал себя как инструмент для поиска тонких ошибок в сложных параллельных программах [44]. В подобных случаях возникновение некорректной ситуации, как правило, связано с взаимодействием потоков друг с другом. Данный факт значительно затрудняет анализ, так как проявление ошибки носит стохастический характер, а ее искусственное повторение не всегда представляется возможным.

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

Синтетический анализ использует комбинации представленных выше подходов (например, тестирование на модели) [22].

1.2. Формальная верификация алгоритмов и программ

Идея формальной проверки корректности программных и аппаратных систем зародилась в 60-ых годах XX века. За несколько последних десятилетий предпринимался ряд попыток разработки методов и методик верификации.

Несмотря на то, что в данной области были получены серьезные результаты, сегодня по-прежнему не существует единого и универсального метода проверки корректности [16].

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

1.2.1. Техника дедуктивного анализа

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

Первые методы дедуктивного анализа были предложены Флойдом и Хоаром в 60-ых годах прошлого века [44]. Способ, предложенный Флойдом, основан на проверке истинности некоторой формулы логики высказываний на всевозможных линейных путях между парами точек сечений, полученных при декомпозиции блок-схемы проверяемого алгоритма Данный способ обладает [22].

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

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

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

1.2.2. Техника проверки эквивалентности

Второй подход – техника проверки эквивалентности – применяется в основном для верификации аппаратных систем [44]. Хотя некоторые идеи, заложенные в нем, используются и для проверки корректности программного обеспечения. Задача верификации сводится к проверке согласованности спецификации (то, что требуется от системы) и реализации (то, как система работает на самом деле). При этом как спецификация, так и реализация выражаются с помощью удобных, с точки зрения представления аппаратуры, исполняемых моделей.

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

1.2.3. Техника проверки моделей

Третий подход – техника проверки моделей (model checking) – может быть охарактеризован как строгая методология, включающая три компонента:

исполняемую модель верифицируемой программы или алгоритма, требования, выраженные в виде логико-алгебраической модели, и способ установления соответствия модели объекта анализа предъявляемым требованиям [16, 20].

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

Большая часть основанных на этой технике методов требуют участия специалиста только на этапах описания модели объекта проверки и спецификации. Следствием этой особенности является чрезвычайно высокая вычислительная сложность используемых алгоритмов и большой размер моделей. Другими словами, все формальные методы балансируют между степенью зависимости от эксперта (препятствие для автоматизации; данные могут быть представлены максимально компактно) и вычислительной сложностью (можно автоматизировать; большой объем данных). Model checking позволяет исключить (в некоторых случаях – свести к минимуму) участие человека в процессе верификации. Во-вторых, практически все применяемые способы сопоставления модели и требований в случае получения отрицательного результата позволяют также построить контрпример – последовательность состояний, приводящую к нарушению спецификации. Данный факт значительно облегчает процесс отладки как модели, так и объекта верификации.

Применение методов на основе техники проверки моделей сопряжено с двумя трудностями проблемой полноты модели;

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

Важно понимать, что не существует средств, способных гарантировать корректность анализируемого объекта [16, 20, 44]. Формальная верификация позволяет установить факт соответствия только проверяемым требованиям. Если эти требования не полны, то ошибка может остаться необнаруженной. Тем не менее, формальная верификация часто бывает предпочтительнее тестирования, так как она однозначно устанавливает факт соответствия или несоответствия требованиям. Кроме того, результат верификации с помощью техники проверки моделей точен настолько, насколько точна модель. Возможна ситуация, когда отрицательный результат проверки связан не с ошибкой алгоритма, а с ошибкой построения модели. В таком случае, как правило, исследование причин сбоя обнаруживает погрешность модели. После устранения неточности потребуется перепроверка всех успешно верифицированных ранее свойств. Такой сценарий приводит всего лишь к дополнительным временным затратам. Тогда как противоположная ситуация (положительный результат верификации вследствие погрешности модели) приводит к необнаруженной ошибке. Поэтому важным этапом верификации является этап построения модели объекта исследования достаточного уровня детализации [63].

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

Так, например, модели некоторых программ могут насчитывать более чем 10100 – 10200 состояний [16]. Для работы с такими объемами данных используются различные приемы: ленивые способы построения модели, компактные представления данных и т.д.

Известно также несколько высокоэффективных методов формальной верификации, основанных на технике проверки моделей (bounded model checking, probabilistic model checking и т.д.). К сожалению, их общим недостатком является ограниченная применимость. Например, символьные методы оказываются эффективными только в тех случаях, когда удается построить компактную бинарную решающую диаграмму [61], соответствующую объекту верификации.

Тем не менее, именно проверка моделей является самой перспективной для массового применения техникой формальной верификации. Доказательством этого утверждения является тот факт, что ее авторы, Эдмунд М. Кларк, Ален Эмерсон и Иосиф Сифакис, в 2007 году были удостоены премии Тьюринга «за их роль в развитии проверки моделей – высокоэффективную технику верификации программ, широко применяемую при разработке как программного, так и аппаратного обеспечения».

1.3. Классическая схема верификации с применением техники проверки моделей Принятым в model checking способом представления модели объекта верификации является система переходов – абстрактная структура, представляющая собой совокупность множества состояний системы и переходов между этими состояниями [44]. Фактически, подобная модель является разновидностью конечного автомата, к отличительным особенностям которого следует отнести способность описания процессов, происходящих внутри вычислительной машины, без излишних сложностей.

На практике наиболее часто применяются отмеченные системы переходов – системы, переходам между состояниями которых сопоставлены некоторые отметки, накладывающие дополнительные ограничения на возможность активации или сигнализирующие о факте выполнения определенных условий. В некоторых случаях отметки сопоставляются вершинам модели. Такие структуры можно считать расширением конечного автомата, в котором отсутствуют пометки на переходах, поскольку основной целью является описание конечным образом бесконечных последовательностей состояний (т.е. вычислений) при произвольных входах [16]. Таким образом, причины переходов – конкретные внешние события, существенные для конечного автомата, – не требуют рассмотрения. Теоретически такие события могут быть учтены. Однако при верификации чаще всего важно проверить, существует ли некорректное поведение объекта при любых последовательностях внешних событий, и только когда такое поведение найдено, можно искать его причину [16, 60].

Примером подобного представления модели служит структура Крипке [20, 37], которая в силу своей простоты и в то же время наглядности получила широкое распространение в моделировании сложных вычислительных систем и, в том числе, в основанных на технике проверки моделей методах верификации [16].

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

Формально структура Крипке может быть определена как пятерка M S, S0, R, AP, L, где S – конечное непустое множество состояний (вершин);

S 0 S – непустое множество начальных состояний;

R S S – тотальное отношение на S, т.е. множество переходов (дуг), удовлетворяющих требованию: (s S )(s' S )(s, s' ) R (из любого состояния есть переход);

AP – конечное множество атомарных предикатов;

L : S 2 AP – функция пометок (каждому состоянию отображения L сопоставляет множество истинных в нем атомарных предикатов).

Базовые термины и определения, касающиеся структуры Крипке, приведены в приложении А.

Предъявляемые к верифицируемому объекту требования обычно представляются с помощью расширения классической логики высказываний – темпоральной логики, которая позволяет оперировать порядком событий во времени. В основном применяются две модификации темпоральной логики – темпоральная логика ветвящегося времени (CTL) и темпоральная логика линейного времени (LTL). Однако, в силу своей универсальности, полноты и простоты для понимания, LTL используется чаще. Немаловажным является также тот факт, что выражения LTL позволяют специфицировать свойства безопасности и живости. В работе [40] сформулирована и доказана теорема, согласно которой с помощью комбинации свойств безопасности и живости можно специфицировать любое требование к программе или алгоритму.

В LTL в дополнение к базовым логическим операторам (,,,) и константам (true, false) вводится шестерка временных операторов [70].

Next (X ) – выражение Xp истинно в текущем состоянии, если в следующий момент времени p истинно.

Future (F ) – выражение Fp истинно в текущем состоянии, если в будущем p станет истинно.

Globally (G) – выражение Gp истинно в текущем состоянии, если во всех будущих состояниях p будет истинно.

Until (U ) – выражение pUq истинно в текущем состоянии, если в будущем q станет истинно, а до тех пор истинно будет p.

Week until (W ) – выражение pWq истинно в текущем состоянии, если в будущем q станет истинно, а до тех пор истинно будет p, или же p всегда будет истинно.

Release (R) – выражение pRq истинно в текущем состоянии, если в будущем p станет истинно, а до того момента времени включительно истинно будет q, или же q всегда будет истинно.

Под «когда-нибудь в будущем» и «всегда в будущем» в LTL принято понимать также текущий момент времени («сейчас»).

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

В приложении Б содержатся вспомогательные сведения об этом исчислении.

Кроме того, дополнительные сведения о специфических особенностях темпоральной логики линейного времени и ее отличиях от других модальных исчислений могут быть найдены в работах [62, 66, 79]. В приложении В представлены примеры спецификации реальных ошибок в параллельных программах и алгоритмах.

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

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

Требования к Объект объекту верификации верификации

–  –  –

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

Approximate Probabilistic Model Checker (APMC) относится к семейству основанных на технике проверки моделей вероятностных верификаторов. Для спецификации требований к объекту исследования используется вероятностная темпоральная логика линейного или ветвящегося времени. Рандомизированный алгоритм верификации, применяемый для проверки соответствия модели предъявляемым требованиям, обладает существенными особенностями. Его структура предполагает перенос выполнения наиболее трудоемких участков вычислений (генерация путей и проверка формулы) на кластерную вычислительную систему [41].

Пакет PRISM [84] представляет интерес с точки зрения используемых моделей. Основанный, как и APMC, на вероятностном model checking PRISM способен анализировать реализации, представленные в форме цепей Маркова с дискретным временем, непрерывных цепей Маркова, Марковских процессов, вероятностных автоматов, вероятностных временных автоматов, а также расширений данных структур на основе весов и вознаграждений. Описание верифицируемых алгоритмов и систем выполняется с помощью языков PRISM language, PEPA и PlainMC [72]. Требования задаются как формулы непрерывной стохастической логики или вероятностной темпоральной логики линейного времени (допускается использование логики непрерывного времени).

PRISM проверяет такие временные свойства, как «какова вероятность сбоя системы в течении следующих четырех часов?» или «какой ожидаемый размер будут иметь данные, полученные в течении следующих тридцати минут?». В основе работы ядра системы лежат принципы символьного представления данных (бинарные решающие диаграммы, мульти-терминальные решающие диаграммы) а также применения дискретно-событийного моделировании и [71], симметричной редукции. На практике наиболее широко PRISM используется для верификации коммуникационных и мультимедийных протоколов или алгоритмов криптографии [84].

Популярной средой для проверки алгоритмов является программный пакет SPIN [92]. SPIN ориентирован в первую очередь на верификацию распределенных программных систем: модель (в виде структуры Крипке), построенная по описанию на языке Promela, может быть проверена как на шаблонные ошибки (взаимоблокировка, гонки, необоснованное предположение об относительной скорости процессов и т.д.), так и на соответствие произвольному свойству, описываемому формулой темпоральной логики линейного времени [92].

Важными особенностями данного пакета являются:

применение автоматного подхода (верификация на основе автомата Бюхи);

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

возможность верификации распределенных систем с динамическим изменением числа процессов;

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

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

поддержка трех режимов работы: симулятор, точный верификатор, приближенный верификатор [92].

Интересной возможностью системы SPIN является поддержка работы в режиме драйвера для swarm-верификации, которая позволяет решать независимые подзадачи, возникающие во время проверки корректности крупных систем, параллельно на различных компьютерах [17].

В 2009 году было выпущено дополнение для трансформации среды разработки Eclipse в инструмент для описания систем на языке Promela. В 2011 году группа исследователей из штата Миннесота разработала расширение языка

– ableP. AbleP позволяет использовать многомерные массивы, Promela комбинированные типы данных, недетерминированные условные конструкции и т.д. Код ableP может быть автоматически преобразован в чистый код Promela [77].

Разработчики системы Bandera, основанной на технике проверки моделей, отмечают в качестве главного достоинства своей разработки возможность анализировать реальный программный код [39]. Более того, Bandera способна преобразовывать параллельные Java-программы в эквивалентное описание на языках Promela и TRANS.

Исследователи из Масарикова университета разработали инструментальную систему DiVinE Tool [57]. Важной особенностью реализации является хорошая масштабируемость – DiVinE Tool может работать как на многоядерном персональном компьютере, так и на серьезном промышленном кластере. В ходе верификации устанавливается соответствие модели (поддерживается несколько форматов описания, в том числе и LLVM) требованиям, выраженным в виде формулы LTL. При этом для компактного представления модели объекта верификации применяются различные оптимизации (в основном вариации редукции частичных порядков). Кроме того, DiVinE Tool отличается удобным анализатором контрпримеров.

Высокой популярностью при разработке коммуникационных протоколов и распределенных систем в промышленных масштабах пользуется программный комплекс CADP. Большая часть верифицирующих алгоритмов CADP работает с отмеченными системами переходов, но некоторые свойства проверяются и на вероятностных моделях [49]. Интересным с точки зрения реализации выглядит использованный разработчиками CADP подход к решению проблемы взрыва числа состояний модели. При решении задач малой размерности в памяти хранятся все состояния модели. При обработке задач большой размерности используется техника «генерации модели на лету» – в памяти хранится только текущее состояния и информация, необходимая для перехода в связные состояния.

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

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

Анализируемые системы в TAPAs описываются с помощью алгебры процессов [51]. В настоящий момент поддерживаются описания CCSP (модификация исчисления взаимодействующих систем, расширенная операторами из исчисления последовательных процессов) и PEPA (алгебра процессов с оценкой эффективности). Второй вариант представляет собой объединение CCS и CSP, расширенное посредством введения вероятностных ветвлений и временных переходов. При работе в режиме проверки соответствия формулы темпоральной логики модели, заданной с помощью алгебры процессов, TAPAs автоматически выполняет преобразование описания в отмеченную систему переходов.

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

Разработанный исследователями из Дании и Швеции пакет UPPAAL представляет собой многофункциональный инструмент для моделирования, валидации и верификации систем реального времени. В качестве модели исследуемой системы предлагается использовать композицию временных автоматов, расширенную добавлением типов данных [101]. UPPAAL, как и многие подобные системы, имеет гибкую модульную архитектуру, а нехарактерной особенностью пакета является наличие мощного графического интерфейса.

Набор утилит FC2Tools, как и TAPAs, оперирует моделями, описанными средствами алгебры процессов. Проблема взрыва числа состояний решается использованием бинарных диаграмм (явным, неявным или комбинированным способами). В качестве преимуществ над аналогами разработчики указывают возможность конвертирования FC2 файлов в другие форматы для взаимодействия со сторонними верификаторами [102]. Для FC2Tools существует графическая оболочка Autograph.

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

LTSmin совместим со сторонними программными комплексами: SPIN, muCRL, CADP, opaal и т.д.

Инструмент PAT [83] предназначен для исследования параллельных систем и систем реального времени. Среди его сильных сторон стоит выделить возможность верификации с применением нескольких подходов (в том числе и вероятностную проверку моделей) и удобный, с точки зрения отладки, режим анимированной симуляции. Спецификация требований к системам осуществляется с помощью формул LTL.

Краткая характеристика рассмотренных выше программных средств представлена в таблице 1.1.

–  –  –

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

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



Pages:   || 2 | 3 | 4 | 5 |   ...   | 6 |
Похожие работы:

«Молодежный инновационный форум Приволжского федерального округа Конкурс научно-технического творчества молодежи (НТТМ) Интернет-сайт: http://ify.ulstu.ru. Ульяновск, 2015 год УДК 504.06+574+663.1 Разработка экобиокомплекса «ЖИП» (Живой Источник Плодородия) для эффективного и безопасного земледелия Тольяттинский государственный университет Кутмина Светлана, студент, Андрианова Любовь, студент Заболотских Влада Валентиновна, кандидат биологических наук, доцент В данном проекте авторами разработан...»

«МИНОБРНАУКИ РОССИИ ФГБОУ ВПО УРАЛЬСКИЙ ГОСУДАРСТВЕННЫЙ ЛЕСОТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ Кафедра ботаники и защиты леса Е.А. Зотеева ЛАБОРАТОРНЫЙ ПРАКТИКУМ ПО АНАТОМИИ РАСТЕНИЙ (КОРЕНЬ, СТЕБЕЛЬ, ЛИСТ) для студентов всех форм обучения специальностей 250201, 250203, 250100, 020802 Екатеринбург Печатается по рекомендации методической комиссии ЛХФ. Протокол № 1 от 16 сентября 2010 г. Рецензент – канд. биол. наук доцент кафедры БиЗЛ М.В. Воробьева Редактор Е.Л. Михайлова Оператор компьютерной верстки Г.И....»

«УДК 539.261 В.В. Трофимов, В.В. Чижиков, Р.У. Ильясов, П.П. Панов ПРИМЕНЕНИЕ ПОРТАТИВНОГО РЕНТГЕНОВСКОГО ТЕНЗОМЕТРА ДЛЯ КОНТРОЛЯ НАПРЯЖЕННОДЕФОРМИРОВАННОГО СОСТОЯНИЯ В БУРИЛЬНЫХ ТРУБАХ Валерий Васильевич Трофимов, к.ф.-м.н., с.н.с, профессор, кафедра «Транспортные и технологические системы». Санкт-Петербург, СанктПетербургский государственный политехнический университет, Россия. Е-mail: vtrofimov@mail.ru Валерий Васильевич Чижиков, к.т.н., исполнительный директор ЗАО «Акватик». Санкт-Петербург,...»

«Выпуск 3 2014 (499) 755 50 99 http://mir-nauki.com УДК 621.391(075.8) Трещев Иван Андреевич ФГБОУ ВПО «Комсомольский-на-Амуре государственный технический университет» Россия, Комсомольск-на-Амуре Заведующий кафедрой «Информационная безопасность автоматизированных систем» Кандидат технических наук E-Mail: kalkt@yandex.ru Вильдяйкин Геннадий Федорович ФГБОУ ВПО «Комсомольский-на-Амуре государственный технический университет» Россия, Комсомольск-на-Амуре Кафедра «Информационная безопасность...»

«УДК 321.01: 316.774 NETO-КРАТИЯ ИЛИ НОВЫЙ ТОТАЛИТАРИЗМ? НЕКОТОРЫЕ НАБЛЮДЕНИЯ НАД ФЕНОМЕНОМ ВЛАСТИ В ИНФОРМАЦИОННОМ ОБЩЕСТВЕ Муза Д.Е. Донецкий национальный технический университет кафедра философии E-mail: dmuza@mail.ru Аннотация Муза Д.Е. Neto-кратия или новый тоталитаризм? Некоторые наблюдения над феноменом власти в информационном обществе. Проанализирован феномен власти в информационном обществе. Показан негативный характер нетократической власти, который проявляется в руководстве...»

«Российский научно-исследовательский институт проблем мелиорации ОСНОВНЫЕ ПРИНЦИПЫ И МЕТОДЫ ЭКСПЛУАТАЦИИ МАГИСТРАЛЬНЫХ КАНАЛОВ И СООРУЖЕНИЙ НА НИХ Под общей редакцией академика РАН, доктора технических наук, профессора В. Н. Щедрина Новочеркасск РосНИИПМ УДК 626.823.004 ББК 38.776 О 752 РЕЦЕНЗЕНТЫ: В. И. Ольгаренко – член-корреспондент РАН, Заслуженный деятель науки РФ, доктор технических наук, профессор; Ю. А. Свистунов – доктор технических наук, профессор О 752 Основные принципы и методы...»

«Министерство образования и науки Российской Федерации Казанский государственный технический университет им.А.Н.Туполева ТЕПЛООБМЕНА ИНТЕНСИФИКАЦИЯ ТЕПЛООБМЕНА Ю.Ф.ГОРТЫШОВ, И.А. ПОПОВ, В.В.ОЛИМПИЕВ, А.В.ЩЕЛЧКОВ, С.И.КАСЬКОВ ТЕПЛОГИДРАВЛИЧЕСКАЯ ЭФФЕКТИВНОСТЬ ПЕРСПЕКТИВНЫХ СПОСОБОВ ИНТЕНСИФИКАЦИИ ИНТЕНСИФИКА ТЕПЛООТДАЧИ В КАНАЛАХ ТЕПЛО ОБОРУДОВАНИЯ ТЕПЛООБМЕННОГО ОБОРУДОВАНИЯ Под общей редакцией Ю.Ф.Гортышова Казань УДК 536.24 ББК 31.3 Г74 Гортышов Ю.Ф., Попов И.А., Олимпиев В.В., Щелчков А.В.,...»

«Электрическая печь для сауны SAUNA-therm Тип 44 / 64 / 84 / 104 Руководство пользователя Уважаемый покупатель, Благодарим Вас за покупку печи для сауны LANG’s. Мы уверены, что наш высококачественный продукт будет долго и надежно служить Вам. Печи LANG’s. Качество, сделанное в Германии. Электрическое подключение Подключение печи для сауны и блока управления должно осуществляться только специалистом согласно инструкциям по монтажу производителей печи для сауны и блока управления! Технические...»

«Московский авиационный институт (национальный исследовательский университет) ЭЛЕКТРОННЫЙ ЖУРНАЛ «ПРИКЛАДНАЯ ГЕОМЕТРИЯ» http://apg.mai.ru/ Выпуск 13, N 28 (2011), стр. 23-32 МОДЕЛИРОВАНИЕ ФОРМООБРАЗОВАНИЯ ДЕТАЛЕЙ СРЕДСТВАМИ КОМПЬЮТЕРНОЙ ГРАФИКИ С ИСПОЛЬЗОВАНИЕМ ВСПОМОГАТЕЛЬНЫХ ПОВЕРХНОСТЕЙ А. А. Ляшков, Канева Ю. А. Омский государственный технический университет Кафедра “Начертательная геометрия, инженерная и компьютерная графика” 644050, Омск, пр. Мира, 11 e-mail:3dogibmod@mail.ru Аннотация....»

«Проблемы и перспективы развития орошаемого земледелия при машинном орошении Я.Э. Пулатов, А. Курбанов ГУ «ТаджикНИИГиМ» Республика Таджикистан В настоящее время для обеспечения орошения земель на площади 743,6 тыс.га действуют сложнейшие инженерные гидротехнические системы доставки и отвода воды. С начала 1960-х годов в районах орошаемого земледелия все больше распространяется тяга к машинному подъему воды, как одному из основных мероприятий повышения водообеспеченности. К началу 1970-х годов в...»

«ЖЕРЕБЦОВ Сергей Валерьевич СТРУКТУРНЫЕ ИЗМЕНЕНИЯ В ХОДЕ БОЛЬШОЙ ПЛАСТИЧЕСКОЙ ДЕФОРМАЦИИ И РАЗВИТИЕ МЕТОДОВ ПОЛУЧЕНИЯ УЛЬТРАМЕЛКОЗЕРНИСТОЙ СТРУКТУРЫ В ПОЛУФАБРИКАТАХ ИЗ СПЛАВОВ НА ОСНОВЕ ТИТАНА Специальность 05.16.01 Металловедение и термическая обработка металлов и сплавов АВТОРЕФЕРАТ диссертации на соискание ученой степени доктора технических наук Екатеринбург 2013 Работа выполнена в ФГАОУ ВПО «Белгородский государственный национальный исследовательский университет» Научный...»

«ТЕМА НОМЕРА: Корпоративный научнопроектный комплекс ОАО «НК «Роснефть» НАУЧНОТЕХНИЧЕСКИЙ СОДЕРЖАНИЕ ВЕСТНИК ОАО «НК «РОСНЕФТЬ» Издается с 2006 года ГЕОЛОГИЯ И ГЕОФИЗИКА РЕДАКЦИОННАЯ КОЛЛЕГИЯ Левин Д.Н., Резников Д.С. Спектрально-временное прогнозирование типов Богданчиков С.М. геологического разреза и фильтрационно-емкостных свойств (главный редактор) коллекторов по комплексу геофизических данных Худайнатов Э.Ю. (заместитель Гайдук В.В. Термодинамика катагенеза керогена главного редактора)...»

«Министерство образования и науки Российской Федерации Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования «Тамбовский государственный технический университет» В. В. ЛЕДЕНЁВ СТРОИТЕЛЬСТВО И МЕХАНИКА Утверждено Учёным советом университета в качестве краткого справочника для аспирантов, магистрантов и студентов Тамбов Издательство ФГБОУ ВПО «ТГТУ»  1 УДК 624.04(075.8) ББК Н581.1я73 Л39 Р е це н зе н ты: Доктор технических наук, профессор,...»

«ГЕОДЕЗИЯ ГЕОДЕЗИЯ И КАРТОГРАФИЯ ОРГАН ГЕОДЕЗИЧЕСКИХ СЛУЖБ СТРАН СНГ ВЫПУСКАЕТСЯ ПРИ ПОДДЕРЖКЕ ФЕДЕРАЛЬНОЙ СЛУЖБЫ ГОСУДАРСТВЕННОЙ РЕГИСТРАЦИИ, КАДАСТРА И КАРТОГРАФИИ МИНИСТЕРСТВА ЭКОНОМИЧЕСКОГО РАЗВИТИЯ РОССИЙСКОЙ ФЕДЕРАЦИИ Ежемесячный научно-технический и производственный журнал 7 июль 2014 ОСНОВАН В АВГУСТЕ 1925 ГОДА Содержание РЕДкОллЕГИЯ Главный редактор Геодезия Серебряков С. В. Мазуров Б. Т., Некрасова О. И. Аппроксимация гравитационного Антипов И. Т. влияния локального рельефа по его...»

«Общие требования к ВКР (из Положения об итоговой государственной аттестации выпускников, утвержденного на заседании ученого совета ЧГПУ им. И. Я. Яковлева 27.04.2012 г., протокол №9) 4.11. Требования к выпускной квалификационной работе 4.11.1. Выпускная квалификационная работа является заключительным этапом обучения студента и формой контроля его теоретической и практической подготовки к будущей профессиональной деятельности. 4.11.2. Целью выполнения ВКР являются: обобщение знаний, умений и...»





Загрузка...


 
2016 www.os.x-pdf.ru - «Бесплатная электронная библиотека - Научные публикации»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.