Шаблон:Current Seminars — различия между версиями

Доклад по статье H. Barringer, A. Goldberg, K. Havelund, K. Sen "Rule-Based Runtime Verification"

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

Доклад по статье K.C. Shashidhar, Maurice Bruynooghe, Francky Catthoor, Gerda Janssens "Verification of Source Code Transformations by Program Equivalence Checking"

Как правило, когда алгоритмы для обработки цифровых сигналов адаптируются для работы в энергоэффективных и эффективно функционирующих встроенных системах, применяется комбинация ручных и автоматических преобразований. Это порождает сложную задачу верификации. Задача верификации упрощается при конвертирования кода в DSA-форму (dynamic single assignment form). Данная статья описывает метод доказательства эквивалентности двух программ в DSA-форме, в которых индексация элементов массивов и условия завершения циклов являются (кусочно заданными) аффинными выражениями. Для таких программ может быть использовано геометрическое моделирование и сразу для наборов элементов может быть показано, что результат вычислений обеих программ представляет собой одну и ту же функцию от входных данных.

Доклад по статье Aleksandr Tvardovskii, Nina Yevtushenko "On minimization of Timed Finite State Machines"

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