Системная информатика, 2016, № 7

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

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

Расширенные автоматы активно используются при построении тестов на основе формальных моделей. Однако полнота тестов, построенных по расширенному автомату на основе покрытия путей, переменных и т.п., остается практически неизвестной; более того, как известно, такие тесты не обнаруживают большое количество часто встречающихся функциональных ошибок в программных реализациях систем, поведение которых описано таким расширенным автоматом. В данной работе мы предлагаем способ для расширения множества тестовых последовательностей, построенных по расширенному автомату. Поведение расширенного автомата реализуется в языке Java с использованием достаточно простого шаблона. Далее тест, построенный по расширенному автомату одним из известных методов, проверяется па полноту относительно ошибок, сгенерированных инструментом µJava. Поскольку программа составлена по шаблону, то не обнаруженные тестом ошибки напрямую переносятся на ошибки в расширенном автомате. После этого различающая последовательность строится по некоторой автоматной абстракции расширенного автомата, поскольку существуют эффективные методы построения различающих последовательностей для конечных автоматов. Такой конечно автоматной абстракцией может быть, например, l-эквивалент, где l-эквивалент представляет собой дерево высоты l, которое частично описывает поведение расширенного автомата на входных последовательностях длины не более l. Поскольку l-эквиваленты суть конечные автоматы, то для не слишком больших l построение различающей последовательности достаточно просто. Исходный тест, расширенный такими различающими последовательностями, обнаруживает значительно больше ошибок в программных реализациях системы, для которой исходный расширенный автомат использовался как спецификация.

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

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

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