Композиційні методи специфікації та верифікації програмних систем - Автореферат

Редьком та розвивається, зокрема, фахівцями кафедри теорії та технології програмування факультету кібернетики Київського національного університету імені Тараса Шевченка. В КП досліджують системи на різних рівнях абстракції, які виникають на шляху експлікації програмування - абстрактному, булевому та номінативному рівнях. Окрім специфікації іншим важливим етапом розробки ПЗ, який історично одним з перших був підданий формалізації, є верифікація (саме формальна верифікація на противагу інженерним методам тестування). Це зумовлює актуальність теми дисертаційної роботи, яка присвячена проблемам побудови адекватних моделей програмних систем, зокрема серверних середовищ, з метою доведення коректності відповідного ПЗ шляхом специфікації та верифікації. Дисертаційна робота виконувалася в рамках комплексної наукової програми Київського національного університету імені Тараса Шевченка «Інформатизація суспільства» (тема «Логіко-математичні та програмологічні засоби інформаційних технологій», 2001-2005, номер держреєстрації - 0101U002163) та теми «Еталонування семантичних структур мов CASE-середовищ програмологічними засобами», (2001-2005, номер держреєстрації - 0101U005770, замовник - Фонд фундаментальних досліджень Міністерства освіти і науки України).У другому розділі «Композиційно-номінативні методи специфікації»: введено визначення і обґрунтовано природність та адекватність композиційного підходу до специфікації програмних систем, розглянуто композиційні системи різних рівнів абстракції та введено новий комплексно-номінативний рівень і побудовано мову цього рівня ACON, побудовано моделі структур даних програмування та функцій над ними в композиційній системі комплексно-номінативного рівня, обґрунтовано тезу репрезентативної повноти даних комплексно-номінативного рівня та проведено аналіз належності структур даних програмування та функцій над ними до відповідних рівнів абстракції. Необхідність у новому рівні абстракції (конкретнішому) полягає в недостатній виразності мов інших (більш абстрактних) типів, зокрема в потребі розгляду даних на більш збагаченому рівні, коли маємо ситуацію VЗD№Ж, тобто імена можуть бути настільки ж складноструктуровані, як і їх значення (тобто як самі дані). На комплексно-номінативному рівні вводяться дві нові функції - утворення іменної пари та взяття множини імен номінативного даного, а саме: a: V2®D - функція від двох аргументів, яка визначається наступним чином: name a value (d) = [(NAMEЮ) (d) ? (VALUEЮ) (d)] та getnames: D®V-set, тобто IMG_5743dd9a-065a-4ac7-8c05-ad8ffe723b51 . На підставі аналізу структур даних побудовано моделі та зроблено класифікацію різних структур даних, що дозволило обґрунтувати тезу репрезентативної повноти номінативних даних: структури даних мов програмування можуть розглядатися як конкретизації номінативних даних. В результаті моделювання та аналізу структур даних мови RSL (точніше, наявних конструкторів типів) в термінах ACON визначено необхідний набір функцій та композицій для подання різних типів (конструкторів) та функцій над ними (табл.Головний результат дисертаційної роботи - розробка композиційних моделей, мов специфікації та методів верифікації програмних систем, що розвязують практично важливі задачі специфікації систем зі структурованими даними та доведення часткової коректності серверного програмного забезпечення і мають суттєве значення для підвищення якості та надійності програмних систем. В результаті проведеної роботи: побудовано та досліджено нову композиційну мову специфікацій комплексно-номінативного рівня, що дає можливість адекватно моделювати структури даних традиційних мов програмування та функції над ними на основі номінативних даних; проведено аналіз та розподіл структур даних традиційних мов специфікацій та програмування і функцій над ними по рівнях абстракції, побудовано композиційно-номінативну модель структурованих даних та показано її репрезентативну повноту;

Основний зміст роботи

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

проведено аналіз та розподіл структур даних традиційних мов специфікацій та програмування і функцій над ними по рівнях абстракції, побудовано композиційно-номінативну модель структурованих даних та показано її репрезентативну повноту;

на підставі уточнення механізму взаємодії через спільну память запропоновано нову композиційно-номінативну модель багатоекземплярних програм та теоретично обґрунтовано адекватність серверному середовищу класичних клієнт-серверних систем і прагматичну повноту цієї моделі;

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

для побудованої моделі доведено рівнопотужність двох сформульованих варіантів часткової коректності програм в цих мовах;

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

запропонований метод апробовано на реальних системах для верифікації (зокрема, для доведення критичних властивостей системи виплати міжнародних грошових переказів Vigo Remittance Corp.).

1. Панченко Т.В. Використання формальних специфікацій для розробки програмних систем // Вісник Київського університету. Серія: фіз.-мат. науки. - 2002. - вип. 2. - С. 245-256.

2. Панченко Т.В. Моделювання структур даних та функцій над ними в композиційно-номінативній мові ACON // Проблемы программирования. - 2004. - №1-2. - С. 7-15.

3. Нікітченко М.С., Панченко Т.В. Структури даних в композиційних мовах програмування // Вісник Київського університету. Серія: фіз.-мат. науки. - 2004. - вип. 2. - С. 316-325.

4. Панченко Т.В. Використання формальних специфікацій для розробки Електронної біржі Ощадного банку // Проблемы программирования. - 2002. - №1-2. - С. 161-167.

5. Панченко Т.В. Пропозиційне числення для послідовної тризначної логіки (системи типу МАККАРТІ) // Вісник Київського університету. Серія: фіз.-мат. науки. - 2000. - вип. 4. - С. 284-292.

6. Панченко Т.В. Типізація в композиційно-номінативних мовах // Матеріали Міжнародної науково-практичної конференції студентів, аспірантів та молодих вчених «Шевченківська весна. Сучасний стан науки, досягнення, проблеми та перспективи розвитку». Збірник тез. - 2003. - С. 66-68.

7. 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.

8. Панченко Т.В. Методологія доведення властивостей програм в композиційних мовах IPCL // Тези доповідей Міжнародної конференції «Теоретичні та прикладні аспекти побудови програмних систем» (TAAPSD’2004). Київ. - 2004. - С. 62-67.

Размещено на .ru