Формальна розробка систем - Студопедія
Цей підхід до створення ПО має багато рис, подібних до каскадної моделі, але побудований на основі формальних математичних перетворень системної специфікації у виконувану програму. Процес створення програмного забезпечення відповідно до цього підходу показаний на рис. 3.3. Тут спрощення не зазначені зворотні зв'язки між етапами процесу.
Мал. 3.3. Модель формальної розробки ПЗ
Між цим підходом та каскадною моделлю існують наступні кардинальні відмінності.
1. Тут специфікація системних вимог має вигляд деталізованої формальної специфікації, записаної за допомогою спеціальної математичної нотації.
2. Процеси проектування, написання програмного коду та тестування системних модулів замінюються процесом, у якому формальна специфікація шляхом послідовних формальних перетворень трансформується у програму, що виконується. Цей процес показано на рис. 3.4.
Мал. 3.4. Процес формальних перетворень
У процесі перетворення формальне математичне уявлення системи послідовно і математично коректно трансформується на програмний код, поступово дедалі деталізованіший. Ці перетворення виконуються доти, доки всі позиції формальної специфікації не будуть трансформовані в еквівалентну програму. Перетворення виконуються математично коректно - тут немає проблеми перевірки відповідності специфікації та програми.
Перевага методу формальних перетворень, що полягає у точній відповідності кінцевої програми специфікації, забезпечується тим, що дистанція між послідовними перетвореннями значно менша за дистанцію між специфікацією та програмою. ДоведенняКоректності програмного коду для великих систем, що масштабуються зазвичай дуже довго, а часто просто не здійснимо. У цьому плані метод формальних перетворень, що з послідовності невеликих формальних кроків, дуже привабливий. Однак вибір для застосування відповідних формальних перетворень складний та неочевидний.
Найбільш відомим прикладом методу формальних перетворень є метод "чистої кімнати" (Cleanroom), розроблений компанією IBM [239, 310, 219, 284]. Цей метод передбачає покрокову розробку, коли кожному кроці застосовується формальні перетворення. Це дозволяє відмовитися від тестування окремих програмних модулів, а тестування всієї системи відбувається після її збирання. Цей підхід докладніше розглянуто у розділі 19.
Як метод " чистої кімнати " , і інші методи формальних перетворень грунтуються на В-методе [348]. Всі ці методи мають кілька "вроджених" недоліків, а вартість розробки програмного забезпечення за допомогою цих методів не набагато відрізняється від вартості розробок іншими методами. Методи формальних перетворень зазвичай застосовують розробки систем, які мають задовольняти суворим вимогам надійності, безвідмовності і безпеки, оскільки вони гарантують відповідність створених систем їх специфікаціям.
Окрім розробки зазначеного типу систем, методи формальних перетворень не знайшли широкого застосування, оскільки потребують спеціальних знань та досвіду використання. Крім того, для більшості систем ці методи не дають суттєвого виграшу у вартості чи якості порівняно з іншими методами розробки програмного забезпечення. Основна причина полягає в тому, що функціонування більшості систем важко піддається опису методом формальних специфікацій, - при створенні більшостіпрограмних систем більшість зусиль розробників йде саме створення специфікацій.
Чи не знайшли те, що шукали? Скористайтеся пошуком: