Розглянуто питання створення адаптивної інформаційної технології для підвищення достовірності й ефективності діагностування комп'ютерних систем на наявність троянських програм. У ході дослідження виявлено недоліки роботи інформаційних технологій і засобів діагностування комп'ютерних систем на наявність троянських програм. Запропоновано поведінкову модель троянських програм, яка формалізує особливості функціонування цих програм у комп'ютерних системах, та модель процесу діагностування комп'ютерних систем на наявність троянських програм, яка дозволяє здійснювати діагностування з високою достовірністю. Розроблено метод побудови захищених послідовностей і генерації детекторів на базі штучних імунних систем, що дозволяє визначити факт заміни файлів троянськими версіями у процесі діагностування комп'ютерних систем у режимі сканера.

  Скачати повний текст

Розроблено методи для статичної перевірки певних властивостей формальних моделей, а саме: несуперечливості, повноти та цілісності. Розглянуто проблему досяжності заданих станів системи та запропоновано статичні методи для її розв'язання. Побудовано алгоритм фільтрації станів на підставі статичного аналізу моделі та метод побудови абстрактних поведінок моделі для спрямованого пошуку. Розглянуто задачу здійснення переходу системи від одного класу символьних станів до наступного під дією заданого базового протоколу. Така трансформація виконується за допомогою предикатних перетворювачів. Побудовано алгоритми прямого та зворотного предикатних перетворювачів для числових і символьних типів даних, функціональних типів, масивів та списочних типів даних. Розроблено алгоритми трансляції певних підмножин MSC, SDL і UML в мову базових протоколів з метою подальшої автоматичної верифікації. Підмножини цих мов було виділено з урахуванням практичної необхідності у застосованих індустріальних проектах. Запропоновано деякі розширення обраних мов для застосування методів верифікації повною мірою.

  Скачати повний текст

Уперше побудовано алгортим перекладу опису проектованої системи мовою MSC2000 у мережі Петрі та доведено його коректність за допомогою алгебри процесів, а саме - бісмуляційну еквівалентність вхідних MSC діаграм і синтезованої за цими діаграмами мережі Петрі. За цього визначено формальну семантику базового елемента мови MSC2000-<умова>(condition). Розроблено й обгрунтовано оригінальні алгоритми аналізу та верифікації формальної моделі у вигляді мережі Петрі, що використовують метод TSS розв'язання систем лінійних однорідних і неоднорідних діафантових рівнянь над множиною натуральних чисел, а саме: алгоритм верифікації певних властивостей мереж Петрі, зокрема, (структурної обмеженості), L3-живості, досяжності, наявності дедлоків; алгортим побудови S- і T-варіантів мережі Петрі; алгоритм пошуку пасток і тупиків асиметричної мережі Петрі. Рекомендовано здійснювати аналіз зменшеної складності її динамічних властивостей, який має проводитися за допомогою розв'язання рівняння стану. Уперше запропоновано визначення інваріантності властивостей базової моделі як мережі Петрі, яке використовується для створення оригінальної методики пошуку конфліктів функціональностей проектованої системи.

  Скачати повний текст

Розглянуто методи роботи з вимогами, що складають технологію, яка є складовою частиною процесу створення програмних систем з великою кількістю станів. Висвітлено п'ять складових частин цієї технології: формалізацію вимог у вигляді базових протоколів, пошук суперечливостей та неповноти, генерацію тестових наборів з множини вимог, синтез та аналіз динамічних властивостей моделі. Вимоги до інтерактивних систем представлено у вигляді формальних специфікацій - базових протоколів. Визначено клас базових протоколів, для якого задачі технології вирішуються без експонентного вибуху. За допомогою формалізму побудовано алгоритми верифікації базових протоколів з використанням машини доведення, а також синтез моделі за базовими протоколами. На основі методів символьного моделювання розглянуто різні критерії генерації тестів та їх застосування до генерації тестів за специфікаціями, записаними сучасними інженерними мовами - MSC, SDL, UML.

  Скачати повний текст

Досліджено проблеми специфікації та верифікації прагматично важливих класів програмних систем за методами композиційного програмування. Розроблено композиційні моделі та мови для специфікації програмних систем зі структурованими даними. Проведено комплексний аналіз і розподіл структур даних і функцій над ними за рівнями абстракцій. Доведено репрезентативну повноту номінативних даних комплексно-номінативного рівня. Запропоновано композиційні методи для верифікації систем спеціального класу - моделі багатоекземплярного виконання програм у серверному середовищі з паралелізмом у режимі почергового виконання з переключенням зі взаємодією завдяки затосуванню спільної пам'яті. Сформульовано два варіанти часткової коректності програм на введених композиційних мовах та запропоновано методологію верифікацій, що використовує метод з лінійною складністю замість експоненційної.

  Скачати повний текст

Розроблено математичну модель визначення оптимального часу тестування модулів програмних систем (ПС) з урахуванням ризиків відмов під час експлуатації ПС та метод оцінювання ризику відмов їх модулів. Відзначено, що стратегія тестування полягає у визначенні модулів, які потребують більш тривалого тестування. Згідно даній стратегії час тестування кожного модуля повинен виділятися таким чином, щоб вартість (трудомісткість) тестування відповідала величині ризику використання модуля під час роботи ПС. Запропонована стратегія тестування є основою побудованого базового процесу тестування ПС обробки даних, який впорядковує задачі тестування, виконувані на різних стадіях розробки ПС. Зауважено, що запропоновані процес, модель і метод реалізовані у програмному комплексі підтримки інженерії тестування. Наведено результати оцінювання стану процесу тестування організації-розробника ПС та впровадження базового процесу тестування.

  Скачати повний текст

Розв'язано актуальну науково-технічну задачу підвищення достовірності процесу тестування програмного забезпечення (ПЗ) на основі використання апарату штучних нейронних мереж. Проаналізовано розвиток концептуальної моделі підвищення достовірності тестування ПЗ за допомогою виявлення прихованих помилок різних типів під час повторного тестування ПЗ. Описано категорійну модель процесу повторного тестування ПЗ на базі штучних нейронних мереж (ШНМ), яка враховує вплив прихованих помилок попередньої категорії на помилки наступної. Розроблено метод ідентифікації прихованих помилок ПЗ на основі ШНМ, у якому вхідна інформація про результати основного тестування опрацьовується за допомогою ШНМ. Удосконалено метод оцінки достовірності прихованих помилок ПЗ, що враховує кількість виявлених прихованих помилок різних типів категорійності та визначає приріст достовірності процесу тестування у порівнянні з неврахуванням кількості виявлених помилок.

  Скачати повний текст

Створено алгоритми та методи для автоматичної верифікації формальних моделей великих промислових систем. Одержано метод оперативної побудови точних абстракцій станів формальної моделі для перевірки темпоральних властивостей. Головною відмінністю є те, що кожний абстрактний стан формується з підмножини атрибутів та їх реальних значень відповідного конкретного стану, якої достатньо для перевірки властивостей моделі. Абстрактні стани не відрізняють варіювання значень незначущих атрибутів, що дозволяє значно зменшити кількість станів, необхідних для перевірки властивостей моделі. Розвинуто методи спрямованого пошуку поведінки моделі. Як засоби спрямовування використано спеціальні регулярні вирази над алфавітом імен переходів моделі, тим самим задання цілей тестування вдосконалено. Метод дозволяє автоматизувати побудову тестових сценаріїв і аналіз поведінок формальних моделей.

  Скачати повний текст