Панченко Тарас Володимирович. Композиційні методи специфікації та верифікації програмних систем : дис... канд. фіз.-мат. наук: 01.05.03 / Київський національний ун-т ім. Тараса Шевченка. - К., 2006.
Анотація до роботи:
Панченко Т.В. Композиційні методи специфікації та верифікації програмних систем. – Рукопис.
Дисертація на здобуття наукового ступеня кандидата фізико-математичних наук за спеціальністю 01.05.03 – математичне та програмне забезпечення обчислювальних машин і систем. – Київський національний університет імені Тараса Шевченка. – Київ, 2006.
У дисертаційній роботі досліджено проблеми специфікації та верифікації прагматично важливих класів програмних систем методами композиційного програмування. Розроблено композиційні моделі та мови для специфікації програмних систем зі структурованими даними, виконано комплексний аналіз та розподіл структур даних і функцій над ними по рівнях абстракції. Доведено репрезентативну повноту номінативних даних комплексно-номінативного рівня. Розроблено композиційні методи для верифікації систем спеціального класу – моделі багатоекземплярного виконання програм у серверному середовищі з паралелізмом в режимі почергового виконання з переключенням із взаємодією через спільну пам’ять. Сформульовано два варіанти часткової коректності програм на введених композиційних мовах та запропоновано методологію верифікації, що включає метод з лінійною складністю замість експоненційної.
Головний результат дисертаційної роботи – розробка композиційних моделей, мов специфікації та методів верифікації програмних систем, що розв’язують практично важливі задачі специфікації систем зі структурованими даними та доведення часткової коректності серверного програмного забезпечення і мають суттєве значення для підвищення якості та надійності програмних систем. В результаті проведеної роботи:
побудовано та досліджено нову композиційну мову специфікацій комплексно-номінативного рівня, що дає можливість адекватно моделювати структури даних традиційних мов програмування та функції над ними на основі номінативних даних;
проведено аналіз та розподіл структур даних традиційних мов специфікацій та програмування і функцій над ними по рівнях абстракції, побудовано композиційно-номінативну модель структурованих даних та показано її репрезентативну повноту;
на підставі уточнення механізму взаємодії через спільну пам’ять запропоновано нову композиційно-номінативну модель багатоекземплярних програм та теоретично обґрунтовано адекватність серверному середовищу класичних клієнт-серверних систем і прагматичну повноту цієї моделі;
побудовано та досліджено клас композиційно-номінативних мов з композицією паралельного виконання в режимі чергування для адекватної реалізації алгоритмів, які виконуються у серверному середовищі;
для побудованої моделі доведено рівнопотужність двох сформульованих варіантів часткової коректності програм в цих мовах;
для підкласу паралельних програм розроблено метод верифікації часткової коректності, який має лінійну складність замість експоненційної. Запропоновано методологію верифікації властивостей у класі серверних програм на введених композиційних мовах;
запропонований метод апробовано на реальних системах для верифікації (зокрема, для доведення критичних властивостей системи виплати міжнародних грошових переказів Vigo Remittance Corp.).
Публікації автора:
Панченко Т. В. Використання формальних специфікацій для розробки програмних систем //Вісник Київського університету. Серія: фіз.-мат. науки. – 2002. – вип. 2. – С. 245–256.
Панченко Т. В. Моделювання структур даних та функцій над ними в композиційно-номінативній мові ACoN //Проблемы программирования. – 2004. – №1-2. – С. 7–15.
Нікітченко М. С., Панченко Т. В. Структури даних в композиційних мовах програмування //Вісник Київського університету. Серія: фіз.-мат. науки. – 2004. – вип. 2. – С. 316–325.
Панченко Т. В. Використання формальних специфікацій для розробки Електронної біржі Ощадного банку //Проблемы программирования. – 2002. – №1-2. – С. 161–167.
Панченко Т. В. Пропозиційне числення для послідовної тризначної логіки (системи типу МакКарті) //Вісник Київського університету. Серія: фіз.-мат. науки. – 2000. – вип. 4. – С. 284–292.
Панченко Т. В. Типізація в композиційно-номінативних мовах //Матеріали Міжнародної науково-практичної конференції студентів, аспірантів та молодих вчених “Шевченківська весна. Сучасний стан науки, досягнення, проблеми та перспективи розвитку”. Збірник тез. – 2003. – С. 66–68.
Panchenko T. V. Composition Approach to Software Systems Modeling and its Support Tools //International Conference on Dynamical System Modeling and Stability Investigation. Thesis of Conference Reports, May 27-30, 2003. – P. 421.
Панченко Т. В. Методологія доведення властивостей програм в композиційних мовах IPCL //Тези доповідей Міжнародної конференції “Теоретичні та прикладні аспекти побудови програмних систем” (TAAPSD’2004). Київ. – 2004. – С. 62–67.
