К. М. Лавріщева програмна інженерія підручник Київ, 2008
 Скачать 5.23 Mb.
|
|
6.2.2. Модель доведення програми за твердженнями Розглядається формальне доведення програми, заданої структурною логічною схемою і сукупністю тверджень, що описуються логічними операторами, комбінаціями змінних (true/false), операціями (кон’юнкція, диз'юнкція й ін.) і кванторами загальності й існування (табл.6.1). Таблиця 6.1. Список логічних операцій Логічна операція Назва Приклад Значення Кон’юнкція x & y x і y Диз’юнкція x * y x або y Суперечність x ні x Імплікація x y якщо х то у Еквівалентність х = у Х рівнозначно у Квантор загальності х Р(х) для всіх х, умова істинно Квантор існування х Р(х) Існує х, для якого Р(х) істина Розділ 6 157 Мета алгоритму програми – побудова для масиву цілих чисел Т довжини N (array Т[1:N])еквівалентного масиву Т’ тієї ж довжини N, що і масив Т. Елементи в масиві Т’ повинні розташовуватися в порядку зростання їхніх значень. Даний алгоритм реалізується сортуванням елементів вихідного масиву Т за їхнім зростанням. Доведення правильності алгоритму сортування елементів масиву Т (рис. 6.2) проводиться з використанням ряду тверджень про елементи цього алгоритму, якій описуються пунктами П1– П6. M = t r u e I = I + 1 I = 0 З м ін и т и T ’( i+ 1 ) н а T ’( i) T = T ’ M = tr u e M = t r u e 0 A b e g Н і ¬ M = t r u e A e n d I < N T ’( i) > T ’( + 1 ) * * * Н і Н і Рис.6.2. Схема сортування елементів масиву Т' П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) ). Розташування елементів масиву Т в порядку зростання їхніх величин у масиві Т’ здійснюється алгоритмом бульбашкового сортування, суть якого полягає в попередньому копіюванні масиву Т з масиву Т', а потім проводиться сортування елементів згідно з умовою їхнього зростання. У кружках також дано: початковий стан – 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). Отже, виконання вихідних умов забезпечене порядком і відповідною семантикою операторів перестановки масиву. Розділ 6 159 Доведено, що виконання алгоритму програми завершено успішно, це означає її правильність. П3. Цей алгоритм можна подати у вигляді серії теорем, що доводяться. Починаючи з першого твердження і переходячи від одного перетворення до іншого, визначаємо індуктивний шлях висновку. Якщо одне твердження є правильним, то істинним є й інше. Іншими словами, якщо дано перше твердження А 1 і перша точка перетворення А 2, то перша теорема – А 1 А 2 . Якщо А 3 – наступна точка перетворення, то другою теоремою буде А 2 А 3 Інакше кажучи, формулюється загальна теорема А і А j , де А і й А j – суміжні точки перетворення. Ця теорема формулюється так: якщо умова істинна в останній точці, то і вихідне твердження А k А end є істинним. Тобто, можна повернутися до точки перетворення А end і до попередньої точки перетворення. Якщо доведемо, що А k А end справджується, то виходить, що справджується й А j А j+1 , і так далі, поки не одержимо, що А 1 А 0. П4. Далі специфікується твердження типу if – then. П5. Щоб довести, що програма коректна, необхідно послідовно розташувати усі твердження, починаючи з А 1 і закінчуючи А end , цим буде підтверджено істинність вхідної і вихідної умов. П6. Доведення алгоритму програми завершено. 6.3. Верифікація і валідація програм Верифікація і валідація – це методи аналізу, перевірки специфікацій і правильності виконання програм відповідно до заданих вимог і формального опису програми [18–21]. Метод верифікації допомагає зробити висновок про коректність створеної програмної системи при її проектуванні і після завершення її розроблення. Валідація дозволяє встановити здійснимість заданих вимог шляхом їх перегляду, інспекції і оцінки результатів проектування на процесах ЖЦ для підтвердження того, що здійснюється коректна реалізація вимог, дотримання заданих умов і обмежень до системи. Верифікація і валідація забезпечують перевірку повноти, несуперечності і однозначності специфікації і правильності виконання функцій системи. Верифікації і валідації піддаються: – компоненти системи, їх інтерфейси (програмні, технічні і інформаційні) і взаємодія об'єктів (протоколи, повідомлення) у розподілених середовищах; – описи доступу до баз даних, засоби захисту від несанкціонованого доступу до даних різних користувачів; – документація до системи; – тести, тестові процедури і вхідні набори даних. Верифікація і валідація як методи перевірки правильності виконання заданих функцій і відповідності їх вимогам замовника подані в стандарті [7-9] у вигляді самостійних процесів ЖЦ і використовуються, починаючи від етапу аналізу вимог і закінчуючи перевіркою правильності функціонування програмного коду на заключному процесі, а саме, під час тестування. Для цих процесів визначені цілі, задачі і дії з перевірки правильності створюваного проміжного продукту на процесах ЖЦ. Розглянемо їхнє стандартне подання. Процес верифікації. Мета процесу – переконатися, що кожен програмний продукт (і/або сервіс) проекту відбиває погоджені вимоги до їхньої реалізації. Цей процес ґрунтується: – на стратегії і критеріях верифікації всіх робочих програмних продуктів на ЖЦ; – на виконанні дій з верифікації відповідно до стандарту; – на усуненні недоліків, виявлених у програмних (робочих, проміжних і кінцевих) продуктах; – на узгодженні результатів верифікації з замовником. Процес верифікації може проводитися виконавцем програми або іншим співробітником тієї ж організації, або співробітником іншої організації, наприклад представником замовника. Цей процес містить у собі дії з його впровадження і виконання. Впровадження процесу полягає у визначенні критичних елементів (процесів і програмних продуктів), що повинні піддаватися верифікації, у виборі виконавця верифікації, інструментальних засобів підтримки процесу верифікації, у складанні плану верифікації і його затвердження. У процесі верифікації виконуються задачі перевірки умов: контракту, процесу, вимог, інтеграції, коду і документації. Відповідно до плану і вимог замовника перевіряється правильність виконання функцій системи, інтерфейсів і взаємозв'язків компонентів, а також доступ до даних і до засобів захисту. Процес валідації. Мета процесу – переконатися, що специфічні вимоги для програмного продукту виконано, і здійснюється це за допомогою: – розробленої стратегії і критеріїв перевірки всіх робочих продуктів; – обговорених дій з проведення валідації; – демонстрації відповідності розроблених програмних продуктів вимогам замовника і правилам їхнього використання; – узгодження із замовником отриманих результатів валідації продукту. Процес валідації може проводитися самим виконавцем або іншою особою, наприклад, замовником, що здійснює дії з впровадженню і проведенню цього процесу за планом, у якому відбиті елементи і задачі перевірки. При цьому використовуються методи, інструментальні засоби і процедури виконання задач процесу для встановлення відповідності тестових вимог і особливостей використання програмних продуктів проекту на правильність реалізації вимог. На інших процесах ЖЦ виконуються додаткові дії: – перевірка і контроль проектних рішень за допомогою методик і процедур перегляду ходу розроблення; – звернення до CASE-систем [10], що містять у собі процедури перевірки вимог до продукту; – перегляди й інспекції проміжних результатів на відповідність вимогам для підтвердження того, що ПС має коректну реалізацію вимог і задовольняє умови виконання системи. Таким чином, основні задачі процесів верифікації і валідації полягають у тому, щоб перевірити і підтвердити, що кінцевий програмний продукт відповідає призначенню і задовольняє вимогам замовника. Ці процеси взаємозалежні і визначаються, як правило, одним загальним терміном «верифікація і валідація» або «Verification and Validation» (V&V) [19]. Розділ 6 161 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]. Метод перевірки полягає в редукції системи з нескінченним числом станів до системи із скінченного числа станів, а також у доведенні коректності розподіленого Розділ 6 163 застосування за допомогою індуктивних міркувань і системи переходів скінченного автомата. Основні підходи до верифікації – аксіоматичний і семантичний шлях Model Сhecking. Аксіоматичний (за методом Нoare) підхід міститься в описі програми набором аксіом для завдання станів з використанням теорія логіки. Семантичний підхід ґрунтується на теорії темпоральної логіки Манна для завдання специфікації програм. Аксіоми використовуються для керування семантикою мови специфікації. Основними типами даних специфікації в SDL є наперед визначені і сконструйовані типи даних (масив, послідовність і т.д.). У мові описуються формули за допомогою предикатів, булевих операцій, кванторів, змінних і модальностей. Семантика їх визначення залежить від можливих послідовностей дій (поведінки), що виконуються специфікацією процесу, а також моменту часу його виконання. Схема специфікації процесу – це опис умов виконання і діаграм процесів. Вона ініціюється посиланням повідомлення із зовнішнього середовища для виконання. Діаграма процесу складається з описів переходів, станів, набору операцій процесу і переходу до наступного стану. Кожна операція визначає поведінку процесу і спричиняє деяку подію. Логічна формула задає модальність поведінки специфікації і моменти часу. Процес, наданий формальною специфікацією, виконується не детерміновано. Обмін із зовнішнім середовищем відбувається через вхідні і вихідні параметри повідомлень. Подія. У кожний момент часу виконання процес має деякий стан, який може бути поданий у вигляді знімка, що характеризує деяку подію, яка містить у собі значення змінних, яким відповідають параметри і характеристики станів процесу. Таким чином, модель перевірки, набір аксіом мовою логіки і твердження про виконання розподілених програм забезпечують процес їхньої верифікації. |