Последний номер
Последний номерСвежий номер (#№ 25, 01.12.2024)
Скачать выпуск целиком (2.15 МБ)
Улучшение генерации условий корректности для Reflex программ с помощью простого статического анализа
Системы управления играют решающую роль в различных областях, требующих высокой надежности и подтверждения правильности работы программного обеспечения. Для решения этой проблемы используются формальные методы, такие как дедуктивная верификация, которые математически обеспечивают корректность программного обеспечения, критически важного для безопасности. Этот процесс включает в себя генерацию условий корректности на основе аксиоматической семантики...
Подход к автоматизации дедуктивной верификации процесс-ориентированных программ, основанный на шаблонах
Процесс-ориентированное программирование — это подход к разработке управляющего программного обеспечения, в котором программа определяется как набор взаимодействующих процессов. PoST — это процесс-ориентированный язык, который является расширением язык ST из стандарта IEC 61131-3. В области разработки управляющего программного обеспечения формальная верификация играет важную роль вследствие необходимости обеспечения высокой надежности такого программного...
Точный тест планируемости для систем реального времени с абстрактным планировщиком
В этой статье мы формально описываем системы реального времени с абстрактным планировщиком, используя модели Крипке. Эта формализация позволяет специализировать абстрактный планировщик в терминах построенной модели. Мы иллюстрируем этот подход с помощью системы реального времени, в которой работы являются невытесняемыми и имеют фиксированный приоритет (NE-GFP). Мы также формулируем свойство безопасности для...
Интервальная итерация на основе политики для вероятностной проверки модели
Вероятности достижимости и ожидаемые вознаграждения - это два важных класса свойств, которые используются при проверке вероятностной модели. Для вычисления базовых свойств применяются итерационные численные методы. Чтобы гарантировать достоверность результатов вычислений, используется метод интервальных итераций. Этот метод использует два вектора в качестве верхней и нижней границ значений и использует стандартный метод...
В статье представлены объектная модель и язык предметно-ориентированных систем переходов — нового формализма, предназначенного для спецификации и апробации формальных методов обеспечения надежности программного обеспечения.
Многие варианты коммуникационного протокола
скользящего окна, который предназначен обеспечивать надежную
передачу данных по ненадежным каналам, были специфицированы и
верифицированы с использованием различных техник проверки, таких
как доказательство теорем, проверка моделей и их комбинаций. В
данной работе предлагается рассмотреть спецификацию протокола
скользящего окна как мультиагентной модели. Темпоральные и
эпистемические свойства протокола сформулированы с помощью логики
знаний и времени.
В статье описан подход к созданию вычислительных платформ на примере 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 шифрования/дешифрования, вычисления функции нечёткой логики и решения уравнения Лапласа. Преимуществами вычислений на сетях Слепцова являются наглядный графический язык, сохранение естественного параллелизма предметной области, мелкая грануляция параллельных вычислений, формальные методы верификации параллельных программ, быстрые массово-параллельные архитектуры, реализующие модель вычислений.
Описываются оптимизирующие трансформации для операций над списками и деревьями в системе предикатного программирования. Кодирование операций представлено набором правил, определяющих замену исходной операции на ее образ в императивном языке. Результатом трансформаций является императивная программа по эффективности сравнимая с написанной вручную.
В статье описан подход к организации процесса извлечения информации из протоколов клинических испытаний под управлением онтологии. Рассмотрены отдельные компоненты модели знаний, включая семантический словарь, жанровую модель текста, онтологию клинических испытаний, и приведены примеры ситуаций.
Ontological Approach to Organizing Specification Patterns in the Framework of Support System for Formal Verification of Distributed Program Systems
Онтологический подход к организации шаблонов требований в рамках системы поддержки формальной верификации распределенных программных систем
(стр. 111-132)
В статье описывается структура онтологии шаблонов требований, извлекаемых из текстов технической документации. Эта онтология комбинирует шаблоны известных классификаций требований с новыми шаблонами. Язык онтологии допускает запись булевых комбинаций шаблонов следующих типов: качественных, реального и ветвящегося времени, с комбинированными событиями, количественными характеристиками событий и простыми утверждениями о данных. Приведены примеры шаблонов требований к реальной системе управления вакуумированием Большого солнечного вакуумного телескопа. Изложена схема интеллектуальной системы поддержки формальной верификации распределенных программных систем.
В статье предлагается понятие концептуальной модели языка программирования. Этот формализм представляет типы языка программирования, значения, исключения, состояния и выполнимые конструкции абстрактной машины языка программирования, и ограничения для этих сущностей на концептуальном уровне. Представляется новое определение концептуальных систем переходов, ориентированное на спецификацию концептуальных моделей языков программмирования, описывается язык переопределенных концептуальных систем переходов CTSL, и предлагается техника использования CTSL в качестве предметно-ориентированного языка спецификации концептуальных моделей языков программирования. Концептуальные модели для семейства простых языков программирования иллюстрируют эту технику.
В статье предлагается понятие концептуальной операционной семантики языка программирования. Этот формализм представляет операционную семантику языка программирования в терминах его концептуальной модели, основанной на концептуальных системах переходов. Определяется специальный вид концептуальных систем переходов - операционные концептуальные системы переходов, ориентированный на спецификацию концептуальной операционной семантики языков программирования, описывается расширение языка концептуальных систем переходов CTSL для операционных концептуальных систем переходов, и предлагается техника использования расширенного CTSL в качестве предметно-ориентированного языка спецификации концептуальной операционной семантики программных языков. Концептуальная операционная семантика для семейства модельных языков программирования иллюстрирует эту технику.
В работе рассматриваются эксперименты с конечными полуавтоматами, направленные на идентификацию финального (текущего) состояния проверяемой системы после подачи соответствующей входной последовательности. В исследуемой модели действия разделены на входные и выходные, однако в модели отсутствуют специально выделенные семейства начальных и финальных состояний. В статье определяются подходящий синхронизирующий и установочный эксперименты, и предлагаются методы их синтеза для специального класса входо-выходных полуавтоматов, у которых в каждом состоянии определены переходы или только по входным, или только по выходным действиям, а также в графе переходов отсутствуют циклы по выходным символам. Для описанного класса входо-выходных полуавтоматов устанавливаются необходимые и достаточные условия существования безусловных синхронизирующего и установочного экспериментов.
В статье рассказывается о недавних достижениях на пути к строгой верификации промышленных операционных систем (ОС). Под промышленной ОС имеется в виду система, активно используемая в некоторой области, развиваемая и сопровождаемая на протяжении значительного времени. Статья не касается исследовательских ОС, разработанных обычно с целью проверки некоторых идей. Рассматривается декомпозиция задача верификации ОС на подзадачи верификации ее различных частей и отдельных свойств и применение для этого разнообразных методов верификации. В статье делается попытка описать и осмыслить опыт, полученный в рамках нескольких проектов по верификации различных частей ОС в ИСП РАН.
Технология передачи пакетов с принудительной буферизацией традиционно используется в современных сетевых устройствах, таких как коммутаторы и маршрутизаторы. Но иногда она является существенным препятствием для улучшения качества обслуживания, поскольку минимальное время доставки пакета ограничено произведением количества промежуточных узлов на время передачи пакета в канале. Технология сквозной передачи пакетов устраняет это ограничение, так как для переадресации пакета используется только заголовок пакета, который содержит адрес назначения. Таким образом, технология сквозной передачи пакетов имеет значительные возможности для улучшения качества обслуживания. Модели вычислительной решетки со сквозной коммутацией пакетов были разработаны в форме раскрашенных сетей Петри. Модель состоит из узлов коммутации пакетов и генераторов трафика; который может быть представлен в виде моделей пушек генерирующих злонамеренный трафик, замаскированный под обычный мультимедийный. Настоящая работа – это дальнейшее развитие методов анализа прямоугольных коммуникационных решеток для узлов, реализующих сквозную коммутацию пакетов. Методы предназначены для применения при проектировании вычислительных решеток, в разработке новых телекоммуникационных устройств и в интеллектуальных системах защиты. Предварительные оценки показывают, что технология сквозной коммутации пакетов наследует некоторые негативные эффекты, которые ассоциируются с традиционной доставкой пакетов с принудительной буферизацией. Серия экспериментов с моделью выявила возможность блокировки решетки в условиях рабочей нагрузки. Полученные результаты применимы для интеллектуального обнаружения вторжений и планирования противодействия злонамеренному трафику.
В статье представлены подходы к проектированию и реализации программного обеспечения для подготовки нормализованной воды, архитектура, полученные автоматные диаграммы данного процесса, основанные на спецификациях и требованиях. Обсуждаются компоненты системы, уровни абстракции, точки верификации, проблемы при разработке приложения. Показан способ разработки подобных надежных систем.
Разыменование нулевого указателя остаётся одной из основных проблем в современных объектно-ориентированных языках. Очевидное добавление ключевых слов, чтобы различать между всегда ненулевыми и возможно нулевыми ссылками, оказывается недостаточным во время инициализации объекта, когда некоторые поля, объявленные как всегда ненулевые, могут временно быть нулевыми до окончания инициализации. Предлагаемое решение избегает явного кодирования этих промежуточных состояний в текстах программ в пользу статически проверяемых правил допустимости, которые не зависят от специальных условно ненулевых типов. Рассматриваются примеры инициализации объектов, предложенные ранее, и представляются новые для сравнения применимости различных подходов. Удобство использования предлагаемой схемы оценивается на открытых библиотеках с миллионом строк кода, которые были адаптированы, чтобы удовлетворять этим правилам.
Данная работа представляет дальнейшее развитие метода верификации финитной итерации. Она расширяет смешанную аксиоматическую семантику, предложенную для верификации C-light программ. Это расширение включает в себя метод верификации финитной итерации над неизменяемыми массивами с выходом из цикла в C-light программах. Метод содержит правило вывода для итерации без инвариантов, которое использует специальную функцию, выражающую действие тела цикла. Это правило было реализовано в генераторе условий корректности, являющемся частью нашей системы верификации C-light программ. Для доказательства порождённых условий корректности используется индукция, вызывающая сложности у SMT-решателей. На стадии доказательства в нашей системе используется SMT-решатель Z3. Для преодоления упомянутой трудности была предложена стратегия переписывания условий корректности. Она позволяет автоматически верифицировать финитную итерацию в Z3. Также статья описывает применение доказателя теорем PVS для автоматического доказательства подобных условий корректности. Рассмотрен пример, иллюстрирующий применение этих методов.
Целью этого исследования является демонстрация возможности автоматизированной миграции программного кода на новый набор библиотек. Задача миграции кода – не редкость в современных программных проектах. Например, такая задача может возникнуть, когда необходимо перенести проект на другую библиотеку или на другую программную платформу. Разработанный в данной работе метод и прототип инструмента миграции основаны на ранее созданном авторами формализме для описания семантики библиотек. Данный формализм предлагает описывать поведение библиотек с помощью системы расширенных конечных автоматов.
В статье представлена метамодель программных библиотек, а также простой в использовании DSL для описания конкретных библиотек. Представленная метамодель напрямую формирует метод миграции, также описанный в данной статье. Процесс миграции разбит на пять шагов, и для каждого шага предложен алгоритм выполнения.
Рассмотренные модели и алгоритмы реализованы в прототипе инструмента автоматизированной миграции программного кода. Разработанный прототип инструмента был протестирован на нескольких синтетических примерах кода, а также на реальном проекте. Результаты эксперимента показывают, что миграция кода может быть успешно автоматизирована, и разработанный прототип служит доказательством концепции. Созданные модели и алгоритмы формируют основу для более мощных методов и инструментов миграции.
В статье представлен подход к реализации статической проверки типов для динамически-типизированного языка Jolie.
За последние годы создано значительное количество структурированных данных как научными, так и коммерческими организациями. На базе этих данных разрабатываются многочисленные приложения, что делает более важным и нужным знакомство с этим направлением современных ИТ-специалистов. В данной работе обсуждаются как важные аспекты эволюции направления Semantic Web, так и опыт преподавания методов и средств Semantic Web.
Описываются оптимизирующие трансформации склеивания переменных, замены хвостовой рекурсии циклом, открытой подстановки, упрощения и оформления. Результатом трансформаций является эффективная императивная программа. Используется потоковый анализ, включающий построение графа вызовов и определение области жизни переменных программы.
В статье представлены итоги работы 4-й Международной конференции «Развитие вычислительной техники в России и странах бывшего СССР: история и перспективы» (SoRuCom-2017) Зеленоград, Москва, 3-5 октября 2017 г., в организации которой ИСИ СО РАН принимал самое активное участие. Поддержку конференции оказал Российский фонд фундаментальных исследований, Грант 17-07-20538, Computer History Museum (USA, CA), российский гражданин Владимир Курляндчик.
В данной работе представлен логико-вероятностный метод адаптивного управления модульными системами, основанный на использовании свойств функциональной схожести модулей и логико-вероятностного алгоритма направленного поиска правил. Предложенный метод основан на совместном обучении управляющих модулей, начиная с поиска общих для всех модулей управляющих правил и закачивая их последующей спецификацией в соответствии с идеями вероятностного логического вывода. С помощью интерактивного 3D-симулятора были проведены успешные эксперименты с четырьмя виртуальными моделями роботов. Экспериментальные исследования показали, что предложенный подход достаточно эффективный и может быть использован для управления модульными системами с большим количеством степеней свободы.
В статье предлагается метод поиска информации на основе онтологии научной деятельности. Для поиска используются глобальные поисковые системы, которым отправляются автоматически сгенерированные поисковые запросы, включающие названия сущностей онтологии и термины тезауруса. Поисковые запросы формируются таким образом, чтобы найти как можно больше научных ресурсов, релевантных определенной области знаний. При этом результаты поиска, не содержащие информации о научной деятельности, отфильтровываются с использованием онтологии.
В статье рассмотрена двадцатилетняя история и опыт создания автоматизированных систем проверки знаний и навыков по программированию в Новосибирском государственном университете. Приведен анализ эффективности или неэффективности методов и средств в использующихся системах проверки знаний. Описано современное состояние архитектуры системы NSUts.
Статья посвящена проблеме факторизации определений языков и систем программирования. В качестве основного параметра факторизации выбрана семантическая декомпозиция в рамках анализа парадигм программирования. Такой выбор позволяет выделять автономно развиваемые типовые компоненты систем программирования. Типовые компоненты должны быть приспособлены к конструированию различных информационных систем. Кроме того, их существование позволяет формировать методику обучения разработке компонентов информационных систем. Попутно показана дистанция в понятийной сложности между программированием и разработкой систем программирования.
Рассматривается подход к разработке и реализации такого вида паттернов онтологического проектирования, как паттерны содержания. Использование паттернов содержания при построении онтологии научной предметной области позволяет, с одной стороны, обеспечить единообразное и согласованное представление всех сущностей разрабатываемой онтологии, с другой – сэкономить человеческие ресурсы и избежать типичных ошибок онтологического моделирования.
Описывается технология предикатного программирования для реализации параллельной программы решения системы линейных уравнений методом Гаусса-Жордано. Предикатная программа изначально параллельна и не требует распараллеливания. Описывается построение предикатной программы и ее оптимизирующая трансформация с получением эффективной параллельной императивной программы.
Дедуктивная верификация намного проще и быстрее для предикатных программ, чем для аналогичных императивных программ. Для любой программы на языке Си можно построить эквивалентную предикатную программу, провести её дедуктивную верификацию, применить к ней набор оптимизирующих трансформаций и в результате получить исходную программу на языке Си.
Данный метод иллюстрируется для известной библиотечной программы конкатенации строк strcat. Описывается построение, дедуктивная верификация и оптимизирующая трансформация предикатной программы конкатенации строк как объектов алгебраического типа «список» в языке предикатного программирования. Разработан аппарат сканирования списков и новый метод кодирования списков через массивы.
В статье вводится понятийный аппарат для сложных алгоритмов управления, представленный в виде математической модели. Для демонстрации практической ценности модели, описываются грамматика и семантика процесс-ориентированного языка, известного под названием Reflex, или "Си с процессами". Выразительные свойства языка показаны на примере разработки алгоритма управления сушилки для рук. Также представлены результаты практической апробации языка.
В 2008-2013 гг. в Институте систем информатики им. А.П. Ершова развивался сначала проект по исследованию и классификации парадигм языков программирования, а затем – по разработке классификации компьютерных языков, виртуальный мир которых включает тысячи языков программирования, спецификаций, моделирования и множество других языков, которые можно отнести к (пользуясь терминологией, сложившейся в биологии) разным царствам, классам, семействам и так далее. В настоящей статье представлена сумма основных теоретических результатов исследований 2008-2013 гг. по классификации компьютерных языков (которые, по нашему мнению, остаются актуальными и на сегодняшний день) и обсуждаются новые подходы к задаче разработки портала знаний о компьютерных языках (вернее – его наполнении) с использованием научной периодики и современных лингвистических технологий (вместо размеченных источников в Интернете).
Актуальность продолжения исследований по классификации компьютерных языков обусловлена познавательным значением такой классификации, а разработки портала знаний о классификации компьютерных языков – потребностями практики объективного выбора компьютерных языков по спецификации программных проектов.
В статье представлен анализ созданной в ИСИ СО РАН библиотеки PolarDB работы со структурированными данными. Это – библиотека классов, реализованная на платформе .NET Core. Она предназначена для создания систем структурирования, хранения и обработки данных, в том числе большого и очень большого объема. Библиотека построена на ранее разработанной системе рекурсивной типизации и охватывает ряд существенных задач, таких как структурирование данных, сериализация, отображение данных на байтовые потоки, индексные построения, блочная реализация динамических байтовых потоков, распределение данных и обработки данных, резервное копирование и восстановление. Применение библиотеки PolarDB позволяет создавать эффективные решения для специализированных баз данных в разных парадигмах: последовательности, реляционные таблицы, key-value хранилища, графовые структуры
Статья посвящена проблемам извлечения языковых конструкций, в том числе числовых и символьных данных, значимых для заданной предметной области. Предложен подход к описанию естественно-языковых конструкций с помощью лексико-семантических шаблонов и рассмотрен язык описания шаблонов на основе языка YAML. Лексико-семантический шаблон – это структурный образец целевой языковой конструкции с указанным составом и лексико-семантическими свойствами. В случае успешного сопоставления шаблона с фрагментом текста формируется лексический объект, которому приписываются формальные (позиционные) и семантические (класс и свойства) характеристики. В статье представлена архитектура веб-редактора для разработки и тестирования лексико-семантических шаблонов и описан эксперимент по созданию двух специализированных словарей: 1) словарь наименований институтов, должностей, званий и их сокращений и 2) словарь числовых/временных конструкций. Создаваемая технология поддерживает лексико-семантический анализ текста на основе шаблонов и может быть использована как независимо при решении задачи извлечения информации из небольших текстов, так и в составе других систем извлечения информации. Предлагаемый метод эффективен для распознавания параметрических конструкций, содержащих оценку значений параметров объектов (сущностей или событий) предметной области.
Статья посвящена проблемам автоматического построения терминологической системы предметной области. Предложен метод извлечения терминов предметной области на базе электронных энциклопедических источников данных. Особенностью предлагаемого подхода является тщательный анализ структуры термина, распознавание ошибок на базе их лингвистической классификации, автоматическая генерация лексико-синтаксических шаблонов, представляющих многокомпонентные термины, и использование набора эвристических методов обработки «особых» терминов. Использование энциклопедических словарей позволяет автоматически сформировать эталонный список наименований понятий и применять его для оценки качества формируемых словарей.
Рефлекс – процесс-ориентированный язык, который обеспечивает простое в сопровождении программное обеспечение для систем управления. Язык был успешно использован в нескольких критически важных с точки зрения безопасности кибер-физических системах, например в управляющем программном обеспечении для печи выращивания монокристаллического кремния. В настоящее время основной целью языкового проекта Reflex является развитие поддержки для автоматизированной разработки программного обеспечения, ориентированного на критически важные с точки зрения безопасности приложения. В данной статье представлена формальная операционная семантика языка Reflex как базис для применения формальных методов для верификации Reflex программ.
During the climb flight of big passenger planes, the pilot directly adjusts the pitch elevator and the plane reacts on this by changing its pitch angle. However, if the pitch angle becomes too large, the plane is in danger of an airflow disruption on the wings, which can cause the plane to crash. In order to prevent this, modern planes take advantage of control software to limit the pitch angle. However, if the software is poorly designed and if system designers have forgotten that sensors might yield wrong data, the software might cause the pitch angle to become negative, so that the plane loses height and can - eventually - crash. In this paper, we investigate on a model for a Boeing passenger plane how the control software could look like. Based on our model described in MatLab/Simulink, it is easy to see based on simulation that the plane loses height when the sensor for the pitch angle provides wrong data. For the opposite case of a correctly functioning sensor, our simulation does not indicate any problems. This simulation, however, is not a guarantee that the control is indeed safe. For this reason, we translated the MatLab/Simulink-model of the controller into a hybrid program in order to make this system amenable to formal verification using the theorem prover KeYmaera
User-friendly formal specification and verification of concurrent systems from various subject domains are active research topics due to their practical significance. In this paper, we present the method for development of verification-oriented domain-specific process ontologies which are used to describe concurrent systems of subject domains. One of advantages of such ontologies is their formal semantics which makes possible formal verification of described systems. Our method is based on the verification-oriented process ontology. For constructing a domain-specific process ontology, our method uses techniques of semantic markup and pattern matching to associate domain-specific concepts with classes of the process ontology. We give detailed ontological specifications of these techniques. Our method is illustrated by the example of developing a domain-specific ontology for typical elements of automatic control systems.
В Институте систем информатики СО РАН разрабатывается система C-light. Это система дедуктивной верификации C программ. Входным языком данной системы является C-light. C-light программа транслируется в C-kernel программу. Метагенератор условий корректности (УК) принимает на вход C-kernel программу и правила вывода для C-kernel. Для элиминации инвариантов циклов в системе C-light используется символический метод верификации финитных итераций. Поэтому, если C-kernel программа содержит финитную итерацию, то метагенератор порождает для нее УК, основанное на операции замены. Такая операция выражает действие цикла в символической форме. Метагенератор помечает подформулы УК семантическими метками, используя расширение метода Денни и Фишера. Если УК не удалось доказать, то система C-light генерирует его объяснение, используя семантические метки. Обратный транслятор сопоставляет строки кода промежуточной C-kernel программы и исходной C-light программы. Но в случае недоказанного УК можно попытаться доказать его ложность. Ложность УК означает несоответствие программы и спецификации. Поэтому, мы разработали и описали в данной статье эвристическую стратегию доказательства ложности УК для системы ACL2.
For many years, automotive embedded systems have been validated only by testing. In the near future, Advanced Driver Assistance Systems (ADAS) will take a greater part in the car’s software design and development. Furthermore, their increasing critical level may lead authorities to require a certification for those systems. We think that bringing formal proof in their development can help establishing safety properties and get an efficient certification process. Other industries (e.g. aerospace, railway, nuclear) that produce critical systems requiring certification also took the path of formal verification techniques. One of these techniques is \emph{deductive proof}. It can give a higher level of confidence in proving critical safety properties and even avoid unit testing.
In this paper, we chose a production use case: a function calculating a square root by linear interpolation. We use deductive proof to prove its correctness and show the limitations we encountered with the off-the-shelf tools. We propose approaches to overcome some limitations of these tools and succeed with the proof. These approaches can be applied to similar problems, which are frequent in automotive embedded software.
Модель конечного автомата широко используется при анализе и синтезе цифровых компонентов управляющих систем. Для того чтобы учитывать временные аспекты в поведении таких систем, вводятся различные виды временных автоматов. В настоящей работе, мы исследуем проблему построения параллельной композиции автоматов с временными ограничениями и выходными задержками (выходными таймаутами). Компоненты параллельной композиции взаимодействуют в режиме диалога, и композиция выдает внешний выходной символ, когда диалог между компонентами завершается. В данной статье, мы формально определяем оператор параллельной композиции для автоматов с временными ограничениями (временных автоматов) и показываем, что в отличие от классических автоматов, наличие "медленной внешней среды" не является достаточным условием для описания параллельной композиции детерминированных временных автоматов автоматом того же класса, и таким образом, множество детерминированных автоматов с временными ограничениями не является замкнутым относительно операции параллельной композиции. В работе также рассматриваются некоторые классы детерминированных временных автоматов, замкнутые относительно этой операции.
Russell — это логический каркас, предназначенный для спецификации и реализации дедуктивных систем. Он является языком высокого уровня по отношению к языку Metamath, поэтому он наследует основания Metamath, то есть не зависит от какого либо конкретного формального исчисления, но является чистым логическим каркасом. Основная разница между Russell и Metamath заключается в языке доказательств и подходу к синтаксису: доказательства в Russell имеют декларативную форму, то есть содержат явно выражения, составляющие доказательство, а синтаксические правила грамматики разделены в Russell с содержательными правилами вывода.
Russell реализован на c++14 и распространяется по лицензии GPL v3. Репозиторий содержит транслятор из Metamath в Russell и обратно. Оригинальная база теорем Metamath (почти 30 000 теорем) транслируется в Russell, верифицируется, транслируется обратно в Metamath и верифицируется оригинальным верификатором Metamath. Адрес репозитория: https://github.com/dmitry-vlasov/russell.
A Method to Verify Parallel and Distributed Software in C# by Doing Roslyn AST Transformation to a Promela Model
Метод верификации параллельного и распределенного программного обеспечения на C# путем проведения трансформации абстрактного синтаксического дерева Roslyn в модель на Promela
(стр. 13-44)
В статье мы описываем подход для формальной проверки параллельных и распределенных программ на C#. Мы используем технологию Microsoft Roslyn для получения синтаксической и семантической информации об интересных конструкциях в реальном коде, чтобы сгенерировать соответствующий код на модельном языке Promela, предназначенном для описания взаимодействующих систем на основе акторов. Затем мы проверяем проблемы параллельного и распределенного кода, используя предопределенные предикаты LTL для модельной программы. Мы можем определять проблемы гонки данных, неправильное использование блокировок, возможные взаимоблокировки в распределенных сервисных взаимодействиях с использованием подхода проверки модели. Описанный метод может быть использован для построения статического анализатора для платформы .NET.
Описывается построение и дедуктивная верификация предикатной программы бинарного поиска, идентичной программе bsearch на языке Си из библиотеки ОС Linux. В языке предикатного программирования определяются новые конструкции для произвольных типов в качестве параметров программ. Для объектов произвольного типа вводятся трансформации кодирования через указатели.
В статье представлены результаты исследования изменений, происходящих в тематических кластерах, построенных на коллекции текстов конференций предметной области Argument mining. Выявление терминов, установление связей между ними и тематическая кластеризация проведены с помощью сторонних программных средств, позволяющей извлекать термины в форме именных словосочетаний, проводить их кластеризацию на базе алгоритма, основанного на применении функции модулярности. Приводится оценка качества полученных кластеров по трем критериям. Трансформацию терминологического состава кластеров во времени предлагается анализировать с помощью ориентированных графов, построенных на основе критерия, который позволяет фиксировать наиболее важные изменения. Терминологическая лексика выявленных тематических кластеров характеризует отдельные направления, в которых ведутся исследования, а трансформация терминологического состава кластеров во времени демонстрирует смещение интересов.
Цель статьи — описание методики сравнения языков программирования, удобной при исследовании выразительной силы языков и сложности систем программирования. Методика приспособлена к учёту практичных критериев, которые можно рассматривать как подход к решению проблемы факторизации сложных определений языков программирования. Кроме того, в статье представлены результаты анализа наиболее известных языков программирования, основанные на семантических характеристиках парадигм, систематизированных как порядок принятия решений в процессе подготовки и отладки программ. Понятие «парадигма программирования» определяется как способ мышления в процессе программирования. Автор особенно благодарен организаторам и участникам конференций «Научный сервис в среде Интернет» (http://agora.guru.ru/display.php?conf=abrau2020&page=subjects&PHPSESSID=qbn3kbhgnk8b6a9g21qi1nkkq2 ), содержание которых способствовало пониманию основных результатов статьи.
В статье рассматриваются вопросы реализации адаптивности в интеллектуальных системах дистанционного обучения, основанной на технологии адаптивной гипермедиа и моделях индивидуальных стилей обучения.
интеллектуальные системы дистанционного обучения, адаптивные системы, архитектура интеллектуальных систем обучения, адаптивные обучающие гипермедиа-системы, адаптивная гипермедиа, адаптивное представление, адаптивная навигация, индивидуальные стили обучения, модель Колба, модель Хани-Мамфорда, модель Фельдера-Сильверман, модель когнитивных характеристик, таксономия Блума
В данной работе рассматривается эволюция понятия «граф знаний» с момента возникновения и до текущего момента. Также рассматривается вопрос о том, как эволюция систем, позиционирующих себя как графы знаний, повлияла на определение и жизненный цикл графов знаний.
Проводится дедуктивная верификация алгоритма классической пирамидальной сортировки Дж. Вильямса, реализованного программой sort на языке Си в библиотеке ОС Linux. Сортировка реализуется для объектов произвольного типа. Чтобы упростить верификацию, применяются нетривиальные трансформации, заменяющие арифметические операции с указателями явными элементами сортируемого массива. Программа преобразуется на язык предикатного программирования. Конструируются спецификации предикатной программы. Дедуктивная верификация в системах Why3 и Coq оказалась сложной и трудоемкой.
Описывается трансформация программы memweight из библиотеки ОС Linux, устраняющая указатели. Далее программа трансформируется на язык предикатного программирования P. Для предикатной программы, полученной в результате серии упрощающих трансформаций, строится спецификация и проводится дедуктивная верификация. Для упрощения верификации в рамках спецификации строится модель внутреннего состояния исполняемой программы. Верификация программы memweight реализована в системе автоматического доказательства Why3.
Выделение именованных сущностей (NER) - это задача извлечения из текстовых данных информации, принадлежащей к заранее определенным категориям, таким как названия организаций, топонимы, имена людей и т.п. В рамках представленной работы был разработан подход, развивающий идеи предшественников по дообучению глубоких нейроных сетей с механизмом внимания архитектуры BERT. Показано, что предварительное обучение языковой модели задачам восстановления маскированного слова и определению семантической связанности двух предложений позволяет заметно улучшить показатели качества решения задачи выделения именованных сущностей. Достигнут один из лучших результатов в задаче выделения именованных сущностей на наборе данных RuREBus, содержащем тексты распорядительных документов министерства экономического развития Российской Федерации. Одной из ключевых особенностей описываемого решения является близость постановки к реальным бизнес-задачам и выделение сущностей не общебытового характера, а специфичных для экономической отрасли.
В статье представлено исследование эффективности использования признака принадлежности утверждений, участвующих в аргументации, к одному тематическому фрагменту текста. Работа проводилась с целью последующего применения этого признака в автоматическом распознавании аргументационных структур. Объектом исследования служили русскоязычные тексты научно-популярного жанра. Тематическая структура текста строилась на основе выявления сверхфразовых единств (фрагментов текста, объединенных одной темой) путем обнаружения кластеров слов и словосочетаний с помощью сканирующих статистик. Для верификации потенциально возможных связей, извлекаемых из тематической структуры, использовались тексты с ручной разметкой аргументационной структуры. Сопоставление связей, построенных «вручную» и потенциальных, определяемых из тематической структуры, проводилось автоматически. Полученные с макро-усреднением точность и полнота составили 48,6 % и 76,2 % соответственно.
Идентификация состояний является хорошо известной задачей теории конечных автоматов, в частности, установочные последовательности позволяют идентифицировать текущее состояние конечного автомата и широко используются в областях тестирования и верификации программного обеспечения. Для различных классов автоматов сформулированы необходимые и достаточные условия существования безусловных и адаптивных установочных последовательностей и алгоритмов их синтеза. Функционирование современного программного и аппаратного обеспечения часто зависит от временных аспектов, что мотивирует исследования в области временных автоматов. В настоящей работе мы исследуем задачу проверки существования и синтеза установочных последовательностей для автоматов с временными ограничениями. Предлагаемый подход основан на использовании конечно автоматной абстракции временного автомата.
Последовательные реагирующие системы - это формальные модели программ, которые взаимодействуют с окружающей средой, получая входные данные и производя соответствующие выходы. Такие формальные модели широко используются в программной инженерии, компьютерной лингвистике, телекоммуникациях и т. д. В реальной жизни поведение реагирующей системы зависит не только от потока входных данных, но также от времени поступления входных данных и задержек, которые возникают при генерации ответов. Чтобы зафиксировать эти аспекты, в качестве формальной модели последовательной реактивной системы в реальном времени используется временный конечный автомат (TFSM). Однако в большинстве известных предыдущих работ эта модель рассматривалась в упрощенной семантике: отклики в потоке на выходе машины, независимо от их временных меток, следуют в том же порядке, в котором соответствующие входные данные доставляются в машину. Это упрощение облегчает анализ модели, но упускает из виду многие важные аспекты вычислений в реальном времени. В этой статье мы изучаем более строгую семантику TFSM и показываем, как ее представить с помощью систем помеченных переходов. Это открывает возможность применения традиционных формальных методов для проверки более тонких свойств реагирующего поведения в реальном времени, которые ранее игнорировались.
Последовательные реагирующие системы, такие как контроллеры, системные драйверы, компьютерные интерпретаторы, работают с двумя потоками данных и преобразуют входные потоки данных (управляющие сигналы, инструкции) в выходные потоки управляющих сигналов (инструкции, данные). Конечные преобразователи широко используются в качестве подходящей формальной модели для подобных систем обработки информации. Поскольку вычисления преобразователей протекают во времени, темпоральная логика, очевидно, может использоваться как простой и выразительный формализм для определения поведения последовательных реагирующих систем. Однако обычные прикладные темпоральные логики (LTL, CTL) плохо подходят для этой цели, поскольку их формулы интерпретируются на омега-языках, тогда как поведение преобразователей представлено бинарными отношениями на бесконечных последовательностях, то есть омега-трансдукциях. Чтобы обеспечить темпоральную логику возможностью учитывать эту общую особенность поведения реагирующих систем, мы ввели новые расширения этой логики. Это расширение характеризуют две отличительные особенности: 1) временные операторы параметризуются наборами потоков (языков), допустимых для ввода, и 2) наборы (языки) ожидаемых выходных потоков используются в качестве базовых предикатов. В предыдущей серии работ мы изучали выразительные возможности и задачу верификации моделей для Reg-LTL и Reg-CTL, которые являются такими расширениями LTL и CTL, где упомянутые выше языки являются регулярными. Мы обнаружили, что такое расширение темпоральной логики увеличивает их выразительную способность, хотя сохраняет разрешимость задачи верификации моделей. Нашим следующим шагом в систематическом изучении выразительных и алгоритмических свойств новых расширений темпоральной логики является анализ проблемы верификации моделей для конечных автоматов-преобразователей относительно формул логики Reg-CTL*. В этой статье мы описываем алгоритм верификации моделей автоматов-преобразователей для форму логики Reg-CTL* и показываем, что эта задача принадлежит классу сложности ExpSpace.
Мы рассматриваем формальную проверку программного обеспечения управления критическими системами, то есть обеспечение отсутствия ошибок проектирования в системе по отношению к требованиям. Системы управления обычно основаны на промышленных контроллерах, также известных как программируемые логические контроллеры (ПЛК). Специфической особенностью ПЛК является цикл сканирования: 1) считываются входы, 2) изменяются состояния ПЛК и 3) записываются выходы. Поэтому для формальной верификации ПЛК, например, путем проверки модели, необходимо рассуждать как в терминах переходов состояний внутри цикла, так и в терминах более крупных переходов состояний в соответствии с семантикой циклов.
Мы разрабатываем формализацию ПЛК как гиперпроцессной системы переходов и основанный на LTL временной логике cycle-LTL для рассуждений о ПЛК.
Описывается дедуктивная верификация программы kstrtoul на языке Си из библиотеки ОС Linux. Программа kstrtoul реализует вычисление целого числа, представленного в виде последовательности литер. Чтобы упростить верификацию, применяются трансформации замены операций с указателями эквивалентными действиями без указателей. Программа преобразуется на язык предикатного программирования. Конструируется модель внутреннего состояния программы как часть спецификации программы. Дедуктивная верификация проведена в системах Why3 и Coq.
Описывается трансформация и верификация программы bus_sort_breadthfirst, принадлежащей ядру ОС Linux и реализующей сортировку устройств, прикрепленных к шине компьютера. Программа трансформируется с языка Си в язык cP с раскрытием макросов, реорганизацией структур и устранением указателей. Далее программа преобразуется на язык функционального программирования WhyML. Для полученной программы строится спецификация и проводится дедуктивная верификация.
В статье представлена модель баз данных, основанная на последовательности объектов. Рассмотрены вопросы сериализации/десериализации объектов, индексных построений, структуры и методов универсальной последовательности и универсального индекса, реализация полного базиса редактирования через использование первичного ключа, временной отметки и «пустого» значения.
Показано, что спецификация на языке Event-B представима автоматной программой в виде недетерминировнной композиции простых условных операторов, что соответствует узкому подклассу автоматных программ. Спецификация в Event-B является монолитной. Для построения спецификации нет других средств композиции, кроме уточнения, реализующего расширение ранее построенной спецификации.
Сравнение технологий автоматного программирования и Event-B проводится на примере двух задач. Предыдущие решения задачи управления движением на мосту в системе Event-B являются сложными и громоздкими. Предложено более простое решение с верификацией программы в инструменте Rodin. Эффективность методов верификации в Event-B подтверждена нахождением трех нетривиальных ошибок в нашем решении.
В статье представлены результаты экспериментов по конъюнктивной декомпозиции различных представлений булевых функций (ZDD, BDD, OKFDD, AIG) методами, которые получаются путем специализации общего алгоритма декомпозиции. Тестовыми наборами являются случайные булевы функции с различными параметрами, а также набор широко известных бенчмарков, используемых для тестирования алгоритмов оптимизации логических схем. В сравнении участвуют последовательная и многопоточная реализация алгоритма.
Methods and technologies for constructing efficient and reliable programs and software systems based on graph models and semantic transformations
Методы и технологии конструирования эффективных и надежных программ и программных систем на основе графовых моделей и семантических преобразований
(стр. 1-14)
В Институте систем информатики СО РАН с 2021 года выполняется проект «Методы и технологии конструирования эффективных и надежных программ и программных систем на основе графовых моделей и семантических преобразований» коллективом сотрудников лабораторий «Конструирования и оптимизации программ» и «Системное программирование» под научным руководством д.ф.-м.н., профессора В. Н. Касьянова. Ответственными исполнителями проекта являются к.ф.-м.н., доцент Е. В. Касьянова и к.т.н. В. И. Шелехов. В данной статье кратко представлены те результаты выполнения первого этапа данного проекта, которые были получены сотрудниками лаборатории «Конструирования и оптимизации программ».
В статье изложены основные научные результаты, полученные лабораторией информационных систем ИСИ СО РАН в 2021, их связь с мировыми исследованиями и работами предыдущих лет.
В статье рассматривается задача оценки возможностей ликвидации транспортной дискриминации для населения Азиатской части России. Предлагается расширение системы моделирования транспортных потоков МИКС-ПРОСТОР в части включения в нее оценок вариантов мультимодальных пассажирских перевозок.
В статье описаны методы автоматического извлечения терминов и связывания их с Викиданными. Преимуществом предложенных методов является потенциальная возможность их применения к любым областям знаний при наличии только неразмеченных текстов и начальных словарей терминов небольшого размера. Для проведения экспериментов был собран и размечен корпус научных текстов RuSERRC. Корпус и модели находятся в открытом доступе и могут быть полезны для дальнейших исследований другими научными коллективами.
Структуры событий – базовая модель теории параллелизма. В литературе выделяются два различных метода построения семантики систем переходов для событийно-ориентированных моделей. Один из них основан на наборах событий, которые произошли в процессе реализации модели, другой – на фрагментах модели, которые остались после частичной реализации модели. В этой статье исследуется наиболее выразительная модель структур событий – структуры событий для разрешимого конфликта (RC-структуры) – и доказывается изоморфизм этих двух типов систем переходов, построенных из RC-структур, в семантиках шага и частичного порядка.
В статье описывается подход к автоматизации извлечения терминологии для пополнения онтологии научной предметной области из текстов на русском языке. Применимость методов автоматического пополнения онтологии из текстов на естественном языке зависит от характеристик корпуса текстов и используемого языка. Специфика входного языка, характеризующегося сильной флективностью и свободным порядком слов, и отсутствие большого корпуса текстов приводят к выбору лингвистического подхода, базирующегося на использовании лексико-семантических паттернов. К особенностям предлагаемой методики извлечения информации относятся а) автоматическое пополнение предметного словаря на основе онтологии и корпуса текстов и разметка его с помощью системы семантических признаков; б) определение небольшого набора исходных структурных мета-паттернов, устанавливающих концептуальные контексты извлечения онтологической информации; в) автоматическое порождение по набору структурных мета-паттернов множества лексико-семантических паттернов, определяющих лексические, семантические и синтаксические свойства контекстов извлечения.
Метод недоопределённых вычислений является одним из подходов для решения задачи удовлетворения ограничений. На его основе разработан ряд программных систем, в том числе система программирования в ограничениях Nemo. В статье рассматриваются принципы, используемые для разработки системы Nemo, их реализация на практике и возможности, предоставляемые пользователю для решения задач.
Введение в изучение методов обеспечения качества необходимо для понимания разработки сложного и надёжного программного обеспечения. Тем не менее, современная индустрия программного обеспечения требует скорейшего вывода продукта на рынок, а методы формальной спецификации и верификации программ не вызывают особого интереса у широкой массы будущих программистов.
В данной статье автор предлагает организовать специальную дисциплину и проводить обучение тестированию, разработке через тестирование и методам формальной верификации с использованием различных методов написания спецификаций и программных средств проверки программ.
Цель настоящей дисциплины — пересмотреть отношение будущих разработчиков к качеству программного обеспечения, его спецификации и необходимости автоматической проверки.
В рамках данной статьи автор рассматривает собственную дисциплину, объединяющую по сути два курса — тестирование программного обеспечения и формальную верификацию. Предлагаемый подход к обучению в первую очередь практико-ориентирован и включает командную работу. В соответствии с действующим учебным планом дисциплина проводится в последнем семестре для студентов бакалавриата (4 курс). Материал статьи основан на пятилетнем опыте преподавания автора данной дисциплины студентам направления “Программная инженерия”. В статье приведены достаточно объемные и наглядные примеры спецификаций и программ на модельных языках.
Работа посвящена эстонскому ученому в области информатики Энну Тыугу (1935–2020). В фокусе статьи два знаковых события в его биографии – это депортация в 1941 году и интерес к компьютерам. Тема представляется актуальной, поскольку в постсоветской (как и в СССР) среде исследования жизненных путей представителей депортированных народов были малочисленны; мы мало знаем об их жизни и жизни их потомков. Мы не будем подробно останавливаться на вопросе доступа специалистов науки и техники (технократов) к политической власти и принятию управленческих решений и ограничимся интересом к их социально-профессиональной идентичности.
Работа посвящена исследованию проблем автоматизации создания онтологий научных предметных областей с применением методов автоматического анализа текстов на естественном языке. Целью работы является разработка методов автоматической генерации лексико-синтаксических шаблонов для извлечения информации и пополнения онтологий на основе анализа содержательных паттернов онтологического проектирования для научных областей знаний, разрабатываемых в рамках концепции Semantic Web. Паттерны онтологического проектирования представляют собой структурированной описание понятий верхнего уровня в терминах классов, атрибутов и отношений, а также включают вопросы оценки компетенции на естественном языке, служащие для понимания и корректной интерпретации свойств и связей понятия пользователями. В статье предложен подход к генерации лексико-синтаксических паттернов на основе вопросов оценки компетенции. Процесс генерации лексико-синтаксических паттернов включает генерацию предметного словаря, выделение сущностей онтологии и формирование структуры паттернов на основе свойств Data Property и Object Property, и генерацию семантических, грамматических и позиционных ограничений. Вопросы оценки компетенции используются для выявления грамматических и позиционных ограничений, необходимых для поиска онтологических отношений в текстах. Для эксперимента использовалась онтология «Поддержка принятия решений в слабоформализованных областях» и корпус научных текстов той же предметной области. В ходе эксперимента получены следующие результаты: степень неоднозначности сгенерированных шаблонов - 1.5, F1-мера оценки качество поиска атрибутов и отношений объектов - F1-мера составила 0,77 для атрибутов и 0,55 для отношений соответственно. Сравнение результатов, полученных для шаблонов без грамматических ограничений, и результатов, полученных для шаблонов с грамматическими ограничениями, показало, что добавление ограничений существенно улучшает качество извлечение объектов онтологии.
Модель памяти описывает требования консистентности памяти в многопоточной системе. Оптимизации компилятора могут нарушить требования консистентности из-за ошибок, и поведение программы будет отличаться от требуемого. Ошибки в оптимизациях компилятора, например, некорректную перестановку инструкций, очень сложно обнаружить, так как они могут возникать с очень небольшим шансом при реальном исполнении. Существуют различные подходы формальной верификации требований консистентности памяти, однако основная сложность состоит в том, что данные подходы не масшабируются на промышленное программное обеспечение. В данное работе представлен инструмент MCC, который был успешно апробирован на виртуальной машине ARK VM и обнаружил реальную ошибку в оптимизации компилятора. Инструмент MCC является статическим, что позволяет проверить все возможные выполнения конкретной тестовой программы, не полагаясь на реальной выполнение на определенной архитектуре. Подход также включает в себя генерацию тестов и спецификацию проверяемых свойств.
Процессно-ориентированное программирование - перспективный подход к разработке управляющего программного обеспечения. Управляющее программное обеспечение часто требует высокой надежности. Формальные методы верификации, в частности дедуктивная верификация, используются для доказательства правильности таких программ относительно требований. Ранее был разработан язык темпоральных требований чтобы специфицировать темпоральные требования для дедуктивной верификации процесс-ориентированных программ. Было также показано, что значительная часть требований относится к небольшому числу классов. Для этих классов были разработаны шаблоны требований. В данной статье мы представляем коллекцию процесс-ориентированных программ и требований к ним. Требования формализованы на языке темпоральных требований и классифицированы в соответствии с набором шаблонов. Мы также определяем новый шаблон требований. Эти результаты могут быть использованы при исследовании формальных методов верификации процесс-ориентированных программ, в частности, при исследовании методов доказательства условий корректности.
Процесс-ориентированное программирование является парадигмой, основанной на понятии процесса, где каждый процесс внутри является параллельным автоматом. Парадигма предназначена для разработчиков ПЛК (программируемых логических контроллеров) чтобы писать программное обеспечение для Industry 4.0.
Язык poST - перспективное процесс-ориентированное расширение языка структурированного текста (ST) стандарта IEC 61131-3, обеспечивающее концептуальную согласованность исходного кода ПЛК с технологическим описанием управляемого процесса. Этот язык сочетает преимущества автоматного программирования со стандартным синтаксисом языка ST. Мы предлагаем трансформационную семантику poST, содержащую правила трансляции poST-операторов в Promela – входной язык системы проверки моделей SPIN. Следуя этим семантическим правилам, наш транслятор, основанный на Xtext, порождает модель на языке Promela для poST-программы.
Нашим вкладом является метод автоматической генерации кода на языке Promela из управляющих программ на языке poST. Полученная в результате Promela-программа может быть верифицирована с помощью системы SPIN относительно требований к исходной программе poST на языке линейной темпоральной логики LTL.
SSA-форма – промежуточное представление для компиляции императивных программ, где каждой переменной значение присваивается лишь единожды. Будучи правильно определённой, SSA-форма порождает семейство чисто синтаксических категорий с несколькими хорошими свойствами. Мы надеемся, что эта работа послужит основанием для категорного подхода к оптимизации.
Генеративные системы искусственного интеллекта должны тщательно тестироваться, поскольку они могут создавать данные плохого качества, однако процесс тестирования осложняется проблемой тестового оракула. Тестирование инвариантами помогает тестировать программы без тестового оракула. В этом исследовании мы рассматриваем систему ИИ для создания персонализированных стикеров. Персонализированный стикер - это тематическая картинка с лицом человека, декоративными элементами и надписями. Данная система состоит из многих компонент и является стохастической. Мы определили требования для системы целиком и проверили их с помощью тестовых инвариантов. Эти требования регулируют зависимости от качества входных изображений и итоговое качество создаваемых стикеров. Наша методика помогла обнаружить значительные проблемы в тестируемой системе.
В статье представлена текущая реализация языкового сервера для интерактивного доказателя теорем Rzk. Она анализирует соответствующие технологии, связанные с языковым сервером Protocol, расширениями VS Code и доказателями теорем, и как на их основе строится языковая поддержка для Rzk.
В статье представлены некоторые наработки автора в области ТРИЗ – теории решения изобретательских задач. Наработки предполагается превратить в программу-ассистента, предназначенную для широкого круга пользователей и широкого круга задач. Предложена модель постановки задачи, в виде расширенного сценарного анализа, далее выявляется сложность, мешающая реализации этого сценария, предлагаются способы разрешения противоречий. В основном, предложенная методика постановки и решения задачи соответствует теории, разработанной и развитой Г.С. Альтшуллером е его учениками. Новое – это модель, объединяющая разные «веточки» теории и практики ТРИЗ.
В работе предлагается подход к автоматическому построению терминологического ядра онтологии по компьютерной лингвистике. Рассматриваются вопросы создания онтологии верхнего уровня, определяющей возможные классы терминов для их дальнейшего поиска и систематизации. Предложен алгоритм генерации и начального пополнения предметного словаря, включающий два основных этапа. На первом шаге строится система лексико-семантических классов, основанных на классах онтологии. На втором шаге осуществляется наполнение словаря терминами и их соотнесение с классами словаря на основе имеющихся ресурсов: универсальной онтологии научного знания, тезауруса и портала по компьютерной лингвистике. Для проведения экспериментального исследования был собран корпус аналитических статей по компьютерной лингвистике с сайта Хабр и созданы наборы данных с разметкой терминов, включающие по 1065 предложений на русском языке. Проведены эксперименты для решения двух задач: обнаружение терминов и их классификация относительно классов онтологии. Для первой задачи были рассмотрены три нейросетевые модели: xlm-roberta-base, roberta-base-russian-v0 и ruRoberta-large. Лучшие результаты получены на последней модели: 0.91 F-меры. Проведен анализ ошибок классификатора, который показал высокую частотность ошибки неполного выделения термина. Для второй задачи была выбрана модель ruRoberta-large, показавшая лучшие результаты для первой задачи. Среднее значение F-меры для 12 используемых классов онтологии составило 0.89. Предложена общая архитектура системы создания и пополнения онтологий, интегрирующая лингвистические подходы и методы машинного обучения.
Представлен отклик на статью С.П. Прохорова «Основополагающий вклад Академии наук СССР в становление компьютерных наук и компьютерных технологий» в журнале «Вестник Российской Академии наук», 2023, т. 93, № 10, с. 980–988.
В статье представлены итоги VI международной конференции по истории информатики «Развитие вычислительной техники в России, странах бывшего СССР и СЭВ» SoRuCom-23. Она была организована 25–27 сентября 2023 г. на базе Нижегородского кампуса НИУ «Высшая школа экономики».
Непрерывно-временные сети Петри (НВСП) — расширение сетей Петри, где каждый переход имеет собственные часы и временной интервал. Данная модель рассматривается в контексте слабой временной стратегии, в которой ход времени не заставляет переходы срабатывать. Для НВСП исследуются эквивалентности в дихотомиях «интерливинг — истинный параллелизм» и «линейное — ветвящееся время». Анализируются взаимосвязи между эквивалентностями относительно промежуточной и устойчиво атомарной стратегий, определяющих порядок сброса часов переходов
непрерывно-временные сети Петри, слабая временная стратегия, промежуточная и устойчиво атомарная стратегии сброса часов, поведенческие эквивалентности, семантика интерливинга, процессно-сетевая семантика, языковая и бисимуляционная эквивалентности, бисимуляционная эквивалентность с сохранением истории
Системы управления играют решающую роль в различных областях, требующих высокой надежности и подтверждения правильности работы программного обеспечения. Для решения этой проблемы используются формальные методы, такие как дедуктивная верификация, которые математически обеспечивают корректность программного обеспечения, критически важного для безопасности. Этот процесс включает в себя генерацию условий корректности на основе аксиоматической семантики программы и ее требований. Основным недостатком ручной генерации условий корректности является ее трудоемкость и подверженность человеческим ошибкам, что приводит к разработке автоматизированных генераторов условий проверки. Однако они создают избыточные или чрезмерно сложные условия проверки, которые неточно отражают возможные пути работы программы. Для устранения второй проблемы были введены предметно-ориентированные языки, такие как Reflex, которые используют процесс-ориентированную парадигму для оптимизации программирования и упрощения генерации условий проверки. Тем не менее, присущая Reflex структура switch-case может привести к увеличению числа условий корректности, усугубляя первую проблему и усложняя выбор подходящих. В данной статье предлагается простая система статического анализа, предназначенная для оптимизации генерации условий корректности для программ Reflex, что повышает эффективность процесса верификации. Она основана на привязке атрибутов к различным операторам. Затем на протяжении всего процесса генерации условий корректности эти атрибуты собираются и проверяются на совместимость с ранее собранными. Если атрибуты несовместимы, то условия корректности отбрасываются.
Процесс-ориентированное программирование — это подход к разработке управляющего программного обеспечения, в котором программа определяется как набор взаимодействующих процессов. PoST — это процесс-ориентированный язык, который является расширением язык ST из стандарта IEC 61131-3. В области разработки управляющего программного обеспечения формальная верификация играет важную роль вследствие необходимости обеспечения высокой надежности такого программного обеспечения. Дедуктивная верификация — это метод формальной верификации, в котором программа и требования к ней представляются в виде логических формул, а для доказательства того, что программа удовлетворяет требованиям, используется логический вывод. К управляющему программному обеспечению часто предъявляются темпоральные требования. Мы формализуем такие требования для процесс-ориентированных программ в виде инвариантов цикла управления. Но инварианты цикла управления, представляющие требования, недостаточны для доказательства корректности программы. Поэтому мы добавляем дополнительные инварианты, которые содержат вспомогательную информацию. В данной статье рассматривается проблема автоматизации дедуктивной верификации процесс-ориентированных программ. Мы предлагаем подход, в котором временные требования задаются с использованием шаблонов требований, которые строятся из базовых шаблонов. Для каждого шаблона требований определяются соответствующий шаблон дополнительных инвариантов и леммы. Предлагаемый подход позволяет сделать дедуктивную верификацию процесс-ориентированных программ более автоматизированной.
В этой статье мы формально описываем системы реального времени с абстрактным планировщиком, используя модели Крипке. Эта формализация позволяет специализировать абстрактный планировщик в терминах построенной модели. Мы иллюстрируем этот подход с помощью системы реального времени, в которой работы являются невытесняемыми и имеют фиксированный приоритет (NE-GFP). Мы также формулируем свойство безопасности для систем реального времени, используя линейную временную логику LTL. Мы реализуем нашу формализацию систем реального времени с планировщиком NE-GFP на языке Promela, используемом в инструменте проверки SPIN, и проводим эксперименты для доказательства/опровержения свойства безопасности, чтобы оценить эффективность нашего подхода.
Вероятности достижимости и ожидаемые вознаграждения - это два важных класса свойств, которые используются при проверке вероятностной модели. Для вычисления базовых свойств применяются итерационные численные методы. Чтобы гарантировать достоверность результатов вычислений, используется метод интервальных итераций. Этот метод использует два вектора в качестве верхней и нижней границ значений и использует стандартный метод итерации значений для обновления значений этих векторов. В этой статье мы используем комбинацию итерации значений и итерации политики для обновления этих значений. Мы используем итерацию политики для обновления значений вектора с нижней границей. Для вектора с верхней границей мы используем модифицированную версию итерации значений, которая помечает бесполезные действия, чтобы игнорировать их в оставшейся части вычислений. Предлагаемый нами подход дает возможность применить некоторые передовые методы для сокращения времени выполнения вычислений для метода интервальных итераций. Мы рассматриваем набор стандартных примеров, и экспериментальные результаты показывают, что в большинстве случаев предлагаемый нами метод сокращает время выполнения вычислений.