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

Скачать

Предметно-ориентированные системы переходов: объектная модель и язык

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

Верификация мультиагентной модели протокола скользящего окна

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

Языковые средства организации вычислений в области биоинформатики

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

Онтологический подход к проблеме классификации компьютерных языков: состояние и перспективы

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

Комплексный подход к локализации ошибок при верификации Си-программ

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

Исследование стрип-метода обработки сигналов и изображений

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

Подход к созданию исследовательской информационной системы с документально подтверждаемой информацией

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