Процеси перевірки: верифікація та валідація презентация

Содержание

Слайд 1ЛЕКЦІЯ : ПРОЦЕСИ ПЕРЕВІРКИ: ВЕРИФІКАЦІЯ ТА ВАЛІДАЦІЯ
Дишлевий О.П.
NAU

Слайд 2
Загальні ідеї та підходи
Верифікація та валідація
Аксіоматичні перевірки
Інші підходи
Перелік та перспективи
Вівторок, вересень

21, 2010

Якість та тестування програмного забезпечення

Слайд 3Процеси перевірки в життєвому циклі. Верифікація
В архітектурі процесів ЖЦ визначені 4

процеси підтримки які направлені на підвищення якості ПЗ: Верифікація, Валідація, Сумісний перегляд і Аудит.
Виходячи з положення стандарта ISO/IEC 12207 призначення верифікації складається в підтвердженні того, що робочий продукт ПЗ відповідає вимогам в результаті успішної реалізації процеса:
Буде розроблена і впроваджена стратегія верифікації;
Будуть встановлені критерії верифікації всіх необхідних робочих продуктів ПЗ;
Будуть виконуватися належні дії з верифікації;
Буде виконуватися пошук дефектів у робочих продуктах та їх усунення;
Забезпечуватиметься доступ замовника та інших зацікавлених сторін до результатів верифікаційної діяльності ...

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 4Валідація
Призначення процесу валідації полягає в підтвердженні того, що вимоги, що стосуються

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

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 5Спільний перегляд
Призначення процесу спільного перегляду, відповідно до ISO / IEC 12207,

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

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 6Цілі спільного перегляду
Мета періодичних спільних переглядів на рівні управління проектом -

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

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 7Аудит
Призначення процесу аудиту, згідно з ISO / IEC 12207, полягає в

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

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 8Підтримка аудиту
Стандарт визначає робочі продукти і результати діяльності з пропроцесу ЖЦ,

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

Слайд 9Зв'язок і відмінність процесів верифікації та валідації
Верифікація виконується з метою своєчасного

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

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 10Рівні цілісності програмного забезпечення
Рівні цілісності ПЗ системи зв'язуються з діапазоном значень

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

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 11Оцінка вимог до ПЗ
Полягає в аналізі всіх видів вимог з метою

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

Слайд 12Вхідні дані V&V
Опис проекту ПЗ
Потреби користувачів
Стандарти проектування
Звіти про критичність
задач
Звіти про аналіз

загроз
Вихідний код
Плани та графіки розробки
Процедури тестування

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 13Цілі V&V
Аналіз критичності
Аналіз розподілу системних потреб
Аналіз відсліжуваності
Аналіз загроз
Аналіз ризику
Аналіз інтерфейсів
Оцінка документу

опису концепції
Оцінка вимог до ПЗ
Оцінка стану керування налаштуваннями
Створення/верифікація тестування
Аудит інсталяційного налаштування
Пробний запуск
Створення кінцевого звіту

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 14Результати V&V
Звіти про задачі
Звіти про аномілії
Процедури тестування для V&V
Заключний звіт

про V&V

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 15Підтвердження узгодженості вимог до програмного засобу повинно бути засновано на:
Перевірці, чи

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

Слайд 16Підтвердження повноти вимог до програмного засобу повинно бути засновано на:
Перевірці, чи

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

Слайд 17Підтвердження повноти вимог до програмного засобу повинно бути засновано на:
Перевірці, чи

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

Слайд 18Підтвердження точності вимог до програмного засобу повинно бути засновано на…
…перевірці, чи

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

Слайд 19Підтвердження читабельності вимог до програмного засобу повинно бути засновано на:
Перевірці, чи

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

Слайд 20Підтвердження тестопридатності вимог до програмного засобу повинно бути засновано на…
…перевірці наявності

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

Слайд 21 Завдання створення / верифікації плану тестування з метою V & V

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

Слайд 22Завдання верифікації та валідації проекту ПС з низькою критичністю
Цілі V &

V - продемонструвати, що вимоги до ПС коректно, точно і в повному обсязі перетворені в проект, і не запроектовано будь-яких додаткових властивостей програмного засобу, непередбачених вимогами. У ході розгляду документів проекту вирішуються три завдання веріфікації та валідації:
Оцінка проекту програмного засобу,
Створення / верифікація проектів тестів для V & V інтеграції,
Створення / верифікація проектів тестів для V & V системи.

Слайд 23Оцінка проекту програмного засобу
полягає в аналізі коректності, узгодженості, повноти, точності,

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

Слайд 24При верифікації та валідації проекту потрібно оцінити:
Відповідність методів проектування і стандартів

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

Слайд 25Завдання верифікації та валідації реалізації програмного засобу з низькою критичністю
Діяльність по

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

Слайд 26Завдання верифікації та валідації реалізації програмного засобу з низькою критичністю
Оцінка вихідного

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

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

існують об'єктивні критерії приймання кожного компонента вихідного коду і чи можна протестувати код на відповідність цим критеріям.

Слайд 28Завдання верифікації та валідації реалізації програмного засобу з низькою критичністю
Завдання створення

/ верифікації наборів тестів з метою V & V інтеграції виконуються по-різному, залежно від рівня цілісності програмного засобу.
Для програмного засобу з рівнем цілісності 1 або 2 виконання цих завдань полягає в
верифікації відповідності наборів тестів.
Для більш високих рівнів цілісності програмного засобу перевірка наборів тестів, створених розробником, повинна доповнюватися побудовою нових наборів

Слайд 29Завдання верифікації та валідації реалізації програмного засобу з низькою критичністю
Завдання створення

/ верифікації тестових процедур з метою V & V інтеграції (системи) виконуються по-різному, залежно від рівня цілісності програмного засобу.
Для програмного засобу з рівнем цілісності 1 або 2 виконання цих завдань полягає в верифікації відповідності тестових процедур.
Для більш високих рівнів цілісності програмного засобу перевірка тестових процедур, створених розробником, повинна доповнюватися побудовою нових процедур.

Слайд 30Завдання верифікації та валідації випробувань програмного засобу з низькою критичністю
Суть у

підтвердженні результатів виконання інтеграційного, системного та приймального тестування (для рівнів цілісності 1 і 2) або виконання додаткового тестування (для рівнів цілісності 3 та 4). Включає вирішення двох завдань:
Виконання / верифікація тестів для V & V інтеграції;
Виконання / верифікація тестів для V & V системи.
Вихідними продуктами для виконання V & V випробувань є плани і процедури для тестування інтеграції (системи), а також вихідний і виконуваний код програмного засобу.

Слайд 31Управління верифікацією та валідацією
Управління діями по V & V при виконанні

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

Слайд 32Завдання управління верифікацією та валідацією
До завдань управління V & V входить

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

Слайд 33Завдання управління верифікацією та валідацією
В ході управління V & V:
Оцінюється кожне

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

Слайд 34Дії по V & V можуть виконуватися тільки:

розробниками, рівними в правах,


групою розробки (менеджерами та розробниками),
групою якості, спільно представниками замовника і розробника,
тільки замовником або незалежними експертами.

Слайд 35 Процеси V & V, що виконуються організацією (підрозділом), що має певний

рівень технічної, адміністративної чи фінансової незалежності від організації-розробника (підрозділу-розробника), називають незалежною верифікацією та валідацією (IV & V, Independent V & V), а таку організацію (підрозділ) - органом (групою ) IV & V.
IV & V доцільно застосовувати до великих дорогих проектів або проектам критичних з безпеки функціонування систем (safety critical system) для досягнення об'єктивності перевірок і зниження ризику розробки.

Слайд 36Види незалежності групи IV&V:
Технічна незалежність групи IV & V полягає в

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

Слайд 37Структура та зміст плану верифікації та валідації
У плані SVVP фіксується інформація,

необхідна для управління та виконання процесів, дій і завдань по V & V в ході ЖЦ програмного засобу.
Якщо по якомусь з пунктів плану інформація не надається, це повинно вказуватися фразою «дана тема не охоплюється планом» мати обґрунтування. В план можуть бути додані й інші пункти.

Слайд 38План верифікації та валідації програмного засобу
1. Призначення
2. Посилання
3. Визначення
4. Організація роботи

з V & V
4.1. Організація
4.2. Графік робіт
4.3. Схема призначення рівнів цілісності ПО
4.4. Розподіл ресурсів
4.5. Відповідальності
4.6. Інструменти, методології та методи

Слайд 395. Процеси і дії з V & V
5.1. Процес: Управління
5.1.1. Дія:

Управління V & V
5.2. Процес: Придбання
5.2.1. Дія: V & V підтримки придбання
5.3. Процес: Постачання
5.3.1. Дія: V & V планування
5.4. Процес: Розробки
5.4.1. Дія: V & V Концепції
5.4.2. Дія: V & V Вимог
5.4.3. Дія: V & V Проекту
5.4.4. Дія: V & V Реалізації
5.4.5. Дія: V & V Випробувань
5.4.6. Дія: V & V Введення в дію
5.5. Процес: Експлуатація
5.5.1. Дія: V & V Експлуатації
5.6. Процес: Супровід
5.6.1. Дія: V & V Супроводження

Слайд 406. Вимоги до звітних документів V & V
7. Вимоги до адміністративних

процедур
7.1. Реєстрація та прийняття рішень по аномалії
7.2. Політика ітерації завдань
7.3. Регулювання відхилень від плану
7.4. процедури контролю
7.5. Стандарти практичні інструкції та угоди
8. Вимоги до документування V & V

Слайд 41Організація роботи з V & V. У цьому розділі повинні бути

описані:

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

Слайд 42узгоджена схема рівнів цілісності ПЗ. Рівні цілісності повинні бути призначені окремим

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

Слайд 43організаційна структура колективу, що виконує V & V, із зазначенням сфери

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

Слайд 44Процеси і дії з V & V. Кожній дії процесу V

& V потрібно описати:

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

Слайд 45Вимоги до звітних документів V & V.
У цьому розділі зазначаються

види, структура і зміст обов'язкових звітів по V & V.

Слайд 46Вимоги до адміністративних процедур.
У цьому розділі встановлюються вимоги по наступних

аспектах адміністративної підтримки V & V:
складання звітів і прийняття рішень по аномаліям;
повторне виконання завдання V & V;
оформлення відхилень від плану;
процедури контролю;
стандарти, практичні рекомендації та угоди.

Слайд 47Вимоги до документування V & V
У цьому розділі зазначаються призначення ,

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

Слайд 48Звіти з верифікації та валідації
Результати виконання дій і задач V

& V документуються у зведеному звіті про V & V, який може включати:
звіт про завдання V & V;
підсумковий звіт про дію за V & V будь-якого з основних процесів ЖЦ;
звіт про аномалії;
заключний звіт про V & V.

Слайд 49Альтернативи ЗЯ
Дефекти та ЗЯ
Дефект: помилка/відмова/збій.
Попередження / видалення / стримування дефектів.
Схема основних

видів ЗЯ.
Профілактика дефектів: видалення джерел та блокування помилок
Видалення дефектів: контроль / тестування / т.д.
Стримування дефектів: відмовостійкість і стримування відмов(забезпечення безпеки)
Особливий випадок: формальні перевірки (та формальні специфікації)


Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 50ЗЯ та формальні перевірки (ФП)
Формальні методи = формальні специфікації + формальні

перевірки
Формальні специфікації (ФС):
Як частина запобігання дефектів
Формальні запобігання/скорочення дефекту вкладання через неточності,двозначності і т.д.
Менш покриті по відношенню
до ФП
Формальні перевірки(ФП):
Частина ЗЯ, але базується на
позитивних аспектах: “Доведення
відсутність відмов”
Інтенсивність роботи людей
Деякі часто використовувані
підходи

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 51Формальні специфікації: Ідеї
Формальна специфікація:
Зосереджена на коректності
Різні рівні деталізації
Характеристики (3С): повна, якісна,

послідовна
Два типи: описова та поведінкова
Описові ФС:
Логічні: перед/після умови
Математичні функції
Позначення та мовна підтримка
Поведінкові ФС: FSM, мережі петрі, і т.д.

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 52Формальні специфікації: Ідеї
“Тестування показує наявність помилок, а не їх відсутність” –

Дейкстра
ФП: доказ конкретності
ФС: як пре/пост умови
Аксіоми для компонентів або формальних блоків
Склад
Розробка та перевірка разом
Інші схожі підходи
Напів-формальні перевірки
Перевірка моделей
Інспекція на коректність

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 53Основи ФП
Основні підходи
Аксіоматичний підхід Флойд /Хоар
Дейкстра /Гріес з слабкими передумовами. (СП)
Обчислювальний/функціональний

підхід Мілса
Базис перевірок
Логічні (аксіоматичні і СП)
Математичні функції (Міллс)
Інші формалізми
Використовувані процедури/дії
Аксіоматичні
Зворотного виводу (СП)
Попереднє складення (Міллс), і т.д.

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 54Об’єктний та загальний підхід
Основна частина: вирази
Блок (початок/кінець)
Конкатенація
Умовні (if-then/if-then-else)
Цикл (while)
Призначення
ФП
Правила для більших

частин
Складання
Зв’язувачі (логічні наслідки)

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 55Аксіоматичний підхід
аксіоми/блок-схеми Флойда
Примітка на блок-схемі
Логічні відносини
Перевірка використовуваної логіки
аксіоми/формалізація Хоара
Перед/пост-умови
Склад
Цикли і функції/параметри
Інваріанти

(цикли, функції)
Основа для багатьох пізніших підходів

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 56Аксіоматична правильність
Позначення
Заяви: Si
Логічні умови: {P} і т.д.
Схема: {P} S {Q}
Аксіоми /

правила: умови або схеми / висновок
Аксіоми:
Схема для призначення
Основні типи виразів
“З’єднання”
Циклові інваріанти

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 57Аксіоматичний підхід: формальні характеристики
ФС:
Логічного (описового) типу.
Перед/пост-умови
Пара, як специфікації на різних рівнях

деталізації
Приклади специфікації на різних для сегменту:
Змінні вводу/виводу: x,y
Перед/пост-умови: P, Q
Передумови: невід’ємний вхід
Постумова: обчислюється квадратний корінь

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 58Аксіоматичний підхід: Правила виводу
Правила виводу: Послідовність аксіом
Логічні наслідки та висновки.
Гнучкість

для різних пре/пост-умов.
Наслідок 1: послаблені пост-умови
Аксіома А1:
Наслідок 2: більш суворі передумови
Аксіома А2:
У порівнянні з СП

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 59Аксіоматичний підхід: Аксіоми
Схема призначення:
Аксіома А3:
Де виходить з P з усіма вільними входженнями

у заміненого х.
Приклад: з
Пост-умова (підтримання невід'ємного балансу)
Передумова чи
Аксіома 4. Послідовне обєднання:

Використовується для побудови доказів знизу догори

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 60Аксіоматичний підхід: Аксіоми
Умовні аксіоми
Умова 1,if-then-else (Аксіома 5):

Умова 2, пустий else (Аксіома

6):

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 61Аксіоматичний підхід: Аксіоми
Тип циклу: while умова do щось
Аксіома циклу

Спеціалізовані методи для

циклів:
Інваріанта циклу: P (часто називають I)
Як вибрати інваріанта циклу?
Доказ основних циклів: Аксіома А7.
Цикл припинення перевірки
P позитивне в циклі

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 62Аксіоматичні докази
Дано: програма, перед/пост-умови
Базова процедура доказу:
Додати анотації між заявами
Застосовувати аксіоми окремих

заяв використовуючи схеми при значення (A3)
Проста композиція (об’єднання, А4)
Наслідок правил (А1 та А2) як з’єднувачі змішані з вищевказаними
Більш складна композиція:
if-then-else (A5) and if-then (A6)
Аксіома циклу (А7): часто в центрі уваги

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 63Аксіоматичні докази
Базовий доказ фокусується на наступному:
Припиненні циклу та інваріантах
З'єднанні (знизу-вгору)
Використання ієрархічної

(ступенева абстракція) структури в якості керівництва для різних частин (згори-вниз керівництво знизу-вгору процедури)


Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 64Приклад аксіоматичного доказу
Факторіал функції
Приклад аксіоматичного доказу
Передумови:
Постумови:
Вівторок, вересень 21, 2010
Якість

та тестування програмного забезпечення

Слайд 65Приклад аксіоматичного доказу
Ключ доказу: цикл; інші кроки досить прості
Розвиток циклу інваріанту

І:
має часткові результати
З'єднання з умовою циклу
Результат у постумові після циклу:
Спостереження за прикладом доказу: доказ значно довший ніж сама програма

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 66Аксіоматичні докази
Загальні спостереження:
Включає багато кроків
Довжина доказу: на порядок довше ніж програма
Складності

з циклами
Великі/складніші програми:
Багато елементів та (вкладених!) циклів
взаємодії, координації
Масиви та функції/процедури
більш складні схеми/аксіоми
Значно важче
Вибіркова перевірка ідей?

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 67Підхід найслабших передумов (WP)
Підхід Дейкстра/Грайза:
Слабкі передумови:
Модель Дейкстра: Перетворюється предикат
Книга Грайза

“Science of Programming”
Схожий на аксіоматичний підхід:
Основна логіка як у анотаціях
Схожий блок (аксіоми)
інтерпретується як
Відмінність процедур:
Початок з постумов (вихідні дані)
Зворотнє виведення WP

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 68Функціональний підхід
Функціональний підхід
Програма обчислення Мілса
Символічне виконання широко використовується
Ідеї читання/відриву/пізнання коду
Елементи функціонального

підходу
Нотації Мілса
Основні функції, пов'язані з окремими заявами
Композиційні правила
Наступне покрокове/символічне виконання
Порівнянння з Дейкстровою WP

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 69Функціональний підхід: символічне виконання
Символічне виконання для:

Trace 1:


Trace 2:


Обидва залишки використовуються при

перевірці
Деталі у Мілсі (1987а)

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 70Формальна перевірка: Недоліки
Сім міфів (Зелковиц, 1993):
FM гарантує що ПО є бездоганним
Вони

працюють, довівши правильність
Тільки дуже критичні переваги системи
FM повязано зі складними математиками
FM збільшує вартість розробки
Вони є незрозумілими для клієнта
Ніхто не використовує їх для реальних проектів
Спростування дискусія (Зелковиц, 1993)
Проте деякі кількісні дії альтернативні FV методам

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 71Інші моделі/підходи
Виробництво FV більш легке/ширше для використання
Інші моделі для формальної перевірки:
Установка

машин та перевірка моделей
Алгебраїчні дані специфікації/перевірки
Мережі Петрі
Зв’язок перевірених/підтверджених процедур
Загальне судження
Розширення для FM раніше
Додаткові переваги та зниження обмежень
Може призвести до додаткової автоматизації
Гібридні методи
Адаптація та напів формальні методи

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 72Формальна перевірка: Інше
Алгебраїчна специфікація/перевірка:
Вкажіть і перевірте властивості даних
Поведінка специфікації
Базовий варіант
Конструкції
Домен/поведінка відображення
Використання

у перевірці
Приклади стеку
Newstack
Push
Pop
Canonical form

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 73Формальна перевірка: Інше
Модель перевірки:
Поведінкова специфікація через FSM
Пропозиція: власність інтересу проявляється в

якості підходящої формули.
Перевірювач: перевірка обгрунтованої пропозиції алгоритма/програми
Твердження: результат позитивний
Контрприклад: результат негативний
Інші підходи та обговорення:
Алгоритм аналізу
Моделювання та аналіз мереж Петрі
Табличний/напівформальний метод
Основні формальні інспекції
Обмеження аспектів – легше виконання

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 74FM: Застосування
Що може бути формально перевірене:
Програмний код
Формальний дизайн, документація, та інше
Протоколи:

тимчасові властивості – тупик(deadlock)/голод(starvation)
Апаратна перевірка
Розподілена програмна перевірка
Підключення до ПЗ процесу
Покрокове уточнення/перевірка процесу:
Дизайн та перевірка водночас
Різні рівні абстракції
Напр., UNITY система

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 75Використання у безпеці ПЗ
Leveson підхід
Орієнтована перевірка
Рухомий аналіз небезпеки
Розподілені по фазам розвитку
Яке

FM? Необхідне
Інші використання:
Чисте приміщення: поєднані зі статичними випробуваннями
Yih/Tian: PSC

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 76Формальна перевірка: Підсумки
Основні особливості:
Аксіоми/правила для всіх мовних особливостей
Ігнорувати деякі практичні питання:
Розмір,

ємність, побічні ефекти і т.д.
Вперед/назазнизу-вверх процедури
Розробка інваріантів: ключ, але важкий
Загальна оцінка:
Важно, навіть на великих програмах
Дуже важко масштабувати
Невідповідна до математичних задач
Важко автоматизувати
Ручний процес – помилки
Варте для критичного застосування
Порівняння з іншими QA

Вівторок, вересень 21, 2010

Якість та тестування програмного забезпечення

Слайд 77Запитання?
Вівторок, вересень 21, 2010
Якість та тестування програмного забезпечення

Похожие презентации

Обеспечение защиты информации в ходе эксплуатации аттестованной информационной системы 291
Устройство компьютера и его функции 369
Перспективное пользовательское программное обеспечение 325
Характеристики модуляции сигналов оптического диапазона (лекция 19) 284
Электронный документооборот 257
Архитектура ЭВМ и язык ассемблера. Лекция 3 330

Обратная связь

Если не удалось найти и скачать презентацию, Вы можете заказать его на нашем сайте. Мы постараемся найти нужный Вам материал и отправим по электронной почте. Не стесняйтесь обращаться к нам, если у вас возникли вопросы или пожелания:

Email: Нажмите что бы посмотреть 

Что такое ThePresentation.ru?

Это сайт презентаций, докладов, проектов, шаблонов в формате PowerPoint. Мы помогаем школьникам, студентам, учителям, преподавателям хранить и обмениваться учебными материалами с другими пользователями.

Для правообладателей

Яндекс.Метрика