logo
ТППС / Магистры / ТППС-лаб

Лабораторна робота № 4

Тема: Формальні специфікації ПЗ

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

Короткі теоретичні відомості:

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

Термін “формальні методи” має на увазі ряд операцій, до складу яких входять створення формальної специфікації системи, аналіз і доказ специфікації, реалізація системи на основі перетворення формальної специфікації в програми і верифікація програм. Усі ці дії залежать від формальної специфікації програмного забезпечення. Формальна специфікація ‒ це системна специфікація, записана мовою, словник, синтаксис і семантика якого визначені формально. Необхідність формального визначення мови передбачає, що ця мова ґрунтується на математичних концепціях. Тут використовується область математики, яка називається дискретною математикою і ґрунтується на алгебрі, теорії множин і алгебрі логіки.

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

Тепер ясно, що ці пророкування не збулися, причому із цілого ряду причин.

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

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

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

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

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

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

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

Метод “чистої кімнати” розробки ПЗ, ґрунтується на формальних доказах того, що програма відповідає своїй специфікації.