ТЕМА 6
МЕТОДИ ДОВЕДЕННЯ, ВЕРИФІКАЦІЇ І ТЕСТУВАННЯ ПРОГРАМ

 

Сучасні напрями перевірки правильності програм – це формальні специфікації, методи доведення, верифікація і тестування. Наведемо їхній зміст.

1. Формальні специфікації з’явилися у програмуванні в 70-х роках минулого сторіччя. Вони подібні МП і надають засоби, що полегшують опис міркування про властивості і особливості програм у математичній нотації. Під специфікацією розуміють формальний опис функцій і даних програм, якими ці функції оперують. На формальних специфікаціях базуються методи доведення програм, які були започатковані працями з теорії алгоритмів А.А. Маркова [1], А.А. Ляпунова [2], схемами Ю.І.Янова [3] та формальними нотаціями опису взаємодіючих процесів К.А. Хоара [4] і ін. Для перевірки формальної специфікації програми застосовують математичний апарат для опису правильного розв’язку деякої задачі, для якої вона розроблена. Разом з специфікацією розробляються додаткові аксіоми [5–10], твердження про опис операторів і умов, так звані попередні умови або передумови, і постумови, що визначають заключні правили одержання правильного результату.

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

3. Верифікація і валідація – це методи забезпечення перевірки й аналізу правильності виконання заданих функцій програми відповідно до заданих вимог замовника до них і системи у цілому.

4. Тестування – це метод виявлення помилок у ПС шляхом виконання вихідного коду на тестових даних, збирання робочих характеристик у динаміці виконання в конкретному операційному середовищі, виявлення різних помилок, дефектів, відмов і збоїв, викликаних нерегулярними, аномальними ситуаціями або аварійним припиненням роботи системи.

Теоретичні засоби реалізуються як процеси програмування і перевірки правильності програмного продукту. На даний час процеси верифікації, валідації і тестування ПС регламентовані стандартом ISO/IEC–12207 [7] з життєвого циклу ПС. У деякій зарубіжній літературі процеси верифікації і тестування на практиці ототожнюються, вони орієнтовані на досягнення правильності програми.

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

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

Передумова – це обмеження на сукупність вхідних параметрів і постумови як обмеження на вихідні параметри. Передумова і постумова задаються предикатами, результатом яких є булева величина (true/false). Передумова істинна тоді, коли вхідні параметри входять в область припустимих значень даної функції. Постумова істинна тоді, коли сукупність значень задовольняє вимоги, щодо формального визначення критерію правильності одержання результату.

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

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

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

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

5. Організаційна інфраструктура якісного проектування – це різні служби і діяльність груп фахівців, що планують процеси досягнення правильності програм (доказ, верифікація, тестування) з використанням описів тверджень, різних умов, а також тестових даних для спостереження за процесом доведення правильності програм, зокрема тестування, і збирання даних про відмови і помилки програм для їхнього використання при оцінюванні показників якості.

Далі зазначені напрями досягнення правильності програм розглядаються більш детально.

 

6.1. Мови специфікації програм і їхня класифікація

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

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

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

Існують різні підходи до класифікації мов специфікації, що наведені на рисунку 6.1.

 

Рис. 6.1. Категорії формальних мов специфікації

 

Нижче розглянуто основні мови специфікації, класифіковані за сферою застосування.

Універсальні мови специфікації – VDM, Z, RAISE, Spec# мають загально математичну основу з такими засобами:

1) логіки першого порядку, включаючи квантори;

2) арифметичні операції;

3) множини і операції над множинами;

4) описи послідовностей (кортежів, списків) і операції над ними;

5) описи функцій і операцій над ними;

6) описи деревоподібних структур;

7) засоби побудови моделей областей;

8) процедурні засоби мов програмування (оператори присвоювання, циклу, вибору, виходу);

9) операції композиції, аргументами і результатами яких можуть бути функції, вирази, оператори;

10) механізм конструювання нових структур даних.

Мови специфікації предметних областей (доменів) у програмуванні:

1) специфікації доменів;

2) описи взаємодій і паралельного виконання;

3) специфікації мов програмування і трансляторів;

4) специфікації баз даних і знань;

5) специфікації пакетів прикладних програм тощо.

Мови специфікації специфіки доменів DSL (Domain Specific Language) призначені для формалізованого опису задач в термінах предметної області, що підлягає моделюванню. Ці мови можна підрозділити на зовнішні і внутрішні. Зовнішні мови (типу UML, OWL і ін.) за рівнем вищі мов програмування і відповідають, наприклад, предметно-орієнтованої мові DSL, яка використовується для подання абстрактних понять і задач ПрО. Їхній опис трансформується до понять деякої внутрішній мові або мови програмування спеціальними генераторами або текстовими редакторами. Внутрішні мови – мови опису специфічних задач обмеженим синтаксисом і семантикою потребують препроцесорів для перебудови цього опису до базової мови програмування.

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

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

Формальні мови специфікації мов програмування спочатку застосовувалися при розробленні трансляторів. Так зазвичай синтаксис мови програмування описувався КС-граматиками у формі Бекуса–Наура. Такого типу мови є метамовами. Для специфікації семантики мов програмування використовуються формалізми рівностей. Техніка опису мов програмування базується на атрибутних граматиках і абстрактних типах даних з використанням денотаційних, алгебраїчних і атрибутних підходів. Як мови специфікації трансляторів, а також систем реального часу, де правильність і точність виконання програм є головними, використовують мови Z, VDM, RAISE.

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

Для визначення семантики рівності застосовують денотаційний, операційний і аксіоматичний опис. Операційна семантика пов’язана з підстановками (заміна, продукція) і визначається в термінах операцій, що призводять до обчислень алгоритмів. При цьому фіксується порядок і динаміка виконання операцій програми.

У денотаційному підході до семантики надається перевага статичному опису об’єктів у термінах математичних властивостей, а у аксіоматичному – специфікації властивості об’єктів у рамках деякої логічної системи, що містить у собі правила виведення формул та/або інтерпретацій.

Окрім наведеної класифікації мов специфікацій, існують інші. Наприклад, можлива класифікація специфікацій за способом виконання:

– виконувана (executable);

– алгебраїчна (algebraic);

– сценарна (use case or scenarios);

– в обмеженнях (constraints).

Виконувані специфікації припускають розробку прототипів систем для досягнення встановленої мети (VDM, SDL, RSL).

Алгебраїчні специфікації та мови SDL, RSL містять у собі механізми опису аксіом і тверджень, які призначені для доведення специфікованих програм.

Сценарні специфікації (UML) дозволяють описувати різні способи можливого застосування системи.

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

 

6.1.1. Мова формальної специфікацій – VDM

Мова специфікації VDM (Vienna Development Method) була розроблена у віденській лабораторії компанії IBM і призначалася для опису мов типу ПЛ/1, трансляторів і систем із складними структурами даних. У мові специфікується правильна програма і набір тверджень для її доведення [7, 8].

Мова містить у собі такі типи даних:

Х – натуральні числа з нулем;

N – натуральні числа без нуля;

Int – цілі числа;

Bool – булеві;

Qout – рядки символів;

Token – знаки і спеціальні позначення операцій.

Функція специфікує властивості структур даних і операцій над ними – апплікативно (функціонально) або імперативно (алгоритмічно). Наприклад, функції min у мові VDM описують двома способами:

min N1 N2 → N3,

min (N1 N2) = if N1 < N2 then N3.

Об’єкти мови VDM: множини, дерева, послідовності, відображення, сконструйовані складні структури.

Множина: X-set і операції        і ін. Правило: х  А буде коректним тільки тоді, коли А є підмножиною множини, якій належить х. Дистрибутивне об’єднання підмножин покажемо на прикладі:

union {(1, 2), (0, 2), (3, 1)} = (0, 1, 2, 3).

Списки (послідовності): Х – операція, len – довжина списку, inds – номери елемента в списку. Наприклад, inds lst =(i X [f  i  len]).

Узяття першого (голови) елемента списку – hd і залишку (хвоста) після видалення першого елемента із списку – tl. Наприклад, hd (а, b, с, d) = (a), tl (а, b, с, d) = (b, с, d).

Дерево: mk об’єднує послідовності, множини і відображення. Елементи дерев можуть конструюватися. Наприклад, час 10.30 – конструкція let mk, час (h, m) = t, tin визначає значення h = 10, а m = 30.

Відображення: map – таблиця з ключів і значень. Операція dom будує множину ключів, rng – множину його значень.

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

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

Нижче наведено покрокову деталізацію специфікації програм мовою VDM:

1. Визначення термінів, якими буде специфікуватися програма.

2. Опис понять і об’єктів, для позначення яких використовується денотат, що ідентифікується за допомогою деякого імені (або фрази).

3. Опис інваріантних властивостей програми.

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

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

6. Статичний огляд інваріанту програми щодо специфікованого формалізму доведення цього інваріанта.

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

Приклад програми. Алгоритм реєстрації компонента (ком) в репозитарії (repoz). Опис даних на мові «Паскаль» з використанням мовних конструкцій VDM при опису роботи зі списком компонентів (list_ptr).

 

post-Add_rd (r): Rn → bool

r  elems l1.rds

li’.rds = li.rds < mk-R.card(r, <>)> & li’.ctlg = li.ctlgli’ril = li.ril= type

       list = record

            next: pointer

            value: pointer

       list_ptr = list;

       R_card = record

            r.name: string;

            ком: list_ptr

       end;

       repoz = record

            rdrs: list_ptr;

            ctlg: list_ptr;

            ril: list_ptr

       end;

var

       L: repoz;

procedure Add_rd(r=string);

       rcrd: R_card;

       LL: list_ptr;

begin

       if find _rds, r) then

            begin

                        writeln (‘компонент зареєстрований);

            end;

       new (Rcrd);

       Rcrd.r_name := r;

       Rcd.ком := nil;

       new (LL);

       LL.next := L.rds;

       LL.value := ltcrd;

       L.rds := LI

end.

 

6.1.2. Мова формальної специфікації – RAISE

Мова RAISE і RSL-специфікація (RAISE Specification Language) були розроблені в 80-роках XX ст. як результат попереднього дослідження формальних методів верифікації програм і поповнення їх новими можливостями щодо доведення. Метод містить у собі нотації, техніку і інструменти для формального опису (RSL, С++ і Паскаль) програм і доведення їх правильності [9, 107].

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

У мові RSL є абстрактні типи даних і конструктори складних типів даних, такі як добуток (product), множини (sets), списки (list), відображення (map), записи (record) і т.п.

Добуток типів – це впорядкована скінченна послідовність типів Т₁, Т₂., Т_n добутку (product) Т₁  Т₂,...,  Т_n.

Кількість компонентів добутку d – це size (d) = id  (null (couter inc(counter))).

Конструктор добутку d₁ і d₂ будує добуток d₁  d₂ і значення типу product (Т₁  Т,  Т_n), тобто

make product (value 1., value n) = (value i  1) .  (value n n),

де значення value i має тип Т_i, а результуюче значення – тип добутку Т₁ Т₂ , …,  Т_n має значення  (value  n).

Списки типів – це послідовність значень одного типу list Т – можуть бути скінченним списком типів Тk і нескінченним списком типів Tn. За структуру даних типу списків можна взято бінарне дерево, в якому є голова (head), син (tail), який слідує за ним у списку, і хвіст. До операцій списку належить операція hd – узяття першого елемента списку, тобто голови, і операція tl – узяття хвоста – решти елементів (як у мові VDM).

Функція Caddr (I) = L  tail  tail  Head вибирає із списку I елемент та індекс голови елемента, кількість елементів у списку і ін.

Відображення – це структура (map), яка ставить у відповідність значенням одного типу значення іншого типу. Разом з тим відображення – це бінарне відношення декартових добутків двох множин як сукупності двокомпонентних пар, в яких перший компонент – arg, що містить у собі елементи аргументів відображення, а другий компонент – res – відповідні елементи значень цього відображення.

Операції над відображеннями такі: накладення, об’єднання, композиція, зріз, композиція відображень (m₁, m₂).

Запис – це сукупність іменованих полів даних. Цей тип відповідає типу record у мові Паскаль і struct у мові С++. У мові RAISE для запису визначено два конструктори – record, shurt record.

Об’єднання – це конструктор union, що забезпечує об’єднання типів, наприклад, type id = id₁, id₂,., id_n і тип id, який одержує одне із значень у списку елементів.

Конструктор типу – це тип виду type id = id_from_ id1 (id_to_ id1: id1).

Таким чином, мови VDM і RAISE слугують для математичного опису програм і конструювання структур даних як специфікацій, що використовуються при доведенні програм.

 

6.1.3. Концепторна мова специфікації

Для постановки складних математичних задач (підсумовування нескінченних рядів, теоретико-множинних операцій з нескінченними множинами тощо) і задач штучного інтелекту (ігри, розпізнавання образів тощо) з метою їх формального опису запропонована загально математична процедурна мова, а саме, концепторна мова (КМ) [16]. У цій мові процес опису складного завдання проводиться шляхом обґрунтування розв’язку задачі з математичної точки зору, потім формального опису постановок задач і, нарешті, переходу до алгоритмічного опису.

Специфікація складних завдань. Концепторна мова містить у собі декларативні й імперативні засоби теорії множин Цермело–Френкеля. Ядро цієї мови містить набір елементів (типи, вирази, оператори) і засоби визначення нових типів, виразів і операторів.

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

Базові елементи мови – конструктори складених типів і формул, а саме функтори, предикати, конектори і субнектори.

Функтор – це конструктор, що перетворює терми на терми.

Предикати перетворюють терми на формули.

Конекторы вміщують логічні зв’язки і квантори для перетворення однієї формули в іншу.

Субнектор (дескриптор) – це конструктор побудови термів з виразів і формул.

Імперативні засоби КМ – це оператори і процедури для опису об’єктів ПрО за допомогою концепторів. Опис процедури має такий загальний вигляд:

концептор К (<писок параметрів>)

<список імпортних параметрів>

<визначення констант, типів, предикатів>

<опис глобальних змінних>

<визначення процедури>

початок К

<тіло концептора>

кінець К.

Денотаційний підхід полягає у визначенні семантики і підстановці в кожний вираз опису елемента з множини денотатів функції  символів з сигнатури мови. Кожній константі c C, функціональному символу f  F і предикативному символу p  P зіставляється об’єкт з множини денотат. Цей спосіб інтерпретації семантики виразів і операторів мови аналогічний денотаційній семантиці мов програмування.

Аксіоматичний опис КМ – це аксіоми і твердження щодо концепторного опису і проведення дедуктивного доведення і верифікації цього опису.

Логіко-алгебраїчні специфікації КМ призначені для специфікації ПрО, що задаються у вигляді алгебраїчної системи, за допомогою відповідних носіїв, сигнатури і трьох принципів. Перший принцип – логіко-алгебраїчна специфікація ПрО і уточнення понять ПрО, другий принцип – опис властивостей ПрО у вигляді аксіом, які формулюються мовою предикатів першого порядку і хорновських атомарних формул, і, нарешті, третій принцип – це визначення термальних моделей з основних термів специфікації.

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

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

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

Приклади доведення. Нехай треба побудувати специфікацію натуральних чисел з множини цих чисел і сигнатури операцій  = (+, , ). При побудові використовується число 0 і функція проходження s: N → N’. Специфікація складається з таких аксіом:

х + 0 = х

х + s(у) = s (х+у)

х  0 = 0

х + s(у) = s (х  у) + х

0 х

х в  s (х)  s (у)

s (х)  s (у)  х  в

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

 

6.1.4. Звичайна мова специфікації Spec#

Сучасна мова специфікація Spec# є розширенням об’єктно-орієнтованої мови С# засобами, що забезпечують верифікацію програм для платформи.Net [27]. Ці засоби подаються до програми в С# невеликими додатковими описами, а саме:

– ненульових посилань до параметрів викликів CALL;

– контрактів між викликами і реалізаціями;

– обробки виникаючих виключних ситуацій програми для інформування розробника;

– змінювання полів даних об’єктів тощо.

Ненульові типи даних помічаються типом Т! і відповідають деяким змінним програми, які можуть використовуватися при специфікації полів даних, формальних параметрів і з обернених цьому типу значень, локальних змінних програми. Цей тип не належить до елементів масиву. Головне призначення ненульових типів – забезпечити посилання до інших елементів, опис патернів, перевірку умов виходу з виразів і циклів, обумовлених контрактом.

Контракт ставиться між тим, хто робить виклик, і хто – реалізацію. У передумові додається опис стану параметрів при виклику, в постумові визначається умова отримання результату об’єкта, що викликався, і передача цього результату протилежна. Spec# надає підтримку більш дисциплінованому використанню виключення, щоб забезпечити ясність і підтримку життєздатності програми. У програмі можуть бути відмови і помилки. У даному випадку у методі використовується аналіз забороненої умови, коли передумова була не задоволена. Більшість відмов у програмі – це, коли порушена умова контракту. Наприклад, отримання виходу з циклу при перевищенні значення параметра циклу, що не було визначено у передумові.

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

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

Приклад.

Class C{

Int x, y;

Void M () modifies x: {…}.

}.

Тут метод М дозволяє зміну х при умові, що на виході з цього методу у має те саме значення, що на вході. У випадку масиву такий оператор змінює не елементи масиву, а посилання – на цей масив.

Фреймові умови для сервера використовуються під час виконання програми. При цьому modifies перевіряє на вході усі передумови і постумови виконання операторів програми в С#, на яких базуються описи специфікацій в Spec# і рахуються коректними.

Успадкування специфікацій. Контрактний метод успадковується звичайним методом, який під час виконання звертається до нього. Специфікація в Spec# подає код виконання в більш наглядній формі і більш зручній для перевірки заданих постумов. Метод може додавати до опису специфікації додаткові постумови і різні реакції на виключні ситуації. Метод має об’яву в інтерфейсі, подібно до об’яві в класі. Коли клас виконує метод інтерфейса, то його опис містить у собі фреймові умови, котрі є суперкласом виконануваного методу. Для виконання фреймових умов використовується оператор expose. Він, як правило, визначає об’єкт, інваріантний модифікації. Специфікація в Spec# являє собою блок операторів, який явно вказує на те, коли об’єктний інваріант можуть явно використовувати оператори, що вказані після expose. При цьому можуть модифікуватися усі поля в структурі об’єкта.

Підхід до реалізації специфікації. Опис специфікації в Spec# є самостійною програмою, що містить у собі перед- і постумови, а також різні дії над фреймовими структурами щодо програми, яка перевіряється мовою С#. Ця специфікація подається в мово-незалежному форматі і перебудовується в мову С# за допомогою спеціального транслятора, що працює на платформі.Net. Цей транслятор має аналізатор і версифікатор для перевірки правильності опису специфікації. Транслятор виконує переклад у вигляді частини програми, для якої створювалася специфікація. Верифікація специфікації є статичною, вона орієнтована на перевірку правильності опису, а саме, меж масивів, явних значень змінних тощо. Прувер транслятора виконує перевірку деяких умов і операторів, а також значень змінних. Специфікації в Spec# накопичуються у репозитарії, і при застосуванні звертаються до Base Class Library, де накопичуються об’єкти, їхні інваріанти та контракти.

Контракти і аналогічні механізми верифікації програм з мов програмування реалізовані також в системах Java, Eiffel і Spark. У мові Java контракти вміщуються в опис програми як стилізовані коментарі. Середовище Java має такі засоби: перевірку контрактів у динаміці, виконання, виклики та об’єктні інваріанти. В об’єктно-орієнтованій системі Eiffel є бібліотека констрейнів, котрі вставляються у опис об’єкта і виконують верифікацію в динаміці виконання. Однак механізми модифікації не дозволяють для callbacks об’єктних інваріантів і тому вони не вміщуються в модульні об’єкти. Система Spark підтримує підмножину мови Ада при вставці теорем для прувера, помічених як коментарі, але компілятор цієї мови їх не використовує. Засоби верифікації в Spark орієнтовані на окремий опис умов виконання Ада-програм для верифікації, аналогічно до методології Spec#. Вони окремо транслюються у вихідний код Ада-програми і виконуються разом з нею в режимі верифікації.

 

6.2. Методи доведення правильності програм

Формальні методи тісно пов’язані з математичною специфікацією, верифікацією і доведенням правильності програм. Ці методи містять у собі математичну символіку, формальну нотацію і апарат виведення. Правила доведення є громіздкими і тому на практиці рідко використовуються рядовими програмістами. Проте з теоретичної точки зору вони слугують розвитку логіки застосування математичного методу індукції в процесі перевірки правильності програм [4, 5, 17, 18].

 

6.2.1. Базові методи доведення

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

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

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

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

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

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

Основу методу становить математична індукція, абстрактний опис програми і її обчислення. За допомогою цього методу можна довести істинність деякого припущення Р(n) залежно від параметра n для всіх n  n₀, і тим самим довести випадок Р (n₀). Виходячи з істинності Р(n) для будь-якого значення n, доводимо Р(n+1), що достатньо для доведення істинності Р(n) для всіх n  n₀.

 

6.2.2. Модель доведення програми за твердженнями

Розглядається формальне доведення програми, заданої структурною логічною схемою і сукупністю тверджень, що описуються логічними операторами, комбінаціями змінних (true/false), операціями (кон’юнкція, диз’юнкція й ін.) і кванторами загальності й існування (табл. 6.1).

 

Таблиця 6.1. Список логічних операцій

 

Мета алгоритму програми – побудова для масиву цілих чисел Т довжини N (array Т[1:N]) еквівалентного масиву Т’ тієї ж довжини N, що і масив Т. Елементи в масиві Т’ повинні розташовуватися в порядку зростання їхніх значень.

Даний алгоритм реалізується сортуванням елементів вихідного масиву Т за їхнім зростанням.

Доведення правильності алгоритму сортування елементів масиву Т (рис. 6.2) проводиться з використанням ряду тверджень про елементи цього алгоритму, якій описуються пунктами П1– П6.

П1. Вхідна умова алгоритму задається у вигляді початкового твердження:

А_beg: (Т [1:N] – масив цілих) & (Т’ [1:N] – масив цілих).

Вихідне твердження А_end – це кон’юнкція таких умов:

(а) (Т– масив цілих) & (Т’ – масив цілих)

(б) ( i, якщо i  N, то  j (T’(i)  T’ (j))),

(в) ( i, якщо i < N, то (T’ (i)  T’ (i+1))/

Тобто Аend – це:

(Т – масив цілих) & (Т’ – масив цілих)

& i, якщо i  N, то  j (T’(i)  T’ (j)),

& i, якщо i < N, то (T’ (i)  T’ (i+1)).

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

 

Рис. 6.2. Схема сортування елементів масиву Т’

 

У кружках також дано: початковий стан – 0, стан після перестановки місцями двох сусідніх елементів у масиві Т’ – одна зірочка, стан після зміни місцями всіх пар за один прохід усього масиву Т’ – дві зірочки.

Крім уже відомих змінних Т, T’ і N, в алгоритмі використані ще дві змінні: i – типу ціла і М – булева змінна, значенням якої є логічні константи true і false.

П2. Для доведення того, що алгоритм дійсно забезпечує виконання вихідних умов, розглянемо динаміку їхнього виконання послідовно у визначених точках алгоритму.

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

Так, оператор присвоєння означає, що для всіх i (i  N & i > 0) виконується (T’[i]  T[i]).

Результат виконання алгоритму в точці з нулем може бути виражений твердженням

(T[1:N] – масив цілих) & (T ‘[1:N] – масив цілих)

& ( i якщо i  N, то (T [i] = T [i])).

Доведення очевидно, оскільки за семантикою оператора присвоювання (по елементне пересилання чисел з Т в T’) самі елементи при цьому не змінюються, до того ж у даній точці їхній порядок у Т и T’ однаковий. Отже, одержали, що виконується умова «б» вихідного твердження.

Зазначимо, що перший рядок доведеного твердження збігається з умовою «а» вихідного твердження А_end і залишається справедливим до кінця роботи алгоритму, тому в наступних твердженнях наводитися не буде.

У точці з одною зірочкою виконаний оператор

(i < N) (T’(i)) > T’ (i + 1)  (T’(i) і T’(i + 1) міняє місцями елементи.

Як результат роботи оператора буде справедливе таке твердження:

 i, якщо i < N, то (T’(i) < T’(i + 1),

яке є частиною умови «в» твердження А_end (для однієї конкретної пари суміжних елементів масиву T’). Очевидно також, що семантика оператора зміни місцями не порушує умову «б» вихідного твердження А_end.

У точці з двома зірочками виконані всі можливі перестановки місцями пари суміжних елементів масиву T’ за один прохід через T’, тобто оператор зміни працював раз або більше. Однак бульбашкове сортування не дає гарантії, що досягнуто упорядкування за один прохід по масиву T’, оскільки після чергової зміни індекс i збільшується на одиницю незалежно від того, як співвідноситься новий елемент T’(i) з елементом T’(i – 1).

У цій точці також справедливе твердження

i, якщо i < N, то T’(i) < T’ (i + 1).

Частина алгоритму, позначена точкою з двома зірочками, виконується доти, поки не буде упорядкований весь масив, тобто не буде виконуватися умова «а» твердження А_еnd для всіх елементів масиву T’:

i, якщо i < N, то T’ (i) ≤ T’ (i+ 1).

Отже, виконання вихідних умов забезпечене порядком і відповідною семантикою операторів перестановки масиву.

Доведено, що виконання алгоритму програми завершено успішно, це означає її правильність.

П3. Цей алгоритм можна подати у вигляді серії теорем, що доводяться. Починаючи з першого твердження і переходячи від одного перетворення до іншого, визначаємо індуктивний шлях висновку. Якщо одне твердження є правильним, то істинним є й інше.

Іншими словами, якщо дано перше твердження А₁ і перша точка перетворення А₂, то перша теорема – А₁ → А₂. Якщо А₃ – наступна точка перетворення, то другою теоремою буде А₂ → А₃. Інакше кажучи, формулюється загальна теорема А_і → А_j, де А_і й А_j – суміжні точки перетворення. Ця теорема формулюється так: якщо умова істинна в останній точці, то і вихідне твердження А_k → А_end є істинним.

Тобто, можна повернутися до точки перетворення Аend і до попередньої точки перетворення. Якщо доведемо, що А_k → А_end справджується, то виходить, що справджується й А_j → А_j+1, і так далі, поки не одержимо, що А₁ → А₀.

П4. Далі специфікується твердження типу if – then.

П5. Щоб довести, що програма коректна, необхідно послідовно розташувати усі твердження, починаючи з А₁ і закінчуючи А_end, цим буде підтверджено істинність вхідної і вихідної умов.

П6. Доведення алгоритму програми завершено.

 

6.3. Верифікація і валідація програм

Верифікація і валідація – це методи аналізу, перевірки специфікацій і правильності виконання програм відповідно до заданих вимог і формального опису програми [18-21].

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

Верифікації і валідації піддаються:

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

– описи доступу до баз даних, засоби захисту від несанкціонованого доступу до даних різних користувачів;

– документація до системи;

– тести, тестові процедури і вхідні набори даних.

Верифікація і валідація як методи перевірки правильності виконання заданих функцій і відповідності їх вимогам замовника подані в стандарті [7−9] у вигляді самостійних процесів ЖЦ і використовуються, починаючи від етапу аналізу вимог і закінчуючи перевіркою правильності функціонування програмного коду на заключному процесі, а саме, під час тестування.

Для цих процесів визначені цілі, задачі і дії з перевірки правильності створюваного проміжного продукту на процесах ЖЦ. Розглянемо їхнє стандартне подання.

Процес верифікації. Мета процесу – переконатися, що кожен програмний продукт (і/або сервіс) проекту відбиває погоджені вимоги до їхньої реалізації. Цей процес ґрунтується:

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

– на виконанні дій з верифікації відповідно до стандарту;

– на усуненні недоліків, виявлених у програмних (робочих, проміжних і кінцевих) продуктах;

– на узгодженні результатів верифікації з замовником.

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

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

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

Процес валідації. Мета процесу – переконатися, що специфічні вимоги для програмного продукту виконано, і здійснюється це за допомогою:

– розробленої стратегії і критеріїв перевірки всіх робочих продуктів; – обговорених дій з проведення валідації;

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

– узгодження із замовником отриманих результатів валідації продукту.

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

На інших процесах ЖЦ виконуються додаткові дії:

– перевірка і контроль проектних рішень за допомогою методик і процедур перегляду ходу розробки;

– звернення до CASE-систем [10], що містять у собі процедури перевірки вимог до продукту;

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

Таким чином, основні задачі процесів верифікації і валідації полягають у тому, щоб перевірити і підтвердити, що кінцевий програмний продукт відповідає призначенню і задовольняє вимогам замовника. Ці процеси взаємозалежні і визначаються, як правило, одним загальним терміном «верифікація і валідація» або «Verification and Validation» (V&V) [19].

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

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

 

6.3.1. Підхід до валідації сценарію вимог

До процесу створення програм належить опис вимог мовою UML за допомогою сценаріїв і діючих виконавців – акторів як зовнішніх сутностей щодо системи [22]. Вимоги потрібно перевіряти до їхньої перебудови у програмні елементи. Сценарій після трансформації – це послідовність взаємодій між одним або декількома акторами і системою, у якій актор виконує мету сценарію при взаємодії з нею. У моделі вимог сценарій задає кілька альтернативних подій, заданих мовою діаграм UML. Вони розділяються на функціональні (системні) і внутрішні, як визначальне поводження системи. На основі опису сценарію вимоги перевіряються шляхом валідації для виявлення помилок у поданні сценарних вимог. Ця перевірка відбувається ітераційною і складається з наступних кроків:

1. Формалізований опис вимог у вигляді сценаріїв.

2. Створення моделі вимог.

3. Створення спеціальних сценаріїв для валідації вимог.

4. Застосування валідаційних сценаріїв у моделі вимог.

5. Оцінювання результатів поводження моделі вимог.

6. Перевірка умов завершення процесу валідації і при виявленні яких-небудь неточностей повторення кроків, починаючи з п. 2.

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

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

 

Рис. 6.3. Валідація сценаріїв вимог до системи

 

Складова частина валідації вимог за сценаріями – визначення класів еквівалентності вхідних і вихідних даних для валідації і синтезу сценаріїв. Вхідна інформація для синтезу сценаріїв – сценарна модель, що задається мовою взаємодії.

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

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

Автоматичний синтез програми заснований на наступних процедурах:

– валідація вимог шляхом виконання валідаційних сценаріїв;

– додавання перевірених сценаріїв до набору валідаційних сценаріїв і їхнє використання як вхідних даних для синтезу;

– пошук помилок у сценаріях і перевірка різних композицій сценаріїв.

Синтез специфікацій сценаріїв вимог, трансформованих до діаграмам взаємодії, може проводитися в середовищі системи Rational Rose.

 

6.3.2. Верифікація об’єктних моделей

Верифікація об’єктної моделі (ОМ) ґрунтується на специфікації:

– базових (простих) об’єктів ОМ, атрибутами яких є дані та операції об’єкта – функції над цими даними;

– об’єктів, які вважаються перевіреними, якщо їх операції використовуються як теореми, що застосовуються над підоб’єктами і не виводять їх з множини станів цих об’єктів.

Доведення правильності побудови ОМ передбачає:

– введення додаткових і (або) видалення зайвих атрибутів об’єкта і його інтерфейсів в ОМ, доведення правильності об’єкта ОМ на основі специфікації інтерфейсів і взаємодій з іншими об’єктами;

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

Це доведення є завершальним при перевірці правильності ОМ.

Верифікація інтерфейсів об’єктів ОМ зводиться до доведення правильності передачі типів і кількості даних в параметрах повідомлень про їхні специфікації в мові IDL. Інтерфейс складається з операцій звернення до об’єкта, який посилає дані іншому об’єкту через повідомлення. Для доведення правильності специфікації повідомлення створюється набір тверджень, який доводить, що для будь-якої пари елементів повідомлення, наприклад, А і В, перехід від А до В відбувається за один крок. Дія, що виконується в проміжку між А і В, приводить до В. При цьому частина тверджень перевіряє вхідний параметр і його надходження на вхід іншого об’єкта з метою підтвердження його на виході. Якщо доведено, що об’єкт, ініційований повідомленням, формує правильний вихідний результат у вихідному параметрі, то повідомлення вважається правильним.

Верифікація моделі розподіленого застосування виконується на основі специфікації SDL (Specification Description Language), моделі перевірки (Model Checking), індуктивних тверджень, запропонованих Новосибірською школою програмування [13].

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

Основні підходи до верифікації – аксіоматичний і семантичний шлях Model Сhecking.

Аксіоматичний (за методом Нoare) підхід міститься в описі програми набором аксіом для завдання станів з використанням теорія логіки.

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

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

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

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

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

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

 

6.3.3. Підхід до верифікації композиції компонентів

Метод верифікації композиції компонентів базується на специфікації функцій і часових (temporal) властивостей готових перевірених компонентів (типу reuse) і виконується за допомогою абстракцій моделі перевірки Model Сhecking [20].

Загальна компонентна модель (ЗКМ) – це сукупності перевірених специфікацій компонентів, часових властивостей і умов функціонування для асинхронної передачі повідомлень (АПП).

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

– специфікація компонентів мовою xUML [26] діалекту UML з описом часових властивостей;

– опис функцій reuse компоненти, специфікації інтерфейсу і часових властивостей;

– перевірка властивостей складних компонентів композиційним апаратом.

Компоненти моделі можуть бути примітивними і складними.

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

Даний підхід може використовуватися у розподілених програмних системах, що функціонують на платформах типу CORBA, DCOM і EJB.

Модель компонента в ЗКМ моделі має вигляд:

C = (E, I, V, P),

де E – початковий опис компонента; I – інтерфейс цього компонента; V – множина змінних, визначених в множині E і пов’язаних з властивостями з множини Р; Р – часові властивості середовища компонента.

Властивість компонента С включається в Р тоді, коли вона перевірена у середовищі і представлена парою (p, А(p)) на множині E, де p – властивість компонента С в Е, А(p) – множина часових формул з властивостей, визначених на множинах I і V.

Композиція компонентів – це сукупність простіших компонентів: (E₀, I₀, V₀, P₀),..., (E_n–i, I_n–i, V_n–i, P_n–i), визначених на моделі компонента С.

Модель обчислень АПП – це обчислювальна модель системи, задана на скінченній множині взаємодіючих процесів, представлених кортежами:

Р = (Х, Q, ), де X – множина змінних, кожна з яких має тип;  – розширена модель стану; Q – черга повідомлень у порядку надходження;  – множина початкових значень для кожної змінної з X, E і порожнє для Q.

Модель стану ПС (Ф, М, T), де Ф – множина станів; М – множина типів повідомлень; T – набір переходів, визначених на множині Ф і М.

Асинхронна передача повідомлень АПП викликає чергування переходів станів і дій процесів. Для двох процесів Р₁ і Р₂ передача повідомлення від Р₁ до Р₂ містить у собі: тип повідомлення m з множини М для P₂ і відповідні параметри. Коли оператор дії виконується, повідомлення m з параметрами ставиться у чергу до процесу Р₂.

 

6.3.4. Загальні перспективи верифікації програм

Методи формальної верифікації використовувалися для перевірки правильності моделей ПрО, функцій в мові API, безпеки і цілісності БД – у проекті SDV фірми Microsoft і у міжнародному проекті з формальної верифікації ПС.

Ідея створення цього проекту належить Т.Хоару і обговорювалася на симпозіумі з верифікованого ПС у лютому 2005г. у Каліфорнії. Потім у жовтні того ж року на конференції IFIP в Цюріху був прийнятий міжнародний проект строком на 15 років з розробки цілісного автоматизованого набору інструментів для перевірки коректності ПС [14, 15]. У проекті сформульовані такі основні задачі:

– розробка єдиної теорії створення і аналізу програм;

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

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

Репозітарій – це сховище правильних програм, специфікацій і інструментів.

Функції репозитарію:

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

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

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

– розробка механізмів взаємодії для перенесення готових верифікованих продуктів з репозитарію в нові розподілені і мережні середовища для їхнього використання в нових ПС.

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

 

6.4. Тестування програмних систем

Тестування – це метод виявлення помилок у ПС шляхом виконання вихідного коду на тестових даних, збирання робочих характеристик у динаміці виконання в конкретному операційному середовищі, виявлення різних помилок, дефектів, відмовлень і збоїв, викликаних нерегулярними, аномальними ситуаціями або аварійним припиненням роботи системи. Його можна розглядати, як процес семантичного налагодження (перевірки) програми, що полягає у виконанні послідовності різних наборів контрольних тестів, для яких заздалегідь відомий результат. Тобто тестування припускає виконання програми й одержання конкретних результатів виконання тестів [24-26].

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

Історично першим видом тестування було налагодження.

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

Мета тестування – перевірка виконання реалізованих функцій відповідно до їхньої специфікації. На основі зовнішніх специфікацій функцій і проектної інформації на процесах ЖЦ створюються функціональні тести, за допомогою яких проводиться тестування з урахуванням вимог, сформульованих на процесі аналізу предметної області. Методи функціонального тестування підрозділяються на статичні і динамічні.

 

6.4.1. Статичні методи тестування

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

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

Інспекція ПС – це статична перевірка відповідності програми заданим специфікаціями, проводиться шляхом аналізу різних представлень результатів проектування (документації, вимог, специфікацій, схем або коду програм) на процесах ЖЦ. Перегляди й інспекції результатів проектування і відповідності їх вимогам замовника забезпечують більш високу якість створюваних ПС.

При інспекції програм розглядаються документи робочого проектування на процесах ЖЦ разом з незалежними експертами й учасниками розробки ПС. На початковому процесі проектування інспекція припускає перевірку повноти, цілісності, однозначності, несуперечності і сумісності документів з вимогами до програмної системи. На процесі реалізації системи під інспекцією розуміють аналіз текстів програм на дотримання вимог стандартів і прийнятих керівних документів технології програмування.

Ефективність такої перевірки полягає в тому, що залучені експерти намагаються подивитися на проблему «з боку» іпіддають її всебічному критичному аналізу.

Ці прийоми дозволяють на більш ранніх процесах проектування знайти помилки або недоробки шляхом багаторазового перегляду вхідного опису програми. Символьне тестування застосовується для перевірки окремих ділянок програми на вхідних символьних значеннях.

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

 

6.4.2. Динамічні методи тестування

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

Динамічне тестування орієнтоване на перевірку коректності ПС на множині тестів, що проганяються по ПС, з урахуванням зібраних даних на процесах ЖЦ, проведення виміру окремих показників (число відмов, збоїв) тестування для оцінки характеристик якості, зазначених у вимогах, шляхом виконання системи на ЕОМ. Тестування ґрунтується на систематичних, статистичних, (імовірнісних) і імітаційних методах. Охарактеризуємо їх

Систематичні методи тестування поділяються на методи, у яких програма розглядається як «чорна скринька» (використовується інформація про розв’язувану задачу), і методи, у яких програма розглядається як «біла скринька» з використанням структури програми. Цей вид називають тестуванням з керуванням за даними або керуванням на вході-виході. Ціль – з’ясування обставин, при яких поводження програми не відповідає її специфікації. При цьому кількість виявлених помилок у програмі є критерієм якості тестування.

Ціль динамічного тестування програм за принципом «чорної скриньки» – виявлення одним тестом максимального числа помилок з використанням невеликої підмножини можливих вхідних даних.

Методи «чорної скриньки» забезпечують:

– еквівалентне розбиття;

– аналіз граничних значень;

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

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

Класи еквівалентності виділяються шляхом перебору вхідних умов і розбивки їх на дві групи або більше. При цьому розрізняють два типи класів еквівалентності: правильні, що задають вхідні дані для програми, і неправильні, засновані на завданні помилкових вхідних значень.

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

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

Метод «білої скриньки» дозволяє досліджувати внутрішню структуру програми, при чому виявлення всіх помилок у програмі є критерієм вичерпного тестування маршрутів потоків (графа) передач керування, серед яких розглядають:

а) критерій покриття операторів – набір тестів у сукупності повинен забезпечити проходження кожного оператора не менше ніж один раз;

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

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

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

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

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

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

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

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

 

6.4.3. Функціональне тестування

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

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

До задач функціонального тестування належать:

– ідентифікація множини функціональних вимог;

– ідентифікація зовнішніх функцій і побудова послідовностей функцій відповідно до їхнього використання в ПС;

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

– побудова тестових наборів і сценаріїв тестування функцій;

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

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

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

Передумови функціонального тестування:

– коректне оформлення вимог і обмежень до якості ПС;

– коректний опис моделі функціонування ПС у середовищі експлуатації замовника;

– адекватність моделі ПС заданому класу.

 

6.5. Інфраструктура перевірки правильності програмних систем

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

Команда виконує дії з підготовки і проведення таких задач:

– виділення об’єктів перевірки на процесах ЖЦ та на завершальному процесі тестування;

– аналіз і класифікація помилок для розглянутого класу програм, що перевіряються;

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

– підготовка даних і тестів для їхнього виконання і пошуку різного роду помилок і відмовлень у компонентах і в системі в цілому;

– розробка завдань підгрупами команди з проведення і керування процесом досягнення правильної програми;

– підготовка до перевірки виконання вимог до ПС і до системи;

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

Об’єкти процесу – компоненти, групи компонентів, підсистеми і система. Для кожного з них формується стратегія проведення верифікації і тестування. Якщо об’єкт готовий і належить до «білої скриньки» або до «чорної скриньки», склад компонентів якого невідомий, то верифікація функцій проводиться зі спеціально підготовленими даними перевірки функцій і вхідних тестових даних для тестування й отримання вихідних даних. Головна мета верифікації перевірити правильність виконання функцій.

Стратегічна мета тестування – переконатися, що кожен розглянутий вхідний набір даних відповідає очікуваним вихідних даним. Проектувальник тестів повинен заглянути усередину «чорної скриньки» і досліджити деталі процесів обробки даних, питання забезпечення захисту і відновлення даних, а також інтерфейси з іншими програмами і системами. Це сприяє підготовці тестових даних для проведення тестування. Для деяких типів об’єктів група інженерії тестування не може згенерувати представницьку безліч тестових наборів, що демонстрували б функціональну правильність роботи компонентів при всіх можливих наборах тестів.

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

 

6.5.1. Класифікація помилок і методи їхнього пошуку

Міжнародний стандарт ANSI/IEEE–729–83 розділяє всі помилки в розробці програм на такі типи.

Помилка (error) – стан програми, при якому видаються неправильні результати, причиною яких є недоліки (flaw) в операторах програми або в технологічному процесі її розробки, що приводить до неправильної інтерпретації вихідної інформації, отже, і до невірного розв’язку.

Дефект (fault) у програмі – наслідок помилок розробника на кожному з процесів проектування, що може утримуватися у вхідних або проектних специфікаціях, текстах кодів програм, експлуатаційній документації тощо. У процесі виконання програми можуть бути виявлені дефект або збій.

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

– помилкова специфікація або пропущена вимога, яка означає, що специфікація точно не відбиває того, що припускав користувач;

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

– проект програми може містити у собі помилки (наприклад, база даних спроектована без засобів захисту від несанкціонованого доступу користувача, а потрібен захист);

– програма може бути неправильною, тобто вона виконує невластивий алгоритм або він реалізований не цілком.

Таким чином, відмова, як правило, є результатами однієї помилки або більше у програмі, а також наявності різного роду дефектів.

Загальні класи помилок. Усі помилки, що виникають у програмах, розподіляють на такі класи [14, 26]:

– логічні і функціональні помилки;

– помилки обчислень і часу виконання;

– помилки вводу-виводу і маніпулювання даними;

– помилки інтерфейсів;

– помилки обсягу даних і ін.

Логічні помилки – наслідок порушення логіки алгоритму, внутрішньої непогодженості змінних і операторів, а також мовних правил програмування. Функціональні помилки – наслідок неправильно визначених функцій, порушення порядку їхнього застосування або відсутності повноти їхньої реалізації і т.д.

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

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

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

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

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

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

Фірма IВМ розробила підхід до класифікації помилок, названий ортогональною класифікацією дефектів [21]. При такому підході розподіл помилок за категоріями робить відповідальний розробник. Класифікація не залежить від продукту, організації розробки, вона може застосуються до всіх процесів розробки ПС різного призначення. Відповідно до даної класифікації в табл. 6.2 наведено список помилок.

 

Таблиця 6.2. Ортогональна класифікація дефектів IBM

 

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

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

Фірма Hewlett–Packard використовувала класифікацію Буча, встановивши відсоткове співвідношення помилок, що виявляються в ПС на різних стадіях розробки (рис. 6.4.).

 

Рис. 6.4. Відсоткове співвідношення помилок при розробці ПС

 

Це співвідношення, типове для багатьох фірм, що роблять ПС, має деякі відхилення від інших.

Згідно з даними [32] вартість аналізу і формування вимог, внесення до них змін становить приблизно 10%, аналогічно оцінюється вартість специфікації продукту. Вартість кодування оцінюється більше ніж 20%, а вартість тестування продукту дорівнює більш ніж 45% його загальної вартості. Значну частину вартості становить супровід готового продукту і виправлення виявлених у ньому помилок.

Дослідження фірм IBM показали, чим пізніше виявляється помилка в програмі, тим дорожче коштує її виправлення, ця залежність близька до експонентної. Так, військово-повітряні сили США оцінили вартість розробки однієї інструкції в 75 доларів, а вартість супроводу дорівнює близько 4000 доларів.

 

Зв’язок помилки з відмовою. Наявність помилки в програмі, як правило, приводить до відмови ПС при його функціонуванні. Для аналізу причинно- наслідкових зв’язків «помилка-відмова» виконуються такі дії:

– ідентифікація помилок у технологіях проектування і програмування;

– взаємозв’язок помилок процесу проектування і помилок, що допускаються людиною;

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

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

– перевірка і захист від помилок на всіх процесах ЖЦ, а також виявлення дефектів на кожному процесі розробки;

– зіставлення дефектів і відмовлень у ПС для розробки системи взаємозв’язків і методики локалізації, збирання й аналізу інформації про відмови і дефекти;

– розробка підходів до процесів документування й супроводження ПС.

Кінцева мета причинно-наслідкових зв’язків «помилка-відмова» полягає у визначенні методів і засобів тестування і виявлення помилок визначених класів, а також критеріїв завершення тестування на множині наборів даних; у визначенні шляхів удосконалювання організації процесу розробки, тестування і супроводу ПС.

Наведемо таку класифікацію типів відмов:

– апаратна, при якому загальносистемне ПС не працездатне;

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

– програмна, при наявності помилок у компонентах системи;

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

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

 

6.5.2. Процес тестування за життєвим циклом

Наведені типи помилок розподіляються за процесами ЖЦ і їм відповідають такі джерела їхнього виникнення [23, 24]:

– ненавмисне відхилення розробників від робочих стандартів або планів реалізації;

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

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

Розглянемо процес тестування, виходячи з рекомендацій стандарту ISO/IEC– 12207, і наведемо типи помилок, що виявляються під час кожного процесу ЖЦ.

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

Характерними помилками цього процесу є:

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

– некоректність специфікації взаємодії ПС із середовищем функціонування або з користувачами;

– невідповідність вимог замовника окремим і загальним властивостям ПС;

– некоректність опису функціональних характеристик;

– незабезпеченість інструментальними засобами всіх аспектів реалізації вимог замовника й ін.

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

– погодженістю інтерфейсу користувача із середовищем;

– описом функцій (неадекватність цілей і задач компонентів, що виявляються при перевірці комплексу компонентів);

– визначенням процесу обробки інформації і взаємодії між процесами (результат некоректного визначення взаємозв’язків компонентів і процесів);

– некоректним завданням даних і їхніх структур при описі окремих компонентів і ПС у цілому;

– некоректним описом алгоритмів модулів;

– визначенням умов виникнення можливих помилок у програмі;

– порушенням прийнятих для проекту стандартів і технологій.

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

Причиною помилок є:

– безконтрольність значень вхідних параметрів, індексів масивів, параметрів циклів, вихідних результатів та ін.;

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

– порушення стандартів кодування (погані коментарі, нераціональне виділення модулів і компонентів та ін.);

– використання одного імені для позначення різних об’єктів або різних імен одного об’єкта, погана мнемоніка імен;

– непогоджене внесення змін у програму різними розробниками та ін.

Процес тестування. На цьому процесі помилки допускаються програмістами і тестувальниками при виконанні технології збирання і тестування, вибору тестових наборів і сценаріїв тестування та ін. Відмови в програмному забезпеченні, викликані такого роду помилками, повинні виявлятися, усуватися і не впливають на статистику помилок компонентів і на програмне забезпечення в цілому.

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

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

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

Команда розробників системи може також змінити мову опису системи. Деякі помилки можуть бути не виявлені (наприклад, неправильно задані індекси або значення змінних цих операторів).

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

Тестові дані слугують для перевірки роботи системи і складаються різними способами: генератором тестових даних, проектною групою на основі документів або наявних файлів, користувачем з специфікаціях вимог та ін. Дуже часто розробляються спеціальні форми вхідних документів, у яких відображається процес виконання програми за допомогою тестових даних [23-25, 31].

Створюються тести, що перевіряють:

– повноту функцій;

– погодженість інтерфейсів;

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

– надійність виконання системи;

– захист від збоїв апаратури і не виявлених помилок та ін.

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

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

Залежно від задач, що ставляться перед тестуванням програм, складаються тести перевірки проміжних результатів проектування елементів на процесах ЖЦ, а також створюються тести іспитів остаточного коду системи.

Тестування інтегрованої системи. Тести для перевірки окремих елементів системи і тести інтегрованої системи мають загальні і відмінні риси. Як приклад розглянемо схему інтеграції компонентів.

На першому рівні схеми знаходяться, наприклад, компоненти А, B, D, на другому рівні – E, C, G. Вони пов’язані між собою інтерфейсом (рис.6.5).

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

 

Рис. 6.5. Схема тестування інтегрованих компонентів

 

Тести перевіряють внутрішню структуру, логіку і граничні умови виконання кожного компонента. Спочатку тестуються компоненти А, B, D незалежно один від одного і кожний з окремим тестом. Після їхньої перевірки виконується перевірка інтерфейсів для зв’язку компонентів другого рівня: А → E, B → C, D → G, а потім вже компоненти Е, C, G.

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

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

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

Приклад. Оцінювання часу тестування та ризиків відмов модулів.

Нехай ми маємо приклад деякої системи інформаційно-аналітичної підтримки прийняття управлінських рішень із модулів [31, 33] (табл. 6.3.).

Вони функціонують у розподіленому середовищі Oracle RunTime та MS Office (Word, Excel).

 

Таблиця 6.3. Склад програмних комплексів ПС

 

Найбільший внесок у ризик відмов робить ПК3 контролю і введення даних до БД Oracle, який функціонує на 10 робочих місцях. Його головне призначення – контроль даних у формах, підготовлених за допомогою ПК1 та їх експорт до БД. ПК3 виконує запис у більш як 90 таблиць БД, використовує понад 50 нормативно- довідкових таблиць та класифікаторів.

На процесі проектування для цього ПК був виконаний аналіз можливих сценаріїв функціонування (рис. 6.4) за декількома способами використання.

 

Таблиця 6.4. Функції модулів, що надають найбільший внесок у відмови ПС

 

Функції кожного з модулів М1-М5 дійсно є критичними для ПС, оскільки від їх безвідмовної роботи залежить цілісність системи.

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

Очікуваний час t₀ використання кожного модуля при експлуатації ПС та їхні внески С_м визначалися тижневе, місячно, а також – частоти звернення до модулів у кожному сеансі роботи ПК3. Отримані дані про відмови та оцінені параметри моделі надійності наведені в табл. 6.5.

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

 

Таблиця 6.5. Оцінки параметрів моделі надійності для п’яти модулів ПК3

 

Для модулів були встановлені значення різних даних з процесу тестування (табл. 6.6.), а саме:

– вартість одиниці часу тестування с₁ = 0.8 грн.;

– вартість усунення дефекту с₂ = 60 грн.

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

 

Таблиця 6.6. Оцінки часу використання, внесків, ризику та оптимального часу тестування модулів ПК3

 

Наведені таблиці з тестування групи програмних компонентів (ПК1–ПК7) демонструють послідовний процес аналізу і оброблення інформації при їхньому тестуванні і оцінюванні результатів.

 

6.5.3. Інженерія керування тестуванням

За функціональні і системні тести несуть відповідальність розробник і замовник, останній більше впливає на складання тестів для випробувань системи [26, 28, 32].

Цей процес реалізує група тестувальників, що не залежать від групи розробників ПС. Її очолює керівник групи, який повинен мати:

– досвід в області тестування;

– здатність бути лідером і керувати групою тестувальників;

– знання з задач предметної області (і програмного продукту); – знання з інфраструктури (апаратного і системного програмного забезпечення).

Рядовий тестувальник повинен знати:

– галузь виробництва продуктів/технологій створення ПС;

– елементи інфраструктури розробки ПС;

– вимоги до системи і стандарти тестування;

– підходи до використання робочих продуктів процесу тестування;

– інструменти і стратегії тестування;

– вміти аналізувати результати і підбирати нові тестові дані або додавати дані для оцінювання процесу тестування.

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

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

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

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

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

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

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

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

Тестові інженери створюють тестові сценарії (Test Cases), кожний з яких перевіряє результат взаємодії між актором і системою на основі перед- і постумов використання таких сценаріїв. Сценарії в основному належать до тестування за типом «білої скриньки» і орієнтовані на перевірку структури й операцій інтеграції компонентів системи.

Для проведення тестування тестові інженери пропонують процедури тестування (Test Procedures), що вміщують валідацію об’єктів і верифікацію тестових сценаріїв відповідно до плану графіку. Оцінка тестів (Test Evaluation) полягає в оцінці результатів тестування, ступеня покриття програм сценаріями і статусу отриманих помилок. На рис. 6.6. наведено коло обов’язків інженера- тестувальника.

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

 

Рис. 6.6. Схема відповідальності інженера-тестувальника

 

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

Керування тестуванням. Усі засоби тестування ПС об’єднуються базою даних, де містяться результати тестування системи, а також компоненти, тестові контрольні дані й інформацію про документування процесу тестування.

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

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

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

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

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

4. Результати тестування документуються відповідно до діючого стандарту ANSI/IEEE 829 і містять у собі:

– опис задач, призначення і зміст ПС, а також перелік функцій відповідно до вимог замовника;

– технологію розробки системи;

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

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

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

Висновки. Були розглянуті формальні специфікації програм, методи доведення програм за ними, а також сучасні методи і процеси верифікації та тестування ПС, засновані на понятті програм – «біла скринька» і «чорна скринька». Визначено критерії тестування, типи помилок, що виявляються в програмах, а також відмови і помилки на процесах ЖЦ. Сформульовано методи забезпечення процесів отримання правильних програм за допомогою спеціальних груп фахівців, зокрема тестувальників.