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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

На базі мови TL розвинуто формальну мову подання математичних текстів ForTheL, що є близькою за синтаксисом до природної англійської мови і може бути перекладена в мову першого порядку. Сформульовано поняття коректності тексту у мові ForTheL. Запропоновано оригінальне поняття істинності твердження у деякій позиції всередині формули першого порядку та досліджено його властивості. Доведено, що за умов еквівалентності двох формул, що є локально істинною у заданій позиції, ці дві формули є взаємозамінюваними у цій позиції. Відзначено, що поняття локальної істинності дозволяє обгрунтувати коректність різноманітних перетворень складних формул, а саме: розкриття визначень або додання допоміжних тверджень всередині формули. Запропоновано процедуру породження "відомостей" про окремі входження термів у досліджуваний ForTheL-текст; ці відомості є літерами, локально істинними у відповідному входженні, зокрема, вони несуть інформацію про тип терму. На базі цього апарату сформульовано декілька високорівневих схем доведення, які становлять "інструментарій" міркувальника. Проведено дослідження цілекерованих процедур пошуку виведення, що використовуються у програмі "Алгоритм Очевидності". Запропоновано нове доведення коректності поняття допустимої підстановки. Викладено цілекероване табличне числення, що оперує несколемізованими формулами. Доведено, що виведення у цьому численні можуть бути перетворені у виведення у класичному табличному диз'юнктному численні Model Elimination. Доведено можливість зворотнього перетворення. Запропоновано нове табличне цілекероване числення з лінивою парамодуляцією для класичної логіки першого порядку з рівністю, доведено його повноту.

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

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

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