Разработка на формални системи - Студопедия
Този подход към разработването на софтуер има много функции, подобни на модела на водопада, но е изграден на базата на формални математически трансформации на системна спецификация в изпълнима програма. Процесът на създаване на софтуер в съответствие с този подход е показан на фиг. 3.3. Тук, за простота, обратните връзки между стъпките на процеса не са посочени.
Фиг. 3.3. Официален модел за разработка на софтуер
Съществуват следните кардинални разлики между този подход и модела на водопада.
1. Тук спецификацията на системните изисквания има формата на подробна формална спецификация, написана с помощта на специална математическа нотация.
2. Процесите на проектиране, писане на програмен код и тестване на системни модули се заменят с процес, при който формалната спецификация се трансформира в изпълнима програма чрез последователни формални трансформации. Този процес е показан на фиг. 3.4.
Фиг. 3.4. Процес на формални трансформации
В процеса на трансформация, формалното математическо представяне на системата последователно и математически правилно се трансформира в програмен код, постепенно все по-подробен. Тези трансформации се извършват, докато всички позиции на формалната спецификация се трансформират в еквивалентна програма. Трансформациите се извършват математически правилно - няма проблем да се провери съответствието на спецификацията и програмата.
Предимството на формалния метод на трансформация, което се състои в точното съответствие на крайната програма със спецификацията, се осигурява от факта, че разстоянието между последователните трансформации е много по-малко от разстоянието между спецификацията и програмата. Доказателствокоректността на програмния код за големи мащабируеми системи обикновено отнема много време и често просто не е осъществимо. В това отношение методът на формалните трансформации, който се състои от последователност от малки формални стъпки, е много привлекателен. Изборът за прилагане на подходящите формални трансформации обаче е сложен и неочевиден.
Най-известният пример за формалния метод на трансформация е методът Cleanroom, разработен от IBM [239, 310, 219, 284]. Този метод включва разработка на софтуер стъпка по стъпка, когато на всяка стъпка се прилагат формални трансформации. Това ви позволява да откажете да тествате отделни софтуерни модули и тестването на цялата система става след нейното сглобяване. Този подход е разгледан по-подробно в Глава 19.
Както методът "чиста стая", така и други методи за формална трансформация се основават на В-метода [348]. Всички тези методи имат няколко "присъщи" недостатъка и разходите за разработване на софтуер с помощта на тези методи не се различават много от разходите за разработване на софтуер с помощта на други методи. Формалните методи на трансформация обикновено се използват за проектиране на системи, които трябва да отговарят на строги изисквания за надеждност, надеждност и безопасност, тъй като те гарантират, че получените системи отговарят на техните спецификации.
В допълнение към разработването на този тип системи, методите на формалните трансформации не са намерили широко приложение, тъй като изискват специални знания и опит за използване. В допълнение, за повечето системи тези методи не осигуряват значително предимство в цената или качеството пред други методи за разработка на софтуер. Основната причина е, че функционирането на повечето системи е трудно да се опише с помощта на формални спецификации - при създаването на повечетоВ софтуерните системи по-голямата част от усилията на разработчиците отиват в създаването на спецификации.
Не намерихте това, което търсихте? Използвайте търсачката: