Диссертация (1090534), страница 4
Текст из файла (страница 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.Предложенный алгоритм демонстрирует более высокую производитесльность посравнению с существующими подходами. В качестве экспериментальных данныхиспользовались общедоступные тестовые примеры, полученные в ходе решенияпромышленных задач верификации полупроводниковых устройств.Современные решатели рализуют сложные эвристики и оптимизации и,как следствие, могут содержать трудновоспроизводимые ошибки.
Для валидациииспользуемых алгоритмов может быть использована построенная решателеммодель — выполняющего набора значений достаточно для проверки того, чтозаданные ограничения удовлетворены. Однако, для валидации невыполненныхограничений нужны дополнительные данные, т.к. модель в таком случаене будет построена.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
