Індекс рубрикатора НБУВ: В192.162.1

Рубрики:

Наближене розв'язання звичайних диференціальних рівнянь

Шифр НБУВ: Ж15477 Пошук видання у каталогах НБУВ 

На базе системы алгебраического программирования APS предложена технология создания математической информационной среды (МИС) для решения обыкновенных дифференциальных уравнений (ОДУ), далее - Среда. Рассмотрен элемент Среды - комплекс процедур для аналитического решения некоторых классических типов ОДУ. Построенные в работе процедуры представляют собой алгебраические спецификации, записанные в виде близком к традиционному в математике.

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

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

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

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

A guided search method for automatic test scenario building during verification proposed. The method uses user-defined regular expressions as test purposes and for model behavior traversal bounding. Search managing strategies together with trace and state equivalence weakening described.

Описано метод побудови абстракцій для підвищення ефективності перевірки формальних моделей. Послаблення відношення еквівалентності станів досягнуто за рахунок ігнорування незначущих значень атрибутів. Результати експериментів продемонстрували на деяких прикладах зменшення складності виконання перевірки властивостей моделі з експоненційної до поліноміальної.

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

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

Приведен обзор автоматических методов проверки правильности формальных моделей программных систем. Рассмотрены проверяемые свойства, методы редукции и современные инструментальные средства проверки моделей.

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

Цель работы - разработка комплекса инструментальных средств для автоматизации анализа и упрощения понимания поведения кода программных систем. Предложены методы трансляции, абстракции, отладки и построения тестов для языка Кобол. Разработана экспериментальная система, реализующая предложенные методы.