конспект лекцій (ТСПП). Конспект лекцій з дисципліни 07 технологія створення програмних продуктів напряму 050101 Компютерні науки
 Скачать 14.87 Mb.
|
2.5. Вертифікація -статичні, напівстатичні і динамічні структури. Класифікація структур даних. Рисунок 4. Схема используемой классификации методов верификации.
Зазвичай як види експертиз виділяють організаційні експертизи (management review), технічні експертизи (technical review), наскрізний контроль (walkthrough), інспекції (inspection) і аудити (audit). З середини 1990-х активно розвиваються методи оцінки архітектури ПО на основі сценаріїв (scenario based software architecture evaluation), зазвичай не співвідношувані з "традиційними" експертизами. Від інших методів верифікації експертизу відрізняє можливість виконувати її, використовуючи тільки самі артефакти життєвого циклу, а не їх моделі (як у формальних методах) або результати роботи (як в динамічних). Експертиза застосована до будь-яких властивостей ПО і будь-яких артефактів життєвого циклу і на будь-якому етапі проекту, хоча для різних цілей можуть використовуватися різні її види. Вона дозволяє виявляти практично будь-які види помилок, причому робити це на етапі підготовки відповідного артефакту, тим самим мінімізуючи час існування дефекту і його наслідку для якості похідних артефактів. В той же час експертиза не може бути автоматизована і вимагає активної участі людей. Емпіричні спостереження показують, що ефективність експертиз в термінах відношення кількості дефектів, що виявляються, до ресурсів, що витрачаються на це, дещо вищий, ніж для інших методів верифікації. Так, різні звіти показують, що від 50 до 90% усіх зафіксованих в життєвому циклі ПО помилок може бути виявлено за допомогою експертиз. За рахунок їх раннього виявлення може бути досягнута істотна економія ресурсів - витрати на виявлення помилки складають від 5 до 80% від таких же витрат при використанні тестування. Крім того, регулярна участь в експертизах є важливим чинником в навчанні співробітників і сприяє підвищенню якості результатів їх роботи. В той же час ефективність експертизи істотно залежить від досвіду і мотивації її учасників, організації процесу, а також від забезпечення коректної взаємодії між різними учасниками. Це накладає додаткові обмеження на розподіл ресурсів в проекті і може призводити до конфліктів між розробниками, якщо керівництво проекту звертає мало уваги на комунікативні аспекти проведення експертиз.
Такий аналіз добре автоматизується і може бути практично повністю покладений на інструменти, хоча іноді необхідно вручну визначити, наприклад, прийняті в проекті стандарти кодування. Проте застосовний він лише до коду або до певних форматів представлення проектних артефактів, і здатний виявляти тільки обмежений набір типів помилок. Однією з відомих проблем статичного аналізу є також наступна дилема: або використовуються строгі методи аналізу, що не допускають пропуску помилок (тих типів, що шукаються), але що призводять до великої кількості повідомлень про можливі помилки, які такими не є, або точним є набір повідомлень про помилки, але виникає можливість пропустити помилку. Інструменти автоматичної верифікації на основі статичного аналізу застосовуються досить широко, оскільки не вимагають спеціальної підготовки і досить зручні у використанні. Більшість техніки статичної перевірки коректності програм, що довели свою ефективність на практиці, рано чи пізно стають частиною компіляторів або навіть перетворяться в семантичні правила мов програмування.
Аналіз формальних моделей виконується за допомогою специфічної техніки, таких як дедуктивний аналіз (theorem proving), перевірка моделей (model checking) або абстрактна інтерпретація (abstract interpretation). Формальні методи застосовані тільки до тих властивостей, які виражені формально у рамках деякої математичної моделі, а також до тих артефактів, для яких можна побудувати адекватну формальну модель. Відповідно, для використання таких методів в проекті необхідно витратити значні зусилля на побудову формальних моделей. До того ж, побудувати такі моделі і провести їх аналіз можуть тільки фахівці з формальних методів, які не так багато, і чиї послуги коштують досить дорого. Побудову формальних моделей не можна автоматизувати, для цього завжди потрібна людина. Аналіз їх властивостей значною мірою може бути автоматизований, і зараз вже є інструменти, здатні аналізувати формальні моделі промислового рівня складності, проте щоб ефективно користуватися ними часто теж потрібно дуже специфічний набір навичок і знань (у специфічних розділах математичної логіки і алгебри). Проте, у ряді областей, де наслідки помилки в системі можуть виявитися надзвичайно дорогими, формальні методи верифікації активно використовуються. Вони здатні виявляти складні помилки, що практично не виявляються за допомогою експертиз або тестування. Крім того, формалізація вимог і проектних рішень можлива тільки при їх глибокому розумінні, і тому змушує провести ретельний аналіз цих артефактів, для чого часто потрібна спільна робота фахівців з формальних методів і експертів в предметній області. У останні 10 років з'явилися засновані на формальних методах інструменти, вирішальні досить обмежені завдання верифікації ПО з певного класу, та зате здатні ефективно працювати в промислових проектах і що вимагають для застосування мінімальних спеціальних навичок і знань. Набагато частіше, ніж до програм, формальні методи верифікації на практиці застосовуються до апаратного забезпечення. Їх використання в цій області має довшу історію, що привело до створення зріліших методик і інструментів. Це обумовлено вищою вартістю помилок для апаратного забезпечення, одноріднішою його структурою і простішими примітивними елементами, ширшим багатократним використанням проектної інформації, а також більшою звичністю строгих обмежень і точних описів для інженерів.
Прикладами такого роду методів являються звичайне тестування або імітаційне тестування, моніторинг, профілізація. Для застосування динамічних методів необхідно мати працюючу систему або хоч би деякі її компоненти, або ж їх прототипи, тому не можна використовувати їх на перших стадіях розробки. Зате з їх допомогою можна контролювати характеристики роботи системи в її реальному оточенні, які іноді неможливо акуратно проаналізувати за допомогою інших підходів. Динамічно методи дозволяють виявляти в ПО тільки помилки, що проявляються при його роботі, а, наприклад, дефекти зручності супроводу знайти не допоможуть, проте, помилки, що виявляються ними, зазвичай вважаються серйознішими. Для застосування динамічних методів верифікації зазвичай потрібно додаткову підготовку - створення тестів, розробку тестової системи, що дозволяє їх виконувати або системи моніторингу, що дозволяє контролювати певні характеристики поведінки системи, що перевіряється. Але системи тестування, профілізації або моніторингу можуть бути зроблені один раз і використовуватися багаторазово для широких класів ПО, лише самі тести необхідно готувати наново для кожної системи, що перевіряється. В той же час підготовка тестів на ранніх етапах створення ПО дозволяє виявити безліч дефектів в описі вимог і проектних документах - фактично, розробники тестів вимушені в ході своєї діяльності виконувати експертизу артефактів, що служать основою для тестів. Створення набору тестів, що дозволяють отримати адекватну оцінку якості складної системи, є досить трудомістким завданням. Проте серед розробників промислового ПО склалася (не цілком вірне) думка, що тестування є найменш ресурсоємним методом верифікації, тому на практиці воно використовується для оцінки властивостей ПО дуже широко. При цьому найчастіше застосовується не занадто надійна, але досить дешева техніка, такі як (нестроге) імовірнісне тестування, при якому тестові дані генеруються випадковим чином, або ж тестування на основі простих сценаріїв використання, перевіряючі лише найбільш прості ситуації.
У останні 10-15 років з'явилася безліч дослідницьких робіт і інструментів, у рамках яких застосовуються елементи декількох перерахованих вище видів верифікації. Так, в окремі області виділилися динамічні методи, що використовують елементи формальних, - тестування на основі моделей (model - based testing, model driven testing) і моніторинг формальних властивостей (runtime verification, passive testing). Ряд інструментів побудови тестів істотно використовує як формалізацію деяких властивостей ПО, так і статичний аналіз коду. Загальна ідея таких методів цілком зрозуміла - спробувати поєднувати переваги основних підходів до верифікації, купировав їх недоліки. Представлена тут класифікація методів верифікації швидше обумовлена історичними причинами, чим заснована на істотних характеристиках самих цих методів. Дослідники і розробники нових методів і інструментів, намагаючись співвіднести свої роботи з роботами попередників, зазвичай шукають їх у рамках однієї з вказаних груп, тому зараз така схема досить зручна. Проте, як вже було сказано, останнім часом створюються синтетичні методи, що поєднують елементи усіх інших, і через 5-10 років, після появи досить великої кількості таких підходів, буде потрібно детальнішу і змістовнішу класифікацію методів верифікації. Далі при огляді окремих методів верифікації методи, що відносяться до одного типу, розглядаються разом. Найчастіше при цьому описується більш-менш детально тільки один представник цього типу, а також вказуються характеристики, по яких методи того ж типу можуть відрізнятися один від одного. |