Системная информатика, 2013, № 1

В статье представлены объектная модель и язык предметно-ориентированных систем переходов — нового формализма, предназначенного для спецификации и апробации формальных методов обеспечения надежности программного обеспечения.

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

В статье описан подход к созданию вычислительных платформ на примере UGENE Workflow Designer. Эта платформа, основанная на внутреннем языке программирования UWL, демонстрирует, как, следуя принципам внутренней модели платформы и синтаксиса языка программирования, сохранять систему целостной и удобной для развития и поддержки. Система UGENE Workflow Designer предназначена для решения задач биоинформатики, а язык UWL является DSL языком этой области. В статье описаны и обоснованы возможности использования этой вычислительной платформы в качестве основы переиспользования ее средств в некоторых других прикладных областях.

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

Отличительной чертой проекта C-light является максимальное использование формальных непротиворечивых методов. Это касается не только фундаментальных базисов для верификации, таких как операционная семантика Плоткина или логика Хоара, но и реализационных аспектов. Одним из таких моментов является локализация потенциальных ошибок. В большинстве известных систем верификации локализация ошибок просто реализуется программистами как часть функционала системы без подведения какой-либо формальной основы под этот процесс. В свете недавнего расширения проекта C-light техникой семантической разметки и выбора инструментария LLVM/Clang для входного блока системы мы приводим обзор наших наработок для решения этой задачи.

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

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