Главная » Просмотр файлов » Диссертация

Диссертация (1090534), страница 4

Файл №1090534 Диссертация (Исследование и разработка методов автоматического вывода геометрических ограничений с использованием декларативного программирования и формальных методов) 4 страницаДиссертация (1090534) страница 42018-01-18СтудИзба
Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 4)

Предметом исследованияявляются методы распределния ресурсов таким образом, что выполняютсязаданные ограничения на качество сервиса при обеспечении максимальнойприбыли поставщика IoT услуг. Для увеличения прибыли необходимо сократитьчисло нарушений заданного соглашения об уровне предоставления услуги (англ.Service Level Agreement, SLA).

В работе рассматривается постановка задачи17оптимизации в виде комбинаторного аукциона с заданными временнымиограничениями [21]. Победители каждого раунда торгов определяютсяприоритетностью поставленных задач с учетом заданных сроков на выполнениеработы. В ходе торгов минимизируется штрафная функция. Для тестированияпредложенного алгоритма были использованы реальные данные.

В ходеэкспериментов был проведен сравнительный анализ предложенного подхода итрадиционного планировщика. В качестве критериев качества использовалиськоличество завершенных задач и итоговая прибыль поставщика услуг.Одним из вариантов построения IoT является разработка системустойчивого(англ. resilent) IoT. Особенность таких систем является обеспечениеприбыли поставщика услуг с учетом неопределенности в том, в каком контекстебудут использованы элементы IoT сети. В работе [22] задача построенияавтономной устойчивой IoT сети сводится к решению двух задач — поискутаких m изменений в процессе предоставления услуг, которые удовлетворяютинтересам клиентов, которые представляются как k − 1 возможных изменений втребованиях клиентов.

В качестве решения предлагается жадный алгоритм,который последовательно применяет пять моделей для решение двухпоставленных задач. В работе показано, что данная задача принадлежит классуN P –сложных и может быть решена методами комбинаторной оптимизации. Вработе также демонстрируется, как исследуемая задача может быть представленав виде проблемы вычисления оценок кредитного дефолтного свопа (англ. creditdefault swap, CDS). Для оценки предложенного метода решения был проведенанализ базы данных слухов, распространяемых в различных СМИ.

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

Как следствие, современная промышленность ожидаетот разработчиков не “оптимального” решения, а любого, удовлетворяющегозаданным ограничениям, но как можно быстрее.18Одним из методов поиска и построения решения, удовлетворяющегозаданным требованиям, является применение декларативного программированияи формальных методов. Такой подход позволяет гарантировать, что полученноерешение удовлетворяет всем заданным ограничениям. Вместе с тем,использование подобных методов может упростить структуру самого ПО —одни и те же алгоритмы могут быть применены к разным задачам.

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

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

Одако, этой информации зачастуюнедостаточно для полного описания процесса перехода из начального состоянияв конечное. Как правило, эта проблема решается описанием дополнительныхограничений. Предложены и различные методы верификации подобногоописания UML/OCL моделей, основанных на символьных вычислениях.Каждому возможному состоянию системы ставится в соответствие переменненая,взаимоотношения между ними и возможные переходы задаются в видеограничений. В работе [23] рассматривается процедру верификации UML/OCL19моделей с использованием алгоритма SAT, учитыващей дополнительныеограничения на переходы от одного состояния к другому.Современное ПО все больше опирается на использование параллелизмаи конкуррентности.

Однако, данные технологии значительно усложняютпрограммные системы и вносят новые классы ошибок, например, возможностьвозникновения состояния “гонки”, в которм несколько потоков блокируютдоступ к одному и тому же ресурсу и ждут завершения друг друга. В работе [24]рассматривается метод на основе SAT алгоритма для анализа специальногокласса сетей Петри — сетей Гадара. Этот формализм используется длямоделирования поведения многопоточных систем. SAT используется длягенерации оптимальной стратегии управления многопоточным выполнением сучетом теории дискретных систем управления. Экспериментальные результатыдемонстрируют высокую степень масштабируемости предложенного подхода, всравнении с классическими методами. Эксперименты показывают, что подход сиспользованием алгоритма SAT позволяет генерировать системы управления длямоделей с более 100 небезопасных состоянии.Прогресс в развитии методов решения задачи SAT позволяет работатьнад реальными проблемами промышленности, которые могут содержать тысячии десятки тысяч переменных.

В работе [25] рассматриваются проблемыпланирования и назначения. Для решения этих задач приводятся методы сведенияк проблеме SAT, которые затем решаются при помощи современных алгоритмов.Эеспериментальные результаты показывают, что данный подход отличаетсявысокой степенью масштабируемости.Решение ряда практических задач требует от решателя поиска ответана последовательность сходных задач. Перезапуск алгоритма с нуля приведетк полной очистке наборов выученных утверждений и частичных наборовзначений.

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

Алгоритм обучения с конфликтами естественнымобразом поддерживает добавление утверждений. Однако, удаление утвержденийсопровождается дополнительной работой — выученные утверждения,основанные на исключенных фактах, также должны быть сброшены. Вработах [26; 27] при добавлении нового утверждения создается дополнительныйконтекст, в рамках которого продолжается решение исходной задачи. Приудалении утверждения, этот контекст сбрасывается.

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

В литературе обсуждаются методы решения как первой проблемы[30], так и второй [31], но не обеих вместе. В работе [32] рассматриваетсяподход, адресующий обе проблемы одновременно, в котором сначала взадачу добавляются предположения, после чего применяется алгоритм SatElite.Предложенный алгоритм демонстрирует более высокую производитесльность посравнению с существующими подходами. В качестве экспериментальных данныхиспользовались общедоступные тестовые примеры, полученные в ходе решенияпромышленных задач верификации полупроводниковых устройств.Современные решатели рализуют сложные эвристики и оптимизации и,как следствие, могут содержать трудновоспроизводимые ошибки.

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

Характеристики

Список файлов диссертации

Исследование и разработка методов автоматического вывода геометрических ограничений с использованием декларативного программирования и формальных методов
Документы
Свежие статьи
Популярно сейчас
А знаете ли Вы, что из года в год задания практически не меняются? Математика, преподаваемая в учебных заведениях, никак не менялась минимум 30 лет. Найдите нужный учебный материал на СтудИзбе!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
6384
Авторов
на СтудИзбе
308
Средний доход
с одного платного файла
Обучение Подробнее