Последний номер

Скачать

Ресурсы и инструменты для преподавания методов Semantic Web

За последние годы создано значительное количество структурированных данных как научными, так и коммерческими организациями. На базе этих данных разрабатываются многочисленные приложения, что делает более важным и нужным знакомство с этим направлением современных ИТ-специалистов. В данной работе обсуждаются как важные аспекты эволюции направления Semantic Web, так и опыт преподавания методов и...
Скачать

Реализация оптимизирующих трансформаций в системе предикатного программирования

Описываются оптимизирующие трансформации склеивания переменных, замены хвостовой рекурсии циклом, открытой подстановки, упрощения и оформления. Результатом трансформаций является эффективная императивная программа. Используется потоковый анализ, включающий построение графа вызовов и определение области жизни переменных программы.
Скачать
В статье представлены объектная модель и язык предметно-ориентированных систем переходов — нового формализма, предназначенного для спецификации и апробации формальных методов обеспечения надежности программного обеспечения.
Скачать
Многие варианты коммуникационного протокола скользящего окна, который предназначен обеспечивать надежную передачу данных по ненадежным каналам, были специфицированы и верифицированы с использованием различных техник проверки, таких как доказательство теорем, проверка моделей и их комбинаций. В данной работе предлагается рассмотреть спецификацию протокола скользящего окна как мультиагентной модели. Темпоральные и эпистемические свойства протокола сформулированы с помощью логики знаний и времени.
Скачать
В статье описан подход к созданию вычислительных платформ на примере UGENE Workflow Designer. Эта платформа, основанная на внутреннем языке программирования UWL, демонстрирует, как, следуя принципам внутренней модели платформы и синтаксиса языка программирования, сохранять систему целостной и удобной для развития и поддержки. Система UGENE Workflow Designer предназначена для решения задач биоинформатики, а язык UWL является DSL языком этой области. В статье описаны и обоснованы возможности использования этой вычислительной платформы в качестве основы переиспользования ее средств в некоторых других прикладных областях.
Скачать
За полувековую историю развития программирования и информационных технологий возникло несколько тысяч компьютерных языков. Виртуальный мир компьютерных языков включает языки программирования, спецификаций, моделирования и другие языки. В каждой из этих ветвей можно выделить разные подходы (например, императивный, декларативный, объектно-ориентированный), дисциплины обработки (например, последовательная, недетерминированная, распределённая) и формализованных моделей (от машин Тьюринга до машин логического вывода). Поэтому актуальной становится проблема классификации компьютерных языков. Для решения этой проблемы предлагается подход, основанный на парадигмах компьютерных языков и выделении общих атрибутов, присущих разным языкам. При этом особую роль призван сыграть разрабатываемый портал знаний о компьютерных языках. Этот портал предназначен для поиска сведений о компьютерных языках в открытых структурированных источниках в сети Интернет, организации хранения и доступа к собранной информации по логическим запросам с целью выявить законы мира компьютерных языков и помощи в выборе компьютерных языков для формирования новых программных проектов. Существующая в настоящее время версия портала далека от совершенства как с точки зрения представленной информации (количественно и качественно), так и с точки зрения выбора логического языка запросов. Поэтому в настоящей статье представлено общее описание проблемы классификации компьютерных языков, описание принципиального подхода к этой проблеме, текущее состояние портала, а также обсуждаются перспективы развития логического языка запросов.
Скачать
Отличительной чертой проекта C-light является максимальное использование формальных непротиворечивых методов. Это касается не только фундаментальных базисов для верификации, таких как операционная семантика Плоткина или логика Хоара, но и реализационных аспектов. Одним из таких моментов является локализация потенциальных ошибок. В большинстве известных систем верификации локализация ошибок просто реализуется программистами как часть функционала системы без подведения какой-либо формальной основы под этот процесс. В свете недавнего расширения проекта C-light техникой семантической разметки и выбора инструментария LLVM/Clang для входного блока системы мы приводим обзор наших наработок для решения этой задачи.
Скачать
В статье рассмотрен стрип-метод линейного предыскажения сигналов и изображений с использованием нескольких видов матриц преобразования. Определены матрицы, которые достаточно хорошо минимизируют амплитуду помехи. Исследована зависимость качества восстановления данных от местоположения и размера помехи. Выявлена возможность использования стрип-метода в сочетании с компрессией, основанной на разреживании изображения, и разработан алгоритм, реализующий это сочетание.
Скачать
Данная статья посвящена проблемам интеллектуального доступа к информационным ресурсам. Приводится анализ информационных систем, поддерживающих работу с данными, либо представленными текстовыми документами и их фрагментами, либо заданными объектной моделью на основе онтологии предметной области. Авторами предложен подход к созданию системы, которая бы поддерживала оба вышеперечисленных способа представления информации, описана ее архитектура и схема хранилища данных.
Скачать
Задача декомпиляции Java-байткода состоит в построении исходного кода на языке Java, эквивалентного данному байткоду. Байткод — линейная программа с условными и безусловными переходами, а язык Java содержит структуры управления, который образуют иерархию в исходном коде. Эту иерархию необходимо восстанавливать при декомпиляции, в частности, необходимо восстановить блоки обработки исключений try-catch-finally. В проекте Excelsior RVM (виртуальной машины Java со статическим компилятором) байткод декомпилируется для проведения оптимизирующих преобразований. При построении блоков обработки исключений декомпилятор системы Excelsior RVM полагает, что байткод был получен путем компиляции исходного кода стандартным компилятором языка Java, и пытается совершить обратное преобразование. Иногда это не удается для байткода, полученного другими инструментами. В данной работе предложен алгоритм декомпиляции, восстанавливающий блоки обработки исключений из произвольного корректного байткода. Этот алгоритм реализован, интегрирован в систему Excelsior RVM и протестирован на реальных приложениях.
Скачать
В статье рассматриваются несколько популярных классических моделей анализа и прогнозирования временных рядов. Вначале описываются относительно простые модели усреднения и сглаживания, затем модели авторегрессии, скользящего среднего, а также «смешанная» модель авторегрессии-скользящего среднего, полученная путем скрещивания двух последних моделей. Последней рассматривается интегрированная модель авторегрессии-скользящего среднего для случая нестационарных временных рядов.
Скачать
В процессе считывания РНК на определенных участках ДНК — сайтах связывания формируется комплекс белков, называемых транскрипционными факторами. Этот комплекс позволяет закрепиться РНК-полимеразе и начать считывание РНК. Задача поиска сайтов связывания на ДНК является сложной ввиду наличия многих факторов, влияющих на связывание. В их числе — наличие других сайтов связывания на небольшом расстоянии от рассматриваемого сайта. Для исследования этой зависимости авторами были введены в рассмотрение гистограммы распределения плотности сайтов на геноме, названные геномными профилями. В рамках данной работы реализован алгоритм предсказания сайтов связывания с помощью весовых матриц, написана его параллельная реализация для архитектуры NVidia CUDA, реализован алгоритм построения геномных профилей, алгоритмы иерархической кластеризации и кластеризации К-средних для геномных профилей. Реализован алгоритм, позволяющий строить случайные иерархии транскрипционных факторов на основании существующей биологической классификации для того, чтобы оценить качество полученной классификации геномных профилей. Соответствующая программа написана на языке С++ и предназначена для быстрого построения геномных профилей и их первичного анализа. Проведен анализ сходства классификации геномных профилей с биологической классификацией транскрипционных факторов для исследования влияния взаимного расположения сайтов связывания на ДНК.
Скачать
Цель данной работы – установить взаимосвязи между различными параллельными моделями реального времени. Для достижения данной цели мы определили категорию временных причинных деревьев и исследовали, какое место занимает эта категория среди других категорий временных моделей. В частности, мы установили существование сопряженных функторов между категорией временных причинных деревьев и категорией временных структур событий, используя для этого более выразительную модель временных деревьев событий. Тем самым мы показали, что временные причинные деревья проще временных структур событий в том, что они отражают только один аспект семантики истинного параллелизма, а именно причинную зависимость, и не используют понятие события для задания отношения причинной зависимости. С другой стороны, модель временных причинных деревьев более выразительна, чем модель временных структур событий по следующей причине: для нее множество всех возможных последовательностей выполнения может быть определено в терминах дерева без каких-либо ограничений, а множество всевозможных последовательностей выполнения для временной структуры событий должно быть замкнутыми относительно операции перестановки параллельных переходов.
Скачать
Статья описывает применение системы проверки моделей SPIN к решению японской головоломки о переправе через реку (продвинутый вариант задачи о волке, козе и капусте) и головоломки "Irregular IQ Cube" (также называемой "Куб-1").
Скачать
В данной статье рассматривается вопрос сохранения архивов газет в цифровой форме. Предлагается технология, охватывающая цикл сканирование-подготовка-публикация, причем в качестве ключевых задач представлены: отображение на сайте материала выпусков газет и поиск статей по заданию текстового поискового образа (ключевых слов).
Скачать
В работе рассматриваются проблемы сбора информации для тематических интеллектуальных научных интернет-ресурсов, обеспечивающих систематизацию и интеграцию научных знаний, информационных ресурсов, относящихся к определенной области знаний, и средств их интеллектуальной обработки, а также содержательный доступ к ним. Предлагается подход к автоматизации сбора информации, объединяющий методы метапоиска и извлечения информации, базирующиеся на онтологиях и тезаурусах моделируемой области знаний.
Скачать
Определяются языковые средства и методы реализации строковых объектов. Строки реализуются как массивы литер в стиле языков C и C++. Для строковых объектов доступен весь аппарат работы со списками. В связи с этим в данной работе пересматривается язык списков. В работе представлена часть библиотеки для строковых объектов.
Скачать
Технология автоматного программирования ориентирована на разработку простых, надежных и эффективных программ для класса реактивных систем. Автоматная программа реализует конечный автомат в виде гиперграфа управляющих состояний. В качестве языка спецификаций автоматных программ предлагается язык продукций, применяемый для описания сценариев использования (use case) – одного из видов функциональных требований. Технология представлена в виде свода золотых правил программирования, определяющих правильный баланс в интеграции автоматного, предикатного и объектно-ориентированного программирования. Технология иллюстрируется на наборе примеров.
Скачать
В работе проводится сравнение системы «Discovery» с алгоритмами Microsoft Association Rules, Decision Trees и Neural Network, встроенными в Microsoft SQL Server Analysis Services. Показывается, что система «Discovery», во-первых, обладает теоретическими преимуществами перед этими алгоритмами, во-вторых, практически работает лучше на данных, где эти преимущества проявляются явно и, в-третьих, хорошо себя показывает на данных, взятых из репозитория UCI. Эти результаты демонстрируют определенные преимущества системы Discovery перед методами, встроенными в Microsoft SQL Server Analysis Services.
Скачать
В статье рассматривается задача параллельной разметки графа объектов в рамках системы автоматического управления памятью. Авторы формулируют набор ограничений для решения данной задачи и строят алгоритм параллельной разметки, учитывающий эти ограничения. Предложенный алгоритм был реализован в Java-машине Excelsior RVM и апробирован на реальных Java-приложениях. Полученные результаты показывают значительное ускорение разметки графа объектов в большинстве случаев.
Скачать
Представлен новый формализм для описания онтологий систем и их изменений - концептуальные системы переходов. Даны базовые определения теории концептуальных систем переходов. Показано, что эти системы позволяют специфицировать как типовые, так и новые виды онтологических элементов, составляющих онтологии. Описана классификация онтологических элементов на основе таких систем.
Скачать
Определяется типовая архитектура системы управления вида human-in-the-loop. Набор функциональных требований к системе управления беспилотным 4-х винтовым вертолетом - квадрокоптером – определяется как конкретизация типовой архитектуры. Рассматривается две задачи: управление полетом квадрокоптера по заданной траектории и слежение за движущимся объектом.
Скачать
Предложен язык CTSL спецификации концептуальных систем переходов, которые являются формализмом для описания динамических дискретных систем на основе их концептуальной структуры. Рассмотрены базовые виды концептуальных систем переходов. Определены предопределенные элементы и операции языка CTSL.
Скачать
В статье представлены материалы о Летней школе юных программистов 2014 года. С 1976 года по инициативе Андрея Петровича Ершова была организована Летняя школа юных программистов. С момента организации ЛШЮП менялись формы и методические особенности проведения занятий. Численность участников варьировалась, менялась техника. Изначально были потоковые занятия с начинающими и уже «продвинутыми» школьниками, консультанты из Академгородка. Следующим этапом стали мастерские… От нескольких минут практики на БЭСМ-6 до многочасового программирования на персональных компьютерах прошло 40 лет. Однако самое главное – атмосфера сотрудничества, направленная на формирование устойчивого стремления к самообразованию, помощь в профессиональной ориентации, основанная на практической деятельности, дающей представление о выбранной профессии, осознанный выбор жизненного пути, развитие творческих способностей, социализация – бережно хранятся. Коллектив участников Летней школы юных программистов – это не только соратники по профессии, но и сообщество единомышленников.
Скачать
Существует определённый разрыв в уровне математической подготовки программистов-теоретиков и программистов-практиков: первые сильны в науке абстрактной алгебры и математической логики, а вторые – в искусстве разработки программных систем. В статье представлен достаточно простой подход к алгебраическим и логическим основаниям формальной семантики программ, ориентированный на инженеров-программистов с элементарными знаниями по абстрактной алгебре и математической логике. Для этого в статье объясняются основы операционной, денотационной, аксиоматической семантики, а также семантики второго порядка на примере «эзотерического» языка, синтаксически похожего на язык программирования.
Скачать
В статье представлено описание математической модели представления документов. Модель включает в себя описания различных типов сегментов, которые определяются в тексте с помощью маркеров. Для данной модели приведен алгоритм сегментирования текста документа.
Скачать
Обсуждаются возможности изучения процессов на основе представления их с помощью спиралей развития. Вводятся геометрические понятия, связанные со спиралью, позволяющие моделировать развитие проекциями траекторий на различные плоскости пространства факторов.
Скачать
Метод недоопределённых вычислений является одним из подходов для решения задачи удовлетворения ограничений. Его базовым понятием является понятие вида недоопределённости, которое представляет собой способ задания неточного значения в виде множества. В статье рассматриваются различные виды недоопределённости, приводятся их формальные определения, выполняется сравнение и выделяются их основные свойства.
Скачать
В статье описывается подход к анализу совместимости многозадачных приложений реального времени с различными комбинациями дисциплин планирования и протоколов доступа к разделяемым ресурсами при их исполнении на многоядерных платформах. Этот подход основан на введенном недавно понятии плотности приложения, которое выводится из установления выполнимости приложения для различных значений производительности процессора. Описывается программная архитектура относительно простого инструмента имитационного моделирования для определения времени отклика задач (и, тем самым, выполнимости приложения), что обеспечивает более точные данные, по сравнению с известными аналитическими методами там, где они применимы. Представлены результаты работы этого инструмента на ряде эталонных примеров, включая сбалансированные конфигурации Лю-Лейланда, их интерпретации и анализа. Предложенный подход позволяет определить оптимальную для данной конфигурации приложения комбинацию дисциплины планирования и протокола доступа.
Скачать
В статье представлен метод для анализа и верификации Use Case Maps (UCM) моделей с конструкциями управления сценариями, включающими защищенные компоненты и конструкции, служащие для обработки исключительных ситуаций. Анализ и верификация UCM моделей проводится с помощью раскрашенных сетей Петри (РСП) и верификатора SPIN. Описан алгоритм для трансляции конструкций управления сценариями из UCM в РСП. Алгоритм и процедура верификации продемонстрированы на примере сетевого протокола.
Скачать
Расширенные автоматы активно используются при построении тестов на основе формальных моделей. Однако полнота тестов, построенных по расширенному автомату на основе покрытия путей, переменных и т.п., остается практически неизвестной; более того, как известно, такие тесты не обнаруживают большое количество часто встречающихся функциональных ошибок в программных реализациях систем, поведение которых описано таким расширенным автоматом. В данной работе мы предлагаем способ для расширения множества тестовых последовательностей, построенных по расширенному автомату. Поведение расширенного автомата реализуется в языке Java с использованием достаточно простого шаблона. Далее тест, построенный по расширенному автомату одним из известных методов, проверяется па полноту относительно ошибок, сгенерированных инструментом µJava. Поскольку программа составлена по шаблону, то не обнаруженные тестом ошибки напрямую переносятся на ошибки в расширенном автомате. После этого различающая последовательность строится по некоторой автоматной абстракции расширенного автомата, поскольку существуют эффективные методы построения различающих последовательностей для конечных автоматов. Такой конечно автоматной абстракцией может быть, например, l-эквивалент, где l-эквивалент представляет собой дерево высоты l, которое частично описывает поведение расширенного автомата на входных последовательностях длины не более l. Поскольку l-эквиваленты суть конечные автоматы, то для не слишком больших l построение различающей последовательности достаточно просто. Исходный тест, расширенный такими различающими последовательностями, обнаруживает значительно больше ошибок в программных реализациях системы, для которой исходный расширенный автомат использовался как спецификация.
Скачать
Конечные автоматы-преобразователи (трансдьюсеры) над полугруппами могут служить формальными моделями последовательных реагирующих программ. В отдельных случаях задачу верификацию таких программ можно свести к задачам минимизации и проверки эквивалентности. Для эффективного решения этих задач приходится налагать некоторые ограничения на полугруппы, над которыми работают трансдьюсеры. Минимизация трансдьюсеров проводится в три этапа: вначале для всех состояний трансдьюсера вычисляются наибольшие общие делители, затем трансдьюсер преобразуется к приведенной форме путем «вынесения» таких делителей, и в заключении к приведенному трансдьюсеру применяются методы минимизации конечных автоматов. Предложенный метод минимизации позволяет также проверять эквивалентность трансдьюсеров.
Скачать
В данной работе представлены подходы для решения задачи улучшения классификации текстов по тональности в динамически обновляемых текстовых коллекциях. Предлагается три метода решении обозначенной задачи, принципиально различающихся между собой. В данном случае для классификации текстов по тональности используются методы машинного обучения с учителем и методы машинного обучения без учителя. Приведены сравнения методов и показано в каких случаях какой метод наиболее применим. Описываются экспериментальные сравнения методов на достаточно представительных текстовых коллекциях.
Скачать
Замкнутая информационная система - это информационная система такая, что ее окружение не изменяет ее, и имеется передача информация из нее в ее окружение и из ее окружения в нее. В этой работе предложены два формализма (системы информационных запросов и системы концептуальных конфигураций) для абстрактного унифицированного моделирования артефактов (концептуальных набросков и моделей) концептуального дизайна замкнутых информационных систем, ранней стадии процесса проектирования информационных систем. Системы информационных запросов определяют абстрактную унифицированную информационную модель для артефактов, основанную на таких общих понятиях как состояние, информационный запрос и ответ. Системы концептуальных конфигураций являются формализмом для концептуального моделирования систем информационных запросов. Они определяют абстрактную унифицированную концептуальную модель для артефактов. Даны базовые определения теории систем концептуальных конфигураций. Показано, что эти системы позволяют моделировать как типовые, так и новые виды онтологических элементов. Описана классификация онтологических элементов, основанная на таких системах. Определен язык систем концептуальных конфигураций.
Скачать
В статье описан метод верификации семейств распределенных систем, порожденных контекстно-зависимой грамматикой специального вида. Этот метод основан на технике проверки моделей и абстракции. Репрезентативная модель зависит от грамматики, определяющей семейство систем. Эта модель симулирует поведение всех систем семейства таким образом, что свойства, выполнимые в репрезентативной модели, выполняются так же и в этих системах. Показано использование предложенного метода для верификации некоторых свойств мультиагентой системы разрешения контекстно-зависимых неоднозначностей в рамках пополнения онтологий.
Скачать
На сегодняшний день текущая практика промышленной автоматизации такова, что тестирование управляющих алгоритмов в подавляющем большинстве случаев начинается только при запуске ПО на реальном объекте. В результате проверка алгоритма откладывается до этапа пуско-наладочных работ на объекте автоматизации. В статье предложен подход к тестированию алгоритмов управления на основе концепции виртуальных объектов управления. Для гарантии, что алгоритм управления удовлетворяет полностью накладываемым на него требованиями, используется метод верификации Model checking.
Скачать
При разработке требований к поведению распределенных программных систем инженер должен мысленно упорядочивать и определять последовательности событий. Из-за чередования процессов количество возможных последовательностей растет экспоненциально, поэтому разработка таких требований становится нетривиальным занятием. Как следствие, инженеры ограничиваются составлением очень простых требований, которых зачастую бывает недостаточно, чтобы выразить желаемые свойства системы. В работе рассматривается расширение в линейной темпоральной логике известного и часто используемого на практике темпорального отношения leads-to (по событию--запросу когда-нибудь в будущем будет событие--отклик) на последовательность событий при помощи методики составления контекстных требований. Основным результатом данной работы является построение формальных требований к системе управления энергоснабжением судна на основе данной методики. Формальная верификация этих требований методом проверки модели позволила выявить несколько ошибок в поведении системы, допущенных при ее проектировании, 3 из которых оказались критическими.
Скачать
В статье представлена процедура построения параллельной композиции временных автоматов с использованием BALM-II и предложены различные подходы к получению линейных функций, задающих задержки выходов. Наше исследование включает три этапа: на первом этапе мы рассматриваем композицию временных автоматов, временные задержки выходов в которых это натуральное число или ноль; на втором этапе добавляются переходы по таймаутам; на третьем этапе рассматривается композиция временных автоматов в общем случае (когда задержки выходов задаются при помощи множества линейных функций). Данная работа посвящена только первому этапу нашего исследования.
Скачать
Статья посвящена вопросам спецификации структуры и поведения программных библиотек. Описываются существующие проблемы спецификации библиотек. Дается краткий обзор состояния дел в области формализации спецификации библиотек и библиотечных функций. Формулируются требования к создаваемому формализму. На основе требований предлагается формализм, позволяющий специфицировать все необходимые свойства библиотек, требуемые для автоматизации нескольких классов задач: обнаружение дефектов в программном обеспечении, миграция приложений в новое окружение, генерация программной документации. В заключении определяются дальнейшие направления исследований.
Скачать
Класс информационных систем, рассматриваемый в этой работе, определяется следующим образом: система принадлежит этому классу, если ее изменение может быть вызвано как ее окружением, так и факторами внутри системы, и имеется передача информация из нее в ее окружение и из ее окружения в нее. В этой работе предложены два формализма (информационные системы переходов и концептуальные системы переходов) для абстрактного унифицированного моделирования артефактов (концептуальных набросков и моделей) концептуального дизайна информационных систем этого класса, ранней стадии процесса проектирования информационных систем. Информационные системы переходов определяют абстрактную унифицированную информационную модель для артефактов, основанную на таких общих понятиях как состояние, информационный запрос и ответ. Концептуальные системы переходов являются формализмом для концептуального моделирования информационных систем переходов. Они определяют абстрактную унифицированную концептуальную модель для артефактов. Даны базовые определения теории концептуальных систем переходов. Определен язык концептуальных систем переходов.
Скачать
Семантика языка предикатного программирования P формализована с использованием трех видов отношений: совместимости, согласованности и тождества. Рекурсивные типы определены через аппарат наименьшей неподвижной точки. Обобщенные типы представлены типовыми ограничениями (концептами). Для конструкций с неявной типизацией сформулированы правила восстановления типов переменных. Разработаны алгоритмы проверки корректности рекурсии, определения типов для языковых конструкций, проверки семантической корректности конструкций.
Скачать
Операции с АВЛ-деревьями компактно и элегантно представляются в языках функционального программирования. Однако функциональные программы для операций вставки или удаления вершины заведомо неэффективны, поскольку определяют построение нового дерева, а не модификацию исходного. Описывается построение двух версий предикатных программ вставки в АВЛ-дерево, допускающих автоматическую трансформацию в эффективные императивные программы. В языке предикатного программирования введена эффективно реализуемая операция доступа вершины по пути в дереве.
Скачать
Выполнен обзор работ, формирующих теоретические основы вычислений на сетях Слепцова и представляющих особенности рисования, компиляции и компоновки программ на языке сетей Слепцова, а также массово параллельные архитектуры вычисляющей памяти для реализации процессоров сетей Слецова. Сеть Петри выполняется экспоненциально медленнее и является частным случаем сети Слепцова. Рассмотрена универсальная сеть Слепцова, содержащая 13 позиций и 26 переходов, представляющая собой прототип процессора сетей Слепцова. Приведены примеры программ на языке сетей Слепцова для эффективного умножения, RSA шифрования/дешифрования, вычисления функции нечёткой логики и решения уравнения Лапласа. Преимуществами вычислений на сетях Слепцова являются наглядный графический язык, сохранение естественного параллелизма предметной области, мелкая грануляция параллельных вычислений, формальные методы верификации параллельных программ, быстрые массово-параллельные архитектуры, реализующие модель вычислений.
Скачать
Описываются оптимизирующие трансформации для операций над списками и деревьями в системе предикатного программирования. Кодирование операций представлено набором правил, определяющих замену исходной операции на ее образ в императивном языке. Результатом трансформаций является императивная программа по эффективности сравнимая с написанной вручную.
Скачать
В статье описан подход к организации процесса извлечения информации из протоколов клинических испытаний под управлением онтологии. Рассмотрены отдельные компоненты модели знаний, включая семантический словарь, жанровую модель текста, онтологию клинических испытаний, и приведены примеры ситуаций.
Скачать
В статье описывается структура онтологии шаблонов требований, извлекаемых из текстов технической документации. Эта онтология комбинирует шаблоны известных классификаций требований с новыми шаблонами. Язык онтологии допускает запись булевых комбинаций шаблонов следующих типов: качественных, реального и ветвящегося времени, с комбинированными событиями, количественными характеристиками событий и простыми утверждениями о данных. Приведены примеры шаблонов требований к реальной системе управления вакуумированием Большого солнечного вакуумного телескопа. Изложена схема интеллектуальной системы поддержки формальной верификации распределенных программных систем.
Скачать
В статье предлагается понятие концептуальной модели языка программирования. Этот формализм представляет типы языка программирования, значения, исключения, состояния и выполнимые конструкции абстрактной машины языка программирования, и ограничения для этих сущностей на концептуальном уровне. Представляется новое определение концептуальных систем переходов, ориентированное на спецификацию концептуальных моделей языков программмирования, описывается язык переопределенных концептуальных систем переходов CTSL, и предлагается техника использования CTSL в качестве предметно-ориентированного языка спецификации концептуальных моделей языков программирования. Концептуальные модели для семейства простых языков программирования иллюстрируют эту технику.
Скачать
В статье предлагается понятие концептуальной операционной семантики языка программирования. Этот формализм представляет операционную семантику языка программирования в терминах его концептуальной модели, основанной на концептуальных системах переходов. Определяется специальный вид концептуальных систем переходов - операционные концептуальные системы переходов, ориентированный на спецификацию концептуальной операционной семантики языков программирования, описывается расширение языка концептуальных систем переходов CTSL для операционных концептуальных систем переходов, и предлагается техника использования расширенного CTSL в качестве предметно-ориентированного языка спецификации концептуальной операционной семантики программных языков. Концептуальная операционная семантика для семейства модельных языков программирования иллюстрирует эту технику.
Скачать
В работе рассматриваются эксперименты с конечными полуавтоматами, направленные на идентификацию финального (текущего) состояния проверяемой системы после подачи соответствующей входной последовательности. В исследуемой модели действия разделены на входные и выходные, однако в модели отсутствуют специально выделенные семейства начальных и финальных состояний. В статье определяются подходящий синхронизирующий и установочный эксперименты, и предлагаются методы их синтеза для специального класса входо-выходных полуавтоматов, у которых в каждом состоянии определены переходы или только по входным, или только по выходным действиям, а также в графе переходов отсутствуют циклы по выходным символам. Для описанного класса входо-выходных полуавтоматов устанавливаются необходимые и достаточные условия существования безусловных синхронизирующего и установочного экспериментов.
Скачать
В статье рассказывается о недавних достижениях на пути к строгой верификации промышленных операционных систем (ОС). Под промышленной ОС имеется в виду система, активно используемая в некоторой области, развиваемая и сопровождаемая на протяжении значительного времени. Статья не касается исследовательских ОС, разработанных обычно с целью проверки некоторых идей. Рассматривается декомпозиция задача верификации ОС на подзадачи верификации ее различных частей и отдельных свойств и применение для этого разнообразных методов верификации. В статье делается попытка описать и осмыслить опыт, полученный в рамках нескольких проектов по верификации различных частей ОС в ИСП РАН.
Скачать
Технология передачи пакетов с принудительной буферизацией традиционно используется в современных сетевых устройствах, таких как коммутаторы и маршрутизаторы. Но иногда она является существенным препятствием для улучшения качества обслуживания, поскольку минимальное время доставки пакета ограничено произведением количества промежуточных узлов на время передачи пакета в канале. Технология сквозной передачи пакетов устраняет это ограничение, так как для переадресации пакета используется только заголовок пакета, который содержит адрес назначения. Таким образом, технология сквозной передачи пакетов имеет значительные возможности для улучшения качества обслуживания. Модели вычислительной решетки со сквозной коммутацией пакетов были разработаны в форме раскрашенных сетей Петри. Модель состоит из узлов коммутации пакетов и генераторов трафика; который может быть представлен в виде моделей пушек генерирующих злонамеренный трафик, замаскированный под обычный мультимедийный. Настоящая работа – это дальнейшее развитие методов анализа прямоугольных коммуникационных решеток для узлов, реализующих сквозную коммутацию пакетов. Методы предназначены для применения при проектировании вычислительных решеток, в разработке новых телекоммуникационных устройств и в интеллектуальных системах защиты. Предварительные оценки показывают, что технология сквозной коммутации пакетов наследует некоторые негативные эффекты, которые ассоциируются с традиционной доставкой пакетов с принудительной буферизацией. Серия экспериментов с моделью выявила возможность блокировки решетки в условиях рабочей нагрузки. Полученные результаты применимы для интеллектуального обнаружения вторжений и планирования противодействия злонамеренному трафику.
Скачать
В статье представлены подходы к проектированию и реализации программного обеспечения для подготовки нормализованной воды, архитектура, полученные автоматные диаграммы данного процесса, основанные на спецификациях и требованиях. Обсуждаются компоненты системы, уровни абстракции, точки верификации, проблемы при разработке приложения. Показан способ разработки подобных надежных систем.
Скачать
Разыменование нулевого указателя остаётся одной из основных проблем в современных объектно-ориентированных языках. Очевидное добавление ключевых слов, чтобы различать между всегда ненулевыми и возможно нулевыми ссылками, оказывается недостаточным во время инициализации объекта, когда некоторые поля, объявленные как всегда ненулевые, могут временно быть нулевыми до окончания инициализации. Предлагаемое решение избегает явного кодирования этих промежуточных состояний в текстах программ в пользу статически проверяемых правил допустимости, которые не зависят от специальных условно ненулевых типов. Рассматриваются примеры инициализации объектов, предложенные ранее, и представляются новые для сравнения применимости различных подходов. Удобство использования предлагаемой схемы оценивается на открытых библиотеках с миллионом строк кода, которые были адаптированы, чтобы удовлетворять этим правилам.
Скачать
Данная работа представляет дальнейшее развитие метода верификации финитной итерации. Она расширяет смешанную аксиоматическую семантику, предложенную для верификации C-light программ. Это расширение включает в себя метод верификации финитной итерации над неизменяемыми массивами с выходом из цикла в C-light программах. Метод содержит правило вывода для итерации без инвариантов, которое использует специальную функцию, выражающую действие тела цикла. Это правило было реализовано в генераторе условий корректности, являющемся частью нашей системы верификации C-light программ. Для доказательства порождённых условий корректности используется индукция, вызывающая сложности у SMT-решателей. На стадии доказательства в нашей системе используется SMT-решатель Z3. Для преодоления упомянутой трудности была предложена стратегия переписывания условий корректности. Она позволяет автоматически верифицировать финитную итерацию в Z3. Также статья описывает применение доказателя теорем PVS для автоматического доказательства подобных условий корректности. Рассмотрен пример, иллюстрирующий применение этих методов.
Скачать
Целью этого исследования является демонстрация возможности автоматизированной миграции программного кода на новый набор библиотек. Задача миграции кода – не редкость в современных программных проектах. Например, такая задача может возникнуть, когда необходимо перенести проект на другую библиотеку или на другую программную платформу. Разработанный в данной работе метод и прототип инструмента миграции основаны на ранее созданном авторами формализме для описания семантики библиотек. Данный формализм предлагает описывать поведение библиотек с помощью системы расширенных конечных автоматов. В статье представлена метамодель программных библиотек, а также простой в использовании DSL для описания конкретных библиотек. Представленная метамодель напрямую формирует метод миграции, также описанный в данной статье. Процесс миграции разбит на пять шагов, и для каждого шага предложен алгоритм выполнения. Рассмотренные модели и алгоритмы реализованы в прототипе инструмента автоматизированной миграции программного кода. Разработанный прототип инструмента был протестирован на нескольких синтетических примерах кода, а также на реальном проекте. Результаты эксперимента показывают, что миграция кода может быть успешно автоматизирована, и разработанный прототип служит доказательством концепции. Созданные модели и алгоритмы формируют основу для более мощных методов и инструментов миграции.
Скачать
В статье представлен подход к реализации статической проверки типов для динамически-типизированного языка Jolie.
Скачать
За последние годы создано значительное количество структурированных данных как научными, так и коммерческими организациями. На базе этих данных разрабатываются многочисленные приложения, что делает более важным и нужным знакомство с этим направлением современных ИТ-специалистов. В данной работе обсуждаются как важные аспекты эволюции направления Semantic Web, так и опыт преподавания методов и средств Semantic Web.
Скачать
Описываются оптимизирующие трансформации склеивания переменных, замены хвостовой рекурсии циклом, открытой подстановки, упрощения и оформления. Результатом трансформаций является эффективная императивная программа. Используется потоковый анализ, включающий построение графа вызовов и определение области жизни переменных программы.