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

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

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

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

Обгрунтовано можливість активізації пізнавальної діяльності студентів у процесі вивчення числових методів із застосуванням об'єктно-орієнтованих бібліотек математичних, алгоритмічних і проблемних класів. Розроблено методику вивчення курсу "Числові методи" на фізико-математичних факультетах педагогічних і програмуючих спеціальностях технічних вузів.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Дисертація присвячена питанням проектування розподілених програмних систем із застосуванням принципів об'єктно-орієнтованої парадигми. В дисертації розроблено новий метод проектування об'єктно-орієнтованих програмних систем на основі використання формалізованої візуальної мови контурних Р-схем. Обгрунтовано представлення декларативної семантики контурних Р-схем за допомогою графової алгебри процесів. Розроблена аксіоматична семантика Р-схем на базі програмної логіки Хоара. Запропоновані графові алгебри опису типів даних та обгрунтовані методи їх використання для специфікації класів об'єктно-орієнтованих програмних систем. Основні результати праці використані при створенні розподіленої системи керування національною комп'ютерною мережею України, проект INCO-COPERNICUS 96-0114 Європейського Союзу.

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

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

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

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

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

Розглянуто питання розробки нових моделей та елементів структурно-об'єктної технології (СОТ) та інтерфейсного комплексу (ІК) корпоративно інформаційної системи (КІС) з урахуванням недоліків існуючих варіантів реалізації структурних і об'єктних моделей і технологій. Розроблено математичні метамоделі СОТ розробки ІК КІС, які описують процеси, стани та динаміку поведінки СОТ під час виконання проектних робіт. Створено математичні моделі операцій агентів управління розробкою та тестування локальних проектних рішень ІК КІС. Основні результати наукового дослідження програмно апробовано та рекомендовано для автоматизації процесів розробки КІС різного призначення.

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

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

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

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

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

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

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

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

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