Тема.  Основні напрямки забезпечення правильності програмних  систем

План

1. Основні напрямки правильності ПЗ.

2. Формальні методи доведення програм.

3. Процес верифікації та валідації.

 

1. Основні напрямки правильності ПЗ

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

Інспекція ПЗ — аналіз та перевірка різних уявлень системи, ПЗ (специфікацій, архітектурних схем, діаграм, вихідного коду та ін.) і виконується на всіх етапах ЖЦ розробки ПЗ.

Верифікація ПЗ — процес забезпечення правильної реалізації ПЗ, яке відповідає специфікаціям, виконується протягом усього життєвого циклу. Верифікація дає відповідь на питання: Чи правильно створена система?

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

Проводяться також наступні типи оцінок:

ü    управління планами;

ü    інспекціями;

ü    прогонами;

ü    аудитами.

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

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

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

Для перевірки правильності програм і систем використовуються такі основні напрямки:

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

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

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

До методів перевірки правильності програм відносяться:

v   методи доведення правильності програм;

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

 

2.   Формальні методи доведення програм

Ці методи з'явилися в 80—ті роки і поділяються на два класи:

1.     Точні методи доведення у правильності програм.

2.      Методи доведення у часткової правильності програм.

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

Метод Флойда

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

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

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

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

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

Метод Дейкстри включає два підходи до доведення правильності програм.

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

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

Доведення програм за цим методом можна розглядати як доведення теорем в математиці.

Методи перегляду структури програм

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

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

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

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

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

 Метод аналізу дерева відмов

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

 

Метод перевірки на несуперечність

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

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

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

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

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

 

3.     Процес верифікації та валідації

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

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

Методи верифікації об’єктно-орієнтованих програм

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

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

1.  Верифікація базових об'єктів зводиться до верифікації структури, де атрибути об'єктів є даними структури, а внутрішні операції об'єкта — функціями над цими даними.

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

ü  базові об'єкти вважаються перевіреними, якщо їх операції (функції) прийняті за теореми;

ü  доведення об'єктів зводиться до цих теорем;

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

3.  Верифікація інтерфейсів об'єктів зводиться до доведення:

ü  правильності даного інтерфейсу;

ü  достатності параметрів інтерфейсу.

Метод верифікації ООП на основі композиційного підходу можна використовувати як "вниз" так і "нагору". Спочатку доводиться правильність побудованої об’єктної моделі для певної предметної області. Верифікація об’єктної моделі вимагає реалізації на етапах ЖЦ наступних питань:

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

ü  вибору типу для атрибутів об'єкту й перевірка реалізації операцій і безлічі значень цього типу.

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

Валідація є методом перевірки відповідності спроектованого ПЗ вимогам і потребам замовника і передбачає виконання на етапах ЖЦ різного роду дій для отримання коректних програм і систем:

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

Ø   підвищення рівня автоматизації проектування програм;

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

Ø   структурування системи на модулі, їх специфікації, реалізація та використання їх як повторних компонентів (reuse);

Ø   адаптація продукту до умов використання;

Ø   управління проектом.

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

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

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

ü  компонентів системи;

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

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

ü  документації на ПЗ;

ü  тестів і тестових процедур;

ü  спеціальних засобів захисту інформації в системі.

 

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

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

Ø  аналіз способів доступу до файлів або БД відповідно до вимог, принципів передачі даних і процедур маніпулювання даними;

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

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

 

 

Питання для самоконтролю:

1. Навести методи доведення програм.

2. Метод перевірки на несуперечність.

3. Методи верифікації об’єктно—орієнтованих програм.

4. Назвіть формальні методи перевірки правильності програм.

5. Які функції у процесу верифікації програм?

6. Назвіть основні задачі процесу валідації програм.

7. Порівняйте задачі процесів верифікації і валідації програм.

8. У чому відмінність верифікації і валідації?

9. Поясніть в чому полягають процеси верифікації та валідації (Verification & Validation) програмного забезпечення, наведіть приклади.