1. Малюнок 1. Тріада перевірки вимог, коду і тестування
2. Джерело розбіжностей між тестами і кодом
3. Результати, коли вимоги, код і тести незалежні
4. Малюнок 2. Верифікація згенерованого коду
5. Малюнок 3. Валідація з верифікацією і формальна специфікація
6. Ресурси для скачування

Верифікація та валідація при формальної специфікації

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

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

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

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

Малюнок 1. Тріада перевірки вимог, коду і тестування

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

Джерело розбіжностей між тестами і кодом

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

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

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

Результати, коли вимоги, код і тести незалежні

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

Малюнок 2. Верифікація згенерованого коду

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

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

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

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

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

Малюнок 3. Валідація з верифікацією і формальна специфікація

висновок

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

Ресурси для скачування

Схожі теми

Підпишіть мене на повідомлення до коментарів