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

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

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

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

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

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

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