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

Размещено на http://www.allbest.ru/

Размещено на http://www.allbest.ru/

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

Автореферат

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

Загальна характеристика роботи

Актуальність теми. Інформаційні технології сьогодні розвиваються високими темпами, але якість програмного забезпечення (ПЗ) не завжди задовольняє потребам. Про складний стан справ говорять і самі спеціалісти в галузі комп'ютерних технологій (Е. Дейкстра, Г. Буч). Таким чином, гарантування коректності ПЗ є важливою проблемою.

Методи тестування ПЗ мають очевидні обмеження, отже, існує потреба у строгих, базованих на математиці, формальних методах специфікації та верифікації програмних систем. Формальні методи сьогодні розвинені до достатнього для промислового використання рівня. З іншого боку, у замовників та суспільства зростають вимоги щодо їх застосування. Інколи такі вимоги зафіксовані у стандартах на розробку ПЗ, наприклад, в Європейському стандарті для програмної інженерії, вимогах IEEE чи Європейської космічної агенції.

Одним з формальних підходів до специфікації та верифікації ПЗ є композиційне програмування (КП), яке започатковане В.Н. Редьком та розвивається, зокрема, фахівцями кафедри теорії та технології програмування факультету кібернетики Київського національного університету імені Тараса Шевченка. КП є розвитком структурологічного підходу Г. Фреге, який був перенесений на програмування А.А. Ляпуновим та розвинений Ю. І. Яновим, А.П. Єршовим, Л.А. Калужніним, В.М. Глушковим та іншими. В КП досліджують системи на різних рівнях абстракції, які виникають на шляху експлікації програмування - абстрактному, булевому та номінативному рівнях. Системи останнього рівня, композиційно-номінативні (КНС), є досить багатими для адекватного відображення понять програмування.

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

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

Особливо складно верифікувати програми, що працюють у середовищі з паралелізмом. В роботах вітчизняних та іноземних авторів П. І. Андона, А.В. Анісімова, А.Ю. Дорошенка, Ю.В. Капітонової, С.Л. Кривого, К.М. Лаврищевої, О.А. Летичевського, А.Н. Чеботарьова, Ешкрофта (E. Ashcroft), Овіцкі (S. Owicki) - Гріса (D. Gries), Пнуелі (A. Pnueli) та Лампорта (L. Lamport), Джонса (C. Jones), Ченді (K. Chandy) й Місри (J. Misra), Кларка (E. Clarke) та інших, отримано важливі результати в дослідженні реактивних та розподілених паралельних середовищ із взаємодією переважно шляхом передачі повідомлень. Але системи з паралелізмом із міжпрограмною взаємодією шляхом доступу до спільної пам'яті в режимі почергового виконання - фактично, серверні середовища клієнт-серверних систем в загальному випадку - досі недостатньо досліджені. Це зумовлює актуальність теми дисертаційної роботи, яка присвячена проблемам побудови адекватних моделей програмних систем, зокрема серверних середовищ, з метою доведення коректності відповідного ПЗ шляхом специфікації та верифікації. Використання композиційно-номінативних методів для розв'язку цих проблем дозволяє збагатити засоби специфікації та розширити можливості верифікації на досліджені в роботі класи задач.

Зв'язок роботи з науковими програмами, планами, темами. Дисертаційна робота виконувалася в рамках комплексної наукової програми Київського національного університету імені Тараса Шевченка «Інформатизація суспільства» (тема «Логіко-математичні та програмологічні засоби інформаційних технологій», 2001-2005, номер держреєстрації - 0101U002163) та теми «Еталонування семантичних структур мов CASE-середовищ програмологічними засобами», (2001-2005, номер держреєстрації - 0101U005770, замовник - Фонд фундаментальних досліджень Міністерства освіти і науки України). Тематика дисертації пов'язана з науково-дослідною роботою школи програмології на кафедрі теорії та технології програмування Київського національного університету імені Тараса Шевченка, яка присвячена дослідженням та розвитку композиційних методів програмування.

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

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

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

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

дослідити клас клієнт-серверних систем та розробити метод доведення часткової коректності серверного ПЗ.

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

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

Наукова новизна одержаних результатів полягає в тому, що:

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

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

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

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

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

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

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

Основні результати проведеного дослідження використано в ВАТ «Державний ощадний банк України» для специфікації та розробки системи «Електронна біржа» (Довідка про впровадження №7/1-33/1397 від 12.03.2003 р.) та специфікації і доведення критичних властивостей системи виплати міжнародних грошових переказів Vigo Remittance Corp. (Довідка про впровадження №787 від 22.10.2004 р.), а також у підготовці та читанні курсу «Теорія програмування» в Київському національному університеті імені Тараса Шевченка.

Особистий внесок здобувача. Всі основні результати дисертації одержані автором самостійно. У спільно виконаній з науковим керівником роботі М.С. Нікітченку належить постановка задачі та участь в обговоренні результатів.

Апробація теоретичних результатів дисертації. Результати проведених досліджень обговорювались на конференціях і семінарах факультету кібернетики Київського національного університету імені Тараса Шевченка, Інституту кібернетики НАН України, Інституту програмних систем НАН України, Варшавського університету. Основні положення та висновки дисертаційного дослідження неодноразово доповідались на міжнародних наукових і науково-практичних конференціях:

Третя Міжнародна науково-практична конференція з програмування «УкрПРОГ'2002» (Україна, Київ, 21-24 травня 2002 р.),

Міжнародна конференція «Моделювання та дослідження стійкості динамічних систем» (Україна, Київ, 27-30 травня 2003 р.),

Міжнародна науково-практична конференція «Шевченківська весна. Сучасний стан науки: досягнення, проблеми і перспективи розвитку» (Україна, Київ, 14-15 травня 2003 р.),

Четверта Міжнародна науково-практична конференція з програмування «УкрПРОГ'2004» (Україна, Київ, 1-3 червня 2004 р.),

Міжнародна конференція «Теоретичні та прикладні аспекти побудови програмних систем TAAPSD'2004» (Україна, Київ, 5-8 жовтня 2004 р.).

Розроблений метод верифікації програмних систем був відзначений на IV конкурсі науково-технічних проектів молодих вчених, організованому КМДА та НАН України в 2004 р.

Публікації. За темою дисертації опубліковано 8 наукових праць, 5 - статті у фахових виданнях наукових праць, які затверджені ВАК України, 3 - публікації в збірках матеріалів науково-практичних конференцій.

Структура та обсяг роботи. Дисертаційна робота складається із вступу, трьох розділів, висновків, списку використаних джерел (182 найменування) та додатків (А, Б). Загальний обсяг дисертації становить 177 сторінок, основний текст роботи викладено на 140 сторінках.

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

серверний автоматизація програма композиційний

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

Перший розділ «Формальні методи розробки програмних систем» фіксує проблематику, яка досліджується в дисертації. В ньому:

обґрунтовано актуальність проблеми коректності ПЗ та визначено шляхи її розв'язку,

визначено і досліджено базові поняття, на які спирається подальша робота,

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

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

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

У другому розділі «Композиційно-номінативні методи специфікації»:

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

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

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

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

Наведено основні принципи композиційного програмування: розвитку (від абстрактного до конкретного), гносеологічності, підпорядкування та відокремлення, функціональності та композиційності, інтенсіональності. Розглянуто базис побудови композиційних програмних систем: системи даних, функції та композиції. Визначено різні рівні композиційних систем: абстрактний, булевий, номінативний (з однозначним та багатозначним іменуванням), метаномінативний та введено нові системи комплексно-номінативного рівня. В композиційних системах номінативного рівня множину даних D визначають рекурсивно: , де означає клас іменних множин з іменами із V та значеннями з D (W - множина базових значень). Необхідність у новому рівні абстракції (конкретнішому) полягає в недостатній виразності мов інших (більш абстрактних) типів, зокрема в потребі розгляду даних на більш збагаченому рівні, коли маємо ситуацію VD, тобто імена можуть бути настільки ж складноструктуровані, як і їх значення (тобто як самі дані). На комплексно-номінативному рівні вводяться дві нові функції - утворення іменної пари та взяття множини імен номінативного даного, а саме: a: V²D - функція від двох аргументів, яка визначається наступним чином: name a value (d) = [(name) (d) ? (value) (d)] та getnames: DV-set, тобто .

Функція рівності над даними визначена індуктивно.

Усі базові композиції номінативного та метаномінативного рівнів, а також дві нові та функція рівності складають сигнатуру композиційної мови ACoN (Advanced Composition Nominative Language) комплексно-номінативного рівня.

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

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

Аналіз структур даних програмування і функцій над ними, їх належності до відповідних рівнів абстракції та обґрунтування тези проведено на прикладі мови RSL (RAISE Specification Language), оскільки

RAISE (Rigorous Approach to Industrial Software Engineering) має широкий спектр можливостей для розробки специфікацій і ввібрав у себе кращі напрацювання інших формальних методів;

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

мова RSL є досить близькою за синтаксисом до звичайних мов програмування (таких як C, PASCAL та інші);

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

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

В результаті моделювання та аналізу структур даних мови RSL (точніше, наявних конструкторів типів) в термінах ACoN визначено необхідний набір функцій та композицій для подання різних типів (конструкторів) та функцій над ними (табл. 2.1).

Розподіл структур даних і функцій над ними за рівнями абстракції

На підставі побудованих подань типів даних мови RSL сформульовано наступне твердження:

Теорема 2.1. Всі типи даних мови RSL та операції над ними моделюються засобами композиційної мови ACoN комплексно-номінативного рівня.

Доведення проведено шляхом моделювання структур даних мови RSL в композиційній мові ACoN.

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

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

виділено прагматично важливий клас паралельних програм серверного середовища для класичних клієнт-серверних систем,

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

розроблено метод верифікації властивостей програм вказаного класу.

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

Запропоновано клас композиційних мов IPCL (Interleaving Parallel Composition Languages) з традиційним синтаксисом P:= | P₁; P₂ | if b then P₁ else P₂ | while b do P | P₁ || P₂ - клас композиційних мов з паралелізмом в режимі чергування. Цей клас мов є спеціалізацією композиційно-номінативної мови з попереднього розділу. Вона спрощена за структурами даних, акцент зроблено на композиціях, зокрема, паралелізму. Мови класу IPCL ґрунтуються на композиційно-номінативних системах з множиною номінативних даних D=ND (V, W)=, F - набором функцій для перетворення даних та C - композиціями над функціями з F. F=OperPred, де Oper=DD  DD, а Pred=DD  {True, False}, де перше входження D в декартів добуток - «глобальні дані», а друге - «локальні» для поточного процесу. Функції, що повертають значення з множини {True, False} (предикати), не змінюють поточний стан даних DD - вони використовуються в якості умови в операторах (композиціях) розгалуження та циклування. Композиціями є послідовне виконання - «;» (аналог звичайної композиції множення або аплікування, послідовної функціональної композиції) з абстрактним трактуванням «», розгалуження - «if» (аналог композиції «»), циклування - «while» (аналог композиції «»), присвоювання - «:=» (аналог певної комбінації композицій іменування та розіменування) та паралельне виконання в режимі чергування - «||». Семантика всіх композицій є традиційною, семантика останньої є така:

|| - асоціативна і комутативна:

sem _{(A || B) || C} (d) = sem _{A || (B || C)} (d)

sem _{A || B} (d) = sem _{B || A} (d)

|| відносно «if»:

sem _{if b then P else Q || R} (d) = sem _{P || R} (d), якщо b (d) = True,

sem _{if b then P else Q || R} (d) = sem _{Q || R} (d), якщо b (d) = False,

sem _{if b then P else Q; P}' _{|| R} (d) = sem _{P; P}' _{|| R} (d), якщо b (d) = True,

sem _{if b then P else Q; P}' _{|| R} (d) = sem _{Q; P}' _{|| R} (d), якщо b (d) = False,

|| відносно «while»:

sem _{while b do P || R} (d) = sem _{P; while b do P || R} (d), якщо b (d) = True,

sem _{while b do P || R} (d) = sem _R (d), якщо b (d) = False,

sem _{while b do P; P}' _{|| R} (d) = sem _{P; while b do P; P}' _{|| R} (d), якщо b (d) = True,

sem _{while b do P; P}' _{|| R} (d) = sem _P' _{|| R} (d), якщо b (d) = False,

|| відносно «;»:

sem _{(A; B) || P} (d) = sem _{A; (B || P)} (d),

sem _{A || P} (d) = sem _{A; P} (d),

де A, B, C, P, P', Q, R - програми в мові IPCL, b - синтаксичне позначення відповідної умови - предиката pred з Pred, тобто b (d) = sem _b (d) = pred (d), а d  DD.

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

Введено звуження класу IPCL - SeqILProgs = {Prog | Prog = Aⁿ || B^m || … || C^k; A, B, …, C  SeqTerms; n, m, …, k  Z⁺}, де Z⁺ - додатні цілі числа, SeqTerms - програми в мові IPCL, побудовані за допомогою композицій {:=,;, if, while}, без застосування композиції ||. Такі програми називаються багатоекземплярними, враховуючи багатократне використання одних і тих же компонент. Обґрунтовано природність такого класу, орієнтованого на виконання послідовних програм в режимі почергового переключення між ними. Цей клас є адекватною моделлю серверного середовища класичних клієнт-серверних систем (Web-сервери, сервери баз даних, служби операційних систем, багатопроцесорні комплекси тощо).

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

Так, для довільної програми P = Aⁿ || B^m || … || C^k  SeqILProgs (numprocs=n+m+ … +k) побудовано наступну модель її виконання: для кожної програми A, B, …, C отримуємо множину міток A_marks, B_marks, …, C_marks відповідно, які позначають місця входження функцій з F в текст програми P (згідно наведеного в роботі рекурсивного алгоритму) плюс по одній мітці, які ідентифікують стан закінчення обчислень відповідних програм. Тоді S  States = A_marksⁿB_marks^m…C_marks^kDD^numprocs називають станом системи, що виконує програму P, або станом програми P, де перше входження D в декартів добуток - «глобальні дані», а друге - «локальні» для всіх окремих послідовних підпрограм (Aⁿ, B^m, …, C^k) з P, записані в тій же послідовності, що і самі підпрограми в термі програми P. Множина States - множина станів програми P. Виділяються множини початкових станів StartStates  States та заключних станів StopStates  States, в один з яких програма P потрапляє після завершення виконання, вимагається також досяжність заключних станів згідно функції переходів Step. Step, функція кроку виконання програми P, визначає всі можливі перетворення станів - тобто переходи від одного стану до іншого - за один крок під час виконання програми P і тільки їх. Функція Step визначається разом з розстановкою міток під час опрацювання терму програми P рекурсивним алгоритмом структурного аналізу та автоматичної побудови моделюючої системи за програмою в мові, який наведено в роботі.

У випадку відсутності локальних даних у програм A, B, …, C (підпрограм P), доцільно розглядати поняття спрощеного стану - агрегованого стану наступного вигляду - N^PmqD, де Pmq = ||A_marks||+||B_marks||+ … +||C_marks||. Перші ||A_marks|| компонент такого стану містять кількість програм, що перебувають у відповідних мітках програми A в цьому стані, причому сума цих компонент в кожному стані для програми P дорівнює n - кількості інстанцій (екземплярів) програми A в P - в термінах програми P і т.д. Остання компонента D містить глобальні спільні дані для всіх підпрограм P. Спрощений стан оперує з кількостями програм, що знаходяться на кожній мітці виконання, замість ідентифікації позиції (мітки) кожної інстанції кожної окремої підпрограми (A, B, …, C). Насправді, підпрограми є нерозрізнюваними з точністю до поточної мітки виконання, якщо вони не змінюють (фактично, не мають) локальних даних, а лише оперують зі спільними глобальними даними.

В обох випадках моделлю виконання є нескінченна нерозмічена транзиційна система. Властивості формулюються наступним чином. Властивість 1 типу (з передумовою та післяумовою): для предикатів PreCond(S) та PostCond(S) і програми P виконується {PreCond(S)} P {PostCond(S)} (в термінах трійок Т. Хоара (C.A.R. Hoare)). Властивість 2 типу (інваріантного типу): предикат Inv(S) є інваріантом для програми P, якщо він виконується (є істинним) протягом всього часу (на кожному кроці) роботи програми P. Тут S - елемент множини станів або спрощених станів, в залежності від обраної моделі, причому PreCond(S) розглядається лише над початковими станами, а PostCond(S) - над заключними.

Показано рівнопотужність двох типів властивостей:

Теорема 3.1. Нехай програма P (функція переходу Step*) переводить початковий стан S (SStartStates) в кінцевий стан S' (S'StopStates). Тоді для будь-якої пари таких станів S та S' з PreCond(S) випливає PostCond(S') тоді і тільки тоді, коли існує інваріант Inv(s) такий, що є наслідком PreCond(s) для кожного початкового стану (sStartStates  (PreCond(s)  Inv(s))), з нього випливає PostCond(s) в кожному заключному стані (sStopStates  (Inv(s)  PostCond(s))) і він зберігає істинність для кожного переходу з Step ((s, s')Step  (Inv(s)  Inv(s'))).

Запропоновано метод для доведення властивості 2 типу (властивість 1 типу повинна бути зведена до 2 типу), а саме: необхідно перевірити, що SStates  S'States  ((Inv(S) & (S, S')Step)  Inv(S')). Оскільки доведення пропонується робити над «макроперетвореннями», а не мати справу з кожним конкретним переходом (яких в цьому випадку буде нескінченна кількість), то складність верифікації (доведень) у запропонованому методі є лінійною замість експоненційної для підкласу паралельних програм, який розглядається (SeqILProgs). Таким чином, метод враховує багатоекземплярність як характерну рису серверного ПЗ.

Наведено два приклади застосування методу. Один приклад - класичне паралельне додавання до однієї спільної змінної, другий - розробка моделі та верифікація системи виплати міжнародних грошових переказів Vigo Remittance Corp., реалізованої в ВАТ «Державний ощадний банк України» (доведення критичних властивостей).

Таким чином, запропонований метод ґрунтується на композиційній семантиці та має конкретні відмінності від традиційних методів перевірки моделей та методів доведення теорем. За допомогою методу передбачається верифікація підкласу паралельних програм (P = Aⁿ || B^m || … || C^k  SeqILProgs), де кількості паралельно виконуваних (під) програм є довільними натуральними (з 0) числами (n, m, …, k), фіксованими є тільки їх типи (A, B, …, C). Це спеціальний, але досить широкий, клас програм - серверне програмне забезпечення клієнт-серверних середовищ.

Висновки

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

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

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

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

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

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

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

запропонований метод апробовано на реальних системах для верифікації (зокрема, для доведення критичних властивостей системи виплати міжнародних грошових переказів 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.

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