Побудова формальних специфікацій за неформальними вимогами генерація набору тестів, синтез архітектурної моделі і перевірка властивостей. Прототипи програм верифікації формальних специфікацій і символьної генерації в системі інсерційного програмування.
При низкой оригинальности работы "Верифікація та тестування інтерактивних систем, специфікованих за допомогою базових протоколів", Вы можете повысить уникальность этой работы до 80-100%
Національна академія наук України Інститут кібернетики імені В.М. Глушкова Автореферат дисертації на здобуття наукового ступеня кандидата фізико-математичних наук 01.05.03 - математичне та програмне забезпечення обчислювальних машин і систем Верифікація та тестування інтерактивних систем, специфікованих за допомогою базових протоколів Летичевський Олександр Олександрович Київ - 2005 Дисертацією є рукопис. Робота виконана в Інституті кібернетики ім. В.М. Глушкова НАН України. Дисертація присвячена побудові методів роботи з вимогами, що складають технологію, яка є складовою частиною процесу створення програмних систем з великою кількістю станів. Розглянуто п’ять складових частин цієї технології: формалізація вимог у вигляді базових протоколів; пошук суперечливостей та неповноти; генерація тестових наборів з множини вимог; синтез та аналіз динамічних властивостей моделі. Ключові слова: атрибутні транзиційні системи, агенти та середовища, алгебра процесів, вимоги до програмного забезпечення, базові протоколи, верифікація, символьне моделювання, суперечливість та неповнота специфікацій, автоматичне доведення теорем, генерація тестів. С помощью разработанного в работе формализма строятся алгоритмы верификации базовых протоколов с использованием доказательной машины, а также синтез модели по базовым протоколам. Созданные автором прототипы программ, реализующих рассмотренные методы, являются основой системы верификации требований, разработанной и внедренной для работы с требованиями в промышленных телекоммуникационных моделях в кампании Motorola, а также в кампании “Информационные программные системы”. Інтегрована система для обробки SDL-специфікацій була реалізована на базі доказової машини ACL2.
Вы можете ЗАГРУЗИТЬ и ПОВЫСИТЬ уникальность своей работы
