Preview

Труды Института системного программирования РАН

Расширенный поиск
Том 26, № 6 (2014)
Скачать выпуск PDF
5-16 51
Аннотация
24-25 ноября 2014 года в Париже в Институте Мин-Телеком (Institut Mines-Télécom) состоялся совместный российско-французский семинар, посвященный вопросам верификации, тестирования и оценки качества программного обеспечения (Software Verification, Testing, and Quality Estimation). Семинар был приурочен к открытию совместной исследовательской лаборатории по проблемам оценки качества в открытом веб-пространстве, которую организовали Института Мин-Телеком (Франция), Институт системного программирования РАН и Томский государственный университет. Одним из направлений исследований лаборатории будет оценка качества веб-приложений - бурного растущего сектора программных приложений. Ключевое слово этого направления Quality, послужило основой для названия совместной лаборатории - Qualipso. Настоящий выпуск содержит статьи, подготовленные по материалам, которые были представлены на этом семинаре.
17-30 83
Аннотация
В последние годы технология ОТТ (over-the-top) предоставления пользователям доступа к медиа контенту в сети интернет становится все более популярной, и, соответственно, актуальной задачей является оценка качества предоставляемого сервиса. Большинство методов оценки качества сервиса конечным пользователем основаны на сопоставлении наборов значений объективных параметров оценки качества сервиса некоторому единому значению, предсказывающему уровень удовлетворенности пользователя. В данной статье рассматривается новый подход к моделированию мультимедиа ОТТ сервисов, направленный на интегрирование в модели как функциональных, так и нефункциональных аспектов поведения сервиса. Рассматривается три класса нефункциональных параметров: объективные, субъективные и бизнес-параметры, которые, соответственно, влияют на оценку качества сервиса (QoS), качества удовлетворенности пользователя (QoE) и качества бизнеса (QoBiz). Все три класса параметров необходимо учитывать для вычисления/предсказания оценки удовлетворенности пользователя выбранным сервисом. Функциональные требования к поведению сервиса формализованы в виде модели расширенного конечного автомата с таймаутами, который дополнен контекстными переменными, представляющими нефункциональные требования к QoS, QoE и QoBiz. Для предсказания удовлетворенности пользователя, по построенному расширенному автомату сервиса с учетом возможных сценариев поведения пользователя строится l-эквивалентный древовидный автомат, поведение которого совпадает с поведением исходного расширенного автомата на всех входных последовательностях длины не больше l; значения соответствующих контекстных переменных в финальных состояниях автомата представляют собой оценку удовлетворенности пользователя. Предложенный метод иллюстрируется на примере сервиса beIN Sports Connect.
31-46 51
Аннотация
Тестирование является одним из ключевых этапов разработки сложных взаимодействующих систем. Использование формальных моделей при тестировании позволяет автоматизировать процесс генерации тестовых последовательностей по формальному описанию спецификации и дальнейшего тестирования реальной системы. Несмотря на то, что тестирование на основе формальных моделей достаточно хорошо развито, использование этого подхода при тестировании протоколов маршрутизации в беспроводных самоорганизующихся сетях (ad-hoc) требует решения ряда специальных возникающих проблем, поскольку отличительной чертой беспроводных мобильных самоорганизующихся сетей (MANET) является отсутствие предопределенной инфраструктуры и отсутствие управляющих узлов. В данной работе, для формального описания спецификации используется модель расширенного конечного автомата, описанная в терминах языка SDL. Для уменьшения числа неопределенных вердиктов, часто возникающих в традиционном тестировании на основе моделей, рассматривается самоподобие узлов сети. Практическая значимость предложенного подхода иллюстрируется эмуляцией тестирования протокола DSR (Dynamic Source Routing).
47-56 53
Аннотация
Проблема локализации неисправной компоненты в автоматной сети хорошо известна, и в данной работе мы решаем эту проблему для бинарной сети из расширенных автоматов. Для каждой из компонент строится мутационный расширенный автомат, описывающий наиболее вероятные неисправности компоненты. Для композиции мутационного автомата со спецификацией другой компоненты посредством моделирования определяется древовидный конечный автомат, поведение которого совпадает с поведением исходного расширенного автомата на всех последовательностях длины не больше l (l-эквивалент). Из l-эквивалентов удаляются вход-выходные последовательности, принадлежащие композиции-спецификации, и для полученных мутационных l-эквивалентов строится диагностический эксперимент. Если такой диагностический эксперимент существует, то по реакции композиции, предъявленной для тестирования, достаточно часто можно определить, какая из компонент является неисправной, при условии, что неисправности возможны только в одной компоненте.
57-62 52
Аннотация
В работе представлен алгоритм параллельного исследования графа. Автомат на графе является аналогом машины Тьюринга - ячейки ленты соответствуют вершинам графа, где автомат может сохранять некоторую информацию, а движение по ленте соответствует движениям по дугам графа. Такая система может рассматриваться также как совокупность автоматов, размещенных в вершинах графа и взаимодействующих путем посылки сообщений по дугам. Каждый автомат изменяет свое состояние в соответствии с данными, сохраняемыми в вершине, а движение по дугам заменяется посылкой сообщений. Время работы предлагаемого алгоритма параллельного исследования графа ограничено сверху O(n/k+D), где n - число вершин графа, D - диаметр графа, максимальная длина простого пути (пути без самопересечений). В результате работы алгоритма строится два остова графа: прямой остов, корнем которого является корневая вершина графа, ориентированный от корня, и обратный остов, ориентированный к корню.
63-66 54
Аннотация
В статье представлен алгоритм параллельного вычисления произвольной функции от мультимножества значений, находящихся в вершинах графа. Вычисления выполняются автоматами, размещенными в вершинах графа и обменивающихся сообщениями по дугам графа. В основе алгоритма лежит использование информации о структуре графа, извлеченной в результате параллельного исследования графа и представляющей собой прямой и обратный остовы графа. Для хранения этой информации требуется конечное число бит в каждой вершине графа. Вычисление значения той или иной функции основано на алгоритме пульсации: сначала от автомата начальной вершины по всему графу распространяются сообщения-вопросы, которые должны достигнуть каждой вершины, а затем от каждой вершины «в обратную сторону» к начальной вершине двигаются сообщения-ответы. Алгоритм пульсации, по сути, вычисляет агрегатные функции, для которых значение функции от объединения мультимножеств вычисляется по значениям функции от этих мультимножеств. Показано, что любая функция f(x) имеет агрегатное расширение, то есть может быть вычислена как h(f`(x)), где f` агрегатная функция.
67-76 52
Аннотация
В статье предложен подход к тестированию программных реализаций телекоммуникационных протоколов на основе древовидных автоматов. Эффективность предложенного подхода иллюстрируется на примере протокола TCP (Windows).
77-84 60
Аннотация
В данной статье предлагается алгоритм минимизации конечного полностью определенного автомата с таймаутами. Показывается, что в отличие от классических конечных автоматов, для таких автоматов минимальная форма не является единственной с точностью до изоморфизма.
85-98 62
Аннотация
Рассматривается задача синтеза неизвестной компоненты, которая при совместной работе с известной частью системы удовлетворяет заданной спецификации, в случае, когда поведение компонент и спецификация системы в явном виде зависят от времени. Результаты, известные для решения параллельного автоматного уравнения для классических конечных автоматов, обобщаются на случай автоматов с таймаутами. Задача синтеза неизвестной компоненты возникает во многих приложениях и в статье иллюстрируется ее применение для реализации композиции сервисов с заданными ограничениями на временные параметры качества.
99-110 77
Аннотация
Развитие технологий и снижение стоимости беспроводных сенсорных систем привело к открытию новых областей для их применения и повышению требований к обеспечению безопасности и надежности сетей. Ограничения ресурсов узлов беспроводных сенсорных сетей приводят к жестким рамкам для реализации безопасных протоколов их взаимодействия. Так как сенсорные узлы работают, как правило, в неконтролируемой или даже враждебной среде, они подвержены отказам и уязвимы для атак. Для обеспечения надежности и безопасности взаимодействия сенсоров в сети отказоустойчивая маршрутизация становится ключевым элементом, который должен быть реализован в беспроводных сенсорных сетях. В данной работе исследуются два отказоустойчивых протокола маршрутизации, INSENS и ITSRP, для которых проводится анализ параметров их устойчивости к атакам. Моделирование и анализ быстродействия показали, что оба протокола достаточно хороши с практической точки зрения.
111-124 52
Аннотация
В данной статье предлагается алгоритм построения адаптивной проверяющей последовательности для недетерминированного конечного полностью определенного автомата относительно редукции.
125-140 50
Аннотация
Корпоративные системы для организации и поддержания совместной работы становятся все более популярными. В условиях роста использования таких систем разработка методов, обеспечивающих надежное доверительное взаимодействие вовлеченных агентов, становится одной из приоритетных задач. Решение о том, с какими агентами (другими пользователями или приложениями) и каким образом осуществлять взаимодействие, может быть различным для различных систем. В данной работе мы акцентируем внимание на предоставлении вердикта о степени доверия на основе оценки поведения различных агентов с использованием распределенного сетевого он-лайн мониторинга. Предложенная оценка предоставляет системам управления, основанным на «мягком доверии» информацию об опыте доверителя. В данной работе мы предлагаем масштабируемый метод оценки для любого он-лайн мониторинга с использованием вспомогательной модели расширенного конечного полуавтомата и известных методов для уменьшения временной сложности алгоритма оценки.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)