1. Сильні і слабкі сторони модельного підходу
2. якісні характеристики
3. Модельна верифікація в реальному проекті

18.12.2003 Олександр Аграновський, Вадим Зайцев, Борис Телеснін, Роман Хаді

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

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

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

Сильні і слабкі сторони модельного підходу

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

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

У тому випадку, коли властивість виявляється порушеним, у вигляді контрпримера надається діагностує інформація.

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

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

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

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

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

якісні характеристики

Ще не так давно всі вимоги до додатків ділилися на функціональні і нефункціональні. Перші, як правило, були представлені двійковим значенням «працює / не працює», а другі - довгим списком властивостей, верифікованих суб'єктивно (наприклад, «дружелюбність, стійкість, безпеку»). Останнім часом ситуація змінилася, і повний список типів можливих вимог був стандартизований в рамках стандарту ISO 9126 [ 1 ].

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

• Придатність. - Чи виконує додаток призначену йому завдання? Може бути верифіковано шляхом моделювання правильного супутнього оточення (підхід, аналогічний тестуванню).
• Точність. - Наскільки точні результати роботи програми? Важко реалізується при модельному підході; логічна верифікація в даному випадку буде більш ефективна.
• Безпека. - Чи не відбувається неавторизованої витоку інформації? Верифицируется безпосередньо з формулюванням відповідних запитів. Також існує цілий ряд немодельний верифікаторів, які вирішують цю ж задачу.
• Відповідність. - Чи відповідає реалізована функція даного стандарту? Стандарт використовується як специфікація (джерело вимог), реалізація функції моделюється.
• Сумісність. - Чи може цей додаток спілкуватися з відповідними програмними продуктами від інших виробників? Близьким наближенням є мається на увазі сумісність при наявності відповідності стандарту і відсутності недокументованих можливостей. При необхідності більш точної перевірки виконує автоматичне дизасемблювання і емуляцію заданих ділянок програмного коду, ручну налагодження, побудова графа передачі управління і даних.

Безліч атрибутів надійності характерізуюется здатність програмного забезпечення підтримувати певний рівень послуг, що надаються за даних умов і протягом заданого проміжку часу [1,5].

• Завершеність. - Чи є спочатку надається рівень послуг достатнім? Чи все було реалізовано? Це властивість за визначенням не може бути перевірено формальним тестуванням: на кожну очікувану функцію формулюється вимога (або безліч вимог), які перевіряються на моделі.
• Стійкість до помилок. - Чи веде себе програма адекватно в разі надання завідомо неправдивих вхідних даних? Дуже неефективно і громіздко реалізується в модельному підході, існують непогані методи тестування, що вирішують цю проблему.
• Стійкість до оточення (міцність). - Чи може додаток працювати нормально в нестандартному або нестійкому оточенні? Застосування модельного підходу в даному випадку можливо тільки при наявності можливості моделювання оточення. Однак коректне моделювання стрес-ситуації - досить нетривіальне завдання.
• Восстанавливаемость. - Чи може додаток продовжувати роботу після збою? Як правило, це властивість явно прописується в програмі і потребує тільки в перевірці. Може бути перевірено як модельної верифікацією, так і тестуванням.

Безліч атрибутів по зручності користування характеризує труднощі при використанні програмного забезпечення та їх суб'єктивну оцінку тим чи іншим безліччю користувачів [1, 6].

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

Безліч атрибутів продуктивності виявляє зв'язок рівня наданих додатком послуг з обсягом використовуваних при цьому ресурсів [ 1,7 ].

• Поведінка в часі. - Адекватний чи часовий графік використання ресурсів? В даному випадку потрібно тестувати реальну систему, а не її модель (наприклад, для знаходження витоку пам'яті). Абсолютно не підходить для модельної верифікації.
• Використання ресурсів. - Чи ефективно використовуються ресурси? Є спрямованість на реальну систему і існують ефективні методи формального тестування, які в основному базуються на суміші сетй Петрі і спеціалізованих мовах опису моделей верифікації, при прогоні яких відбувається кількісна оцінка потенційно використовуваних ресурсів; максимальне значення дає цілком ефективну оцінку, придатну для більшості реалізацій.
• Алгоритмізація. - Наскільки оптимальні використані алгоритми? Класичний аналіз алгоритмів разом з формальної їх верифікацією дає швидкі і точні результати.

Безліч атрибутів підтримки пов'язано із зусиллями щодо внесення певних змін в працююче додаток [1, 8].

• Аналізований. - Наскільки легко визначити частини, які потребують зміні? Hе піддається формалізації.
• Змінність. - Які зусилля потрібні для внесення змін? Hе піддається формалізації, рівень може бути встановлений апріорі.
• Hастраіваемость. - Чи можна досягти бажаного ефекту без зміни самої програми, змінюючи тільки настройки? Завдання вирішується тестуванням в реальних умовах.
• Стабільність. - Як поводиться програма при внесенні змін на льоту? Ефективно вирішується модельної верифікацією за допомогою недетермінірованних паралельних процесів.
• Тестованого. - Наскільки легко перевіряється робота зміненого контуру? Вирішується паралельно з тестуванням або превентивно явно і до верифікації відносини практично не має.

Безліч атрибутів переместімость характеризує здатність програмного забезпечення бути перенесеним з одного оточення в інше [1, 9].

• Пристосовність. - Чи може додаток змінюватися відповідно до змін оточення? Взаємодіючі недетерміновані послідовні процеси дають хороший результат, в тому числі, і в модельному підході.
• Устанавліваеми. - Чи може додаток встановлюватися на різні платформи або в різні конфігурації? Як правило, явно задається в специфікації і явно реалізується і в перевірці не потребує.
• Узгодженість. - Які стандарти були використані в додатку? Hе потребує перевірки, проте саме відповідність стандартам перевіряти можна і потрібно.
• Замінність. - Чи може додаток бути використано так само, як його еквівалент від іншого виробника? Чи залежить від списку опцій відповідних додатків, які могли б бути або повинні були бути реалізовані? Це відноситься до фази формулювання вимог, тому в верифікації не бере.

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

література

1. International Standard ISO / IEC 9126. Information Technology - Software Product Evaluation - Quality Characteristics and Guidelines for their Use. International Organization for Standardization, International Electrotechnical Commission, Geneva, 1991.
2. Chamillard AT, Clarke LA Improving the Accuracy of Petri Net-based Analysis of Concurrent Programs, Proceedings of the International Symposium on Software Testing and Analysis, San Diego, 1996..
3. Huget M.-F., Wooldridge M. Model Checking for ACL Compliance Verification, Proceedings of the Second International Joint Conference on Autonomous Agents and Multiagent Systems, 2003.
4. Vaishnavi VK, Fraser MD A Validation Framework for a Maturity Measurement Model for Safety-critical Software Systems, Proceedings of the 36th Annual Southeast Regional Conference, 1998..
5. Kumar S., Li K. Using Model Checking to Debug Device Firmware, ACM SIGOPS Operating Systems Review, 36 (SI), Winter 2002.
6. Baresi L., Heckel R., Thone S., Varro D. Modeling and Validation of Service-oriented Architectures: Application vs. Style, Proceedings of the 9th European Software Engineering Conference, 2003.
7. Aagard MD, Jones RB, Kaivola R., Kohatsu KR, Seger C.-JH Formal Verification of Iterative Algorithms in Microprocessors, Proceedings of the 37th Conference on Design Automation, 2000..
8. Bhargavan K., Obradovic D., Gunter CA Formal Verification of Standards for Distance Vector Routing Protocols, Journal of the ACM, 49 (4), July 2002.
9. Ramalingam G., Warshavsky A., Field J., Goyal D., Sagiv M. Deriving Specialized Program Analyses for Certifying Component-client Conformance, Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2002.

Олександр Аграновський, Борис Телеснін, Вадим Зайцев, Роман Хаді ( [email protected] ) - співробітники ГНУ НДІ «Спецвузавтоматика» (Ростов-на-Дону).

Модельна верифікація в реальному проекті

Для створюваної нашим підприємством системи виявлення та захисту від мережевих комп'ютерних атак були розроблені протоколи взаємодії різних розподілених компонентів: інформаційні зонди, які збирають інформацію про трафік мережі; Пункти збору і обробки інформації, що надходить від зондів; мобільна консоль адміністратора. Запропонований протокол на алгоритмічній рівні було проаналізовано за допомогою BAN-логіки - аналог модельного верифікатори для алгоритмів на мовах високого рівня. Програмна реалізація аналізувалася за допомогою мови PROMELA і інструментального верификатора SPIN (spinroot.com/spin).

За допомогою BAN-логіки була отримана модель, детально описує, хто і якою інформацією володіє при обміні даними між різними компонентами системи. Це дозволило виявити помилки в алгоритмі аутентифікації і методі використання криптографічних засобів захисту інформації. За допомогою мови PROMELA була сформульована Верифікаційна модель алгоритму, яка потім була застосована до реалізації алгоритму взаємодії на мові програмування Сі (компілятор gcc і операційна система FreeBSD 5.0). Це, в свою чергу, дозволило виявити факти «витоку» пам'яті, які приводили до повного останову програми за певних, досить вузьких, вхідних умовах. При цьому використовується рівень абстракції моделі (по суті, підхід MDA) дозволив використовувати результати верифікації на всіх платформах, для яких розроблялося додаток (Windows, FreeBSD, Linux, МСВС).

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