Transcript
Tema 3 Formalne specifikacije i metode u softverskom inženjerstvu dr Vladislav Miškovic Fakultet za računarstvo i informatiku PROJEKTOVANJE INFORMACIONIH SISTEMA 2016/2017 Sadržaj predavanja 1. Uvod 2. Formalne specifikacije i metodi 3. Modeliranje sistema 4. Standard UML 5. UML dijagrami analize 6. Analiza i RUP 7. Primeri 2 1. Uvod Proces razvoja softverskog proizvoda podrazumeva izradu detaljnih specifikacija, različite analize, dokazivanje korektnosti, transformacije i verifikaciju softverskog proizvoda Strogi matematički metodi u razvoju softvera nisu rasprostranjeni u praksi zbog složenosti metoda dugog vremena razvoja ograničene primenjivosti metoda, npr. ne obuhvataju interfejse i koriste se za manje sisteme Primena matematičkih metoda je posebno važna u razvoju kritičnih sistema (npr. ugrađenih, embeeded), od kojih se očekuje pouzdanost i bezbednost 3 Ilustracija: Formalna verifikacija kritičnih sistema Jezik SPARK 2014 je formalni jezik, razvijen na osnovu programskog jezika Ada 2012, radi uklanjanja potencijalnih dvosmislenosti i veće bezbednosti ugrađenih sistema Koristi se za razvoj bezbednosno kritičnih sistema, kao što su komercijalni i vojni avioni, sistemi upravljanja avio i željezničkim saobraćajem, medicinske i kosmičke primene Jezik omogućava verifikaciju programa formalnim metodima i smanjivanje ili izbegavanje klasičnog testiranja softvera, koje može da ošteti skupe sisteme u koje se ugrađuje https://youtu.be/plxbobx7lus Verifikacija softvera drona 4 Primer 1: Dokazivanje korektnosti Proizvod je korektan ako zadovoljava postavljene izlazne specifikacije (resursi, uslovi) Testiranje programa (manuelno) Matematički postupak dokazivanja Ilustracija: matematički postupak dokazivanja korektnosti malog segmenta koda: intk, s; inty[n]; k =0; s =0; while(k n){ s =s +y[k]; k =k +1; } 5 Primer 2: Automatizovano dokazivanje korektnosti programa Eksperimentalni sistem Dafny (Microsoft Research) kopiranje koda u editor pokretanje verifikacije dijagnostika 6 Izrada specifikacija u razvoju informacionih sistema Klasične faze razvoja informacionih sistema 1. Definisanje zahteva (Requirements) 2. Analiza (Analysis) 3. Izrada specifikacija (Specification) 4. Projektovanje (Design) 5. Implementacija (Implementation) 6. Testiranje (Testing) 7. Isporuka/uvođenje (Deployment) 8. Održavanje (Maintenance) Izrada specifikacija je rezultat definisanja i analize zahteva Prethodi projektovanju 7 Definisanje problema i sistemskih zahteva Definisanje problema je prvi korak razvoja softvera 1. Identifikacija problema 2. Analiza izvedivosti (operativna, tehnička, vremenska, ekonomska) 3. Analiza isplativosti - cena i efekti primene (cost-benefit) 4. Predlog sistema Strukturiranje sistemskih zahteva Modeliranje procesa/podataka Analitički UML dijagrami klasičan pristup (UseCase) objektno orijentisani pristup (više analitičkih UML dijagrama) 8 Specifikacija Projektni zahtev Rezultat analize je specifikacija korisničkih zahteva (Software Requirements Specification, SRS) oblik i struktura dokumenta prema standardu inženjerstva zahteva ISO/IEC/IEEE (Systems and software engineering - Requirements engineering) koristiće se naziv projektni zahtev za izradu softvera ili kraće projektni zahtev (PZ) 9 1. Uvod Sadržaj projektnog zahteva (SRS) definisan je ISO/IEC/IEEE standardom 1.1 Cilj razvoja 1.2 Obim sistema 1.3 Prikaz proizvoda Perspektiva proizvoda Funkcije proizvoda Karakteristike korisnika Ograničenja 1.4 Definicije 3. Specifikacija zahteva 3.1 Spoljašnji interfejsi 3.2 Funkcije 3.3 Pogodnost za upotrebu 3.4 Zahtevane performanse 3.5 Zahtevi baze podataka 3.6 Projektna ograničenja 3.7 Sistemske karakteristike softvera 3.8 Dopunske informacije 2. Reference 4. Verifikacija (po tezama tačke 3) 5. Prilozi 5.1 Pretpostavke i zavisnosti 5.2 Akronimi i skraćenice 10 2. Formalne specifikacije i metodi 1. Projektni zahtevi i specifikacije 2. Formalne specifikacije i metodi u procesu razvoja softvera 11 2.1 Projektni zahtevi i specifikacije Specifikacija projektnih zahteva se definiše u početnoj fazi procesa razvoja softvera Funkcionalni zahtevi (funkcije proizvoda) opis funkcija sistema - ulazi i odgovarajući izlazi, opis ponašanja Nefunkcionalni zahtevi (ograničenja) ograničenja funkcionisanja sistema - vreme odziva, nivo pouzdanosti, upotreba resursa, standardi) 12 Faze izrade specifikacija softvera 1. Studija izvodljivosti 2. Otkrivanje i analiza zahteva 3. Definisanje korisničkih i sistemskih zahteva 4. Validacija zahteva (ostvarivost, konzistentnost, potpunost) Povećanje uticaja ugovarača Smanjenje uticaja klijenta Definisanje korisničkih zahteva Specifikacija sistemskih zahteva Projektovanje arhitekture Formalna specifikacija Projekt (visokog nivoa) Izrada specifikacija Projektovanje 13 Proces razvoja softvera i formalne specifikacije Izrada formalnih specifikacija se može realizovati paralelno sa projektovanjem Definisanje korisničkih zahteva Specifikacija sistemskih zahteva Formalna specifikacija Projekt (visokog nivoa) Modeliranje sistema Projektovanje arhitekture 14 Uloga specifikacija u razvoju softvera Utiču na cenu razvoja softvera (Sommerville) povećava se cena izrade specifikacija smanjuje se broj grešaka, pa je niža cena projektovanja, implementacije i validacije sistema (posebno za kritične sisteme) Cena Projekt. i implem. Validacija Specifikacija Specifikacija Projekt. i implem. Validacija Grube specifikacije Detaljne specifikacije 15 Jezici izrade specifikacija softvera Neformalni prirodni jezik (izražajan, lako se uči, ali je neprecizan) Poluformalni delimično formalizovani, ne omogućavaju dokazivanje korektnosti Primeri: dijagrami toka (flowchart), IDEF, UML Formalni precizno definisana semantika mehanizmi apstrakcije, analize, modularizacije i višestruke upotrebe koriste se pretežno za bezbednosno kritične sisteme Primeri: propoziciona i predikatna logika, Z, Alloy, SPARK 16 2.2 Formalne specifikacije i metodi u procesu razvoja softvera Formalni metodi su skup tehnika zasnovanih na matematičkom predstavljanju i analizi softvera Verifikcija - potvrda da softver zadovoljava specifikacije Validacija - potvrda da implementirani sistem odgovara očekivanjima budućeg korisnika Formalni metodi uključuju Formalne specifikacije sistema Analize specifikacija i dokazivanje Transformacioni razvoj Verifikaciju programa Utiču na smanjenje broja grešaka u sistemu 17 Proces razvoja softvera korišćenjem formalnih metoda Narativna specifikacija softvera Funkcionalno testiranje Formalni opis u B Formalni dizajn Integracija softvera Generisanje softvera (automatsko) 18 Formalne specifikacije sistema Algebarske specifikacije Sistem se opisuje operacijama i njihovim relacijama Primeri: Larch, CASL, OBJ, Maude Specifikacije zasnovane na modelu Sistem se opisuje stanjima modela, koji se zasniva na matematičkim konstrukcijama, kao što su npr. skupovi i nizovi (sequences) operacije predstavljaju promene stanja sistema Primeri: Z, B, Petri Nets 19 Primeri formalnih specifikacija Propoziciona i predikatna logika Prednosti: izražajna, formalna, teorijski zasnovana Nedostaci: nema mehanizama modularizacije; predikatna logika je neodlučiva (Gödel) Jezik formalnih specifikacija Z (Zed) akademski jezik, koji ima i softversku podršku (alate) nazvan po nemačkom matematičaru Ernstu Zermelu Z = tipizovana predikatna logika 1. reda + teorija skupova + sheme 20 Primer 1: Predikatna logika Propozicija (tvrdnja) smislena deklarativna rečenica, npr. Petar je dobio zadatak Predikat iskaz P(x 1,...,x n ), koji može biti istinit ili lažan, zavisno od vrednosti promenljivih x 1,...,x n Primer: {x x je pozitivan celi broj manji od 4} Predikatni račun (logika predikata) 21 Primer 2: Jezik Prolog (formalna specifikacija već je program) Zasniva se na zaključivanju unazad (backward chaining) nad Hornovim klauzulama, uz neke dodatne mogućnosti upotreba u Evropi i Japanu (projekt Pete generacije računara) Hornova klauzula Program = skup klauzula oblika H :- B 1,... B n. Primer: kriminalac(x):-drzavljanin(x),oruzje(y), prodaje(x,y,z),neprijatelj(z). Efikasna unifikacija i pronalaženje klauzula, depth-first, backward chaining (s leva udesno) Ugrađeni predikati za aritmetičke izraze i sl., npr. Xis Y*Z+3 Važi pretpostavka zatvorenog sveta ( negation as failure ) ako je zadano živ(x) :- not mrtav(x). onda je živ(petar) istinito ako je mrtav(petar) lažno 22 Logičko programiranje u jeziku Prolog Konkatenacija dve liste append([],y,y). append([x L],Y,[X Z]) :- append(l,y,z). Upit:? append(a,b,[1,2]) Odgovori: A=[] B=[1,2] A=[1] B=[2] A=[1,2] B=[] 23 Pristup klasičnog i logičkog programiranja Klasično programiranje 1. Identifikacija problema 2. Prikupljanje informacija 3. Razumevanje problema 4. Programsko rešenje 5. Zapis primera problema u obliku podataka 6. Primena programa na podatke 7. Otklanjanje proceduralnih grešaka Logičko programiranje 1. Identifikacija problema 2. Prikupljanje informacija Zapis informacija u KB 5. Zapis primera problema u obliku činjenica (facts) 6. Postavljanje upita 7. Otkrivanje pogrešnih činjenica (false facts) Pretpostavlja se da je lakše otkloniti grešku u logičkom zrazu, npr. glavni-grad(r.srpska;banjaluka) nego u programskom kodu, npr. x := x Primer 3: Jezik Z Tipovi jednostavni (predefinisani i korisnički) kompozitni (konstruktori, Dekartov proizvod, opis skupova, sekvence) Relacije - podskup Dekartovog proizvoda Funkcije - specijalni slučaj relacije Šeme - opšta forma 25 Formalna specifikacija u jeziku Z 26 Osnovna svojstva jezika Z Zasniva se na predikatnoj logici prvog reda sa više ugrađenih tipova podataka i operacija Omogućava formalni opis statičkih i dinamičkih aspekata sistema Podržava inkrementalne, modularne specifikacije izgradnje i primenom računa šema (schema calculus) Ima prilično veliku zajednicu korisnika Postoje neki alati za podršku, ali je rezonovanje teško, zahteva dokazivanje teorema Iako veoma uticajan (npr. jezik Z je inspirisao Alloy), ne koristi se mnogo u praksi 27 3. Modeliranje sistema 1. Pojam modeliranja sistema 2. Modeliranje softverskih sistema 28 3.1 Pojam modeliranja sistema Model je pojednostavljena predstava ili apstrakcija stvarnosti Modeliranje je neophodno, jer se veoma složeni sistemi ne mogu drugačije razumeti Modeliranje je deo inženjerstva Ciljevi modeliranja pomaže u vizualizaciji budućeg sistema omogućava definisanje strukture ili ponašanja budućeg sistema predstavlja način upravljanja izgradnjom novog sistema dokumentuje izabrana rešenja 29 Vrste modela Skalirani modeli - umanjene kopije (maketa, fotografija) Analogni modeli - modeliraju ponašanje, ne moraju da podsećaju na sistem (mape, grafički modeli) Mentalni modeli - kvalitativni opisi (tekst) Matematički modeli - kvantitativni modeli (analitički, simulacioni) 30 3.2 Modeliranje softverskih sistema U toku definisanja i analize zahteva koriste se modeli sistema, koji su najčešće grafički (dijagrami) Model je pojednostavljena slika softverskog sistema, koja razmatra kontekst u kome se razvija, ponašanje i strukturu sistema dobar opis se postiže upotrebom više komplementarnih modela sistema svaka metodologija razvoja korist i određene modele Primeri modela (semiformalni, analogni): dijagram toka podataka (Data Flow Diagram, DFD) ER model/dijagram UML model promene stanja (state machine) objektni UML modeli (nasleđivanje, agregacija, ponašanje/sekvence) 31 4. Standard UML 1. Nastanak standarda 2. Vrste dijagrama 3. Softverski UML alati 4. Primer UML specifikacije 32 4.1 Nastanak standarda UML Objektno orijentisani programski jezici (1960-te,1970-te): Simula (Kristen Nygaard, 1962) - nadgradnja jezika Algol 60 Smalltalk (Alan Kay, 1980) - objektno orijentisan, GUI Objektno orijentisana analiza i projektovanje Grady Booch, Object-Oriented Design (1982) UML (Unified Modeling Language) je grafički jezik za specifikaciju, izgradnju i dokumentovanje razvoja softvera informacionog sistema Booch i Rumbaugh (Booch+OMT,1994) Rational (Grady Booch, James Rumbaugh, Ivar Jacobson) 33 Načini primene jezika UML 1. Izrada skica prilikom analize problema prikaz različitih aspekata problema i mogućih rešenja 2. Detaljni projektni dijagrami inicijalne specifikacije zahteva u projektnom zahtevu detaljne specifikacije softvera u projektu softvera inicijalno generisanje osnovne strukture koda (forward engineering) vizualizacija i bolje razumevanje postojećeg koda (reverse engineering) 3. UML kao programski jezik kompletna izvršna specifikacija softverskog sistema pomoću UML 34 4.2 Vrste UML dijagrama Statički (strukturni) pogled opis strukture sistema pomoću objekata, atributa, operacija i relacija npr. dijagrami klasa Dinamički pogled opis ponašanja sistema kroz prikaz saradnje objekata i promena unutrašnjih stanja npr. dijagrami sekvenci, aktivnosti, stanja UML je standardizovan razumevanje modela dobra komunikacija 35 UML 2.5 dijagrami (Object Management Group, OMG) Definisano 14 dijagrama u tri kategorije, koji opisuju različite aspekte sistema: Statička struktura (7) npr. dijagram slučajeva korišćenja (Use-Case), dijagram klasa (Class) i paketa (Package) Opšte ponašanje objekata (3) npr. dijagram stanja (Statechart) i dijagram aktivnosti (Activity) Interakcije objekata (4) npr. dijagram sekvenci (Sequence) i dijagram saradnje (Collaboration) 36 4.3 Softverski UML alati 1. Alati za crtanje dijagrama dijagrami toka (flowchart) dijagrami toka podataka (DFD) UML dijagrami 2. Alati za testiranje korektnosti formalnih specifikacija 3. CASE alati za razvoj softvera kreiranje i testiranje semiformalnih specifikacija 4. Integrisana razvojna okruženja (IDE) 37 4.4 Primer UML specifikacije a) Grafički oblik - UML dijagrami grafički prikaz nije dovoljno precizan za potrebe jednoznačne specifikacije u OO razvoju softvera b) Formalni oblik - OCL (Object Constraints Language) jezik OCL je formalni jezik za dopunski detaljni opis UML specifikacija, razumljiv učesnicima razvoja zasnovanog na modelima (Model Driven Engineering, MDE) context Employee inv tudoclinv3: ((self.grade.name = 'diploma') implies (self.taxclass = 'tc1')) and ((self.grade.name = 'doctor') implies (self.taxclass = 'tc2')) and ((self.grade.name = 'professor') implies (self.taxclass = 'tc3')) 38 5. UML dijagrami analize 1. Dijagram slučajeva korišćenja 2. Dijagram aktivnosti 3. Dijagram sekvenci 39 5.1 Dijagram slučajeva korišćenja (Use-Case Diagram) Osnovni problem u procesu projektovanja sistema je izvlačenje tačnih i neophodnih zahteva od učesnika u razvoju i njihovo predstavljanje na način razumljiv onima koji ih verifikuju i odobravaju podaci i modeli procesa, prototipovi, specifikacije zahteva razumljivi projektantima, ali ne i korisnicima dolazi do nerazumevanja, usporavnja razvoja i prekoračenja troškova 40 Dijagrami slučajeva korišćenja Slučaj korišćenja (Use Case) niz automatizovanih i manuelnih koraka za obavljanje jednog poslovnog zadatka (scenario) opis funkcija sistema iz perspektive spoljašnjih korisnika u terminologiji koju oni razumeju Dijagram slučajeva korišćenja opis interakcije između sistema i korisnika i eksternih sistema grafički prikazuje ko će koristiti sistem i na koje načine korisnik očekuje da će sobraćati sa sistemom Use-case narrative daje tekstualni opis zadatka i načina na koji će korisnik saobraćati sa sistemom radi obavljanja zadataka 41 Osnovni simboli Slučaj korišćenja (Use Case) funkcionalni podskup sistema grafički se predstavlja horizontalnom elipsom sa nazivom slučaja korišćenja (iznad, ispod ili u unutrašnjosti) Učesnik (Actor) bilo šta što saobraća sa sistemom radi razmene informacija čovek, organizacija, drugi informacioni sistem/podsistem, eksterni uređaj ili vreme vremenski događaj sistemski događaj aktiviran vremenski, učesnik je vreme Relacija između slučaja korišćenja i učesnika (aktera) 42 Relacija asocijacije slučaja korišćenja Asocijacija relacija između učesnika i slučaja korišćenja u kojoj se događa neka interakcija prikazuje se punom linijom između učesnika i slučaja korišćenja asocijacija je jednosmerna (1) ili dvosmerna (2) ako je strelica na slučaju korišćenja, inicijator je učesnik (akter) (1) ako nema strelice, primalac je akter (2) 43 Ilustracija: Dijagram slučajeva korišćenja za proces prodaje u IBM RSA 44 Ilustracija: Dijagram slučajeva korišćenja za proces prodaje u Visual Studio 5.2 Dijagrami aktivnosti (Activity Diagrams) Opis aktivnosti u sistemu, npr. u analizi sistema može se prikazati model poslovnih procesa, kao i logika slučajeva korišćenja aktivnost odluka grananje spajanje početak kraj prekid (abort) 46 Vertikalna vremenska skala Objekti Poruke 5.3 Dijagram sekvenci (Sequence Diagram) 47 Veza dijagrama sekvenci i slučajeva korišćenja Dijagrami sekvenci se mogu koristiti u razradi slučajeva korišćenja Scenario ObradaProdaje 1. Klijent dolazi na blagajnu da kupi robu/usluge 2. Blajajnik otvara novi račun 3. Blagajnik unosi stavku 4. Sistem beleži stavku i prikazuje opis, cenu i ukupni iznos Sistem ponavlja korake 3 i 4 sve dok ima stavki 5. Sistem prikazuje ukupni iznos sa PDV 6. Blagajnik saopštava ukupni uznos klijentu i traži plaćanje 7. Klijent plaća i Sistem vrši obradu plaćanja 48 5. Analiza i RUP 1. Objektno orijentisana analiza i RUP 2. Početna faza (inception) 49 5.1 Objektno orijentisana analiza i RUP Analiza je proces ispitivanja problema i zahteva, ali ne i njihovo rešavanje u toku analize se pronalaze i opisuju objekti domene problema npr. u IS letenja, koncepti Avion, Let i Pilot 50 Objedinjeni proces razvoja (Unified Process, UP) Proces razvoja softvera (Software Process) je pristup izgradnji, isporuci i održavanju softvera parcijalno uređeni niz koraka usmerenih ka cilju cilj je efikasna i predvidiva isporuka softverskog sistema, koji zadovoljava zahteve Objedinjeni proces (Unified Process, UP) je proces razvoja objektno orijentisanih sistema cilj objedinjenog procesa je omogućavanje izrade visokokvalitetnog softvera, koji zadovoljava korisničke zahteve, za predvidivo vreme i budžet Za kompleksne sisteme, objedinjeni proces predviđa iterativni razvoj, koji se sastoji od niza ciklusa, od kojih svaki rezultuje izvršnom verzijom sistema 51 Faze objedinjenog procesa (UP) Inception Elaboration Construction Transition vreme Objedinjeni proces organizuje rad i iteracije u četiri osnovne vremenske faze: 1. Inception - početna faza, definisanje obima projekta 2. Elaboration - faza razrade, planiranje, izrada specifikacija i osnovne arhitekture sistema 3. Construction - faza izgradnje sistema 4. Transition - faza prenosa sistema krajnjim korisnicima 52 Iteracije i preseci (milestones) Inception Elaboration Construction Transition Preliminarna iteracija Iteracija 1 Iteracija 2 Iteracija i Iteracija N kontrolna tačka/presek verzija konačna verzija Svaka faza i iteracija nosi određeni rizik i vremenski završava u nekoj kontrolnoj tački Pregled projekta u kontrolnoj ili presečnoj tački ocenjuje stepen zadovoljenja korisničkih zahteva i potrebu za eventualnim prestrukturiranjem projekta Svaka iteracija proizvodi novu verziju, stabilni izvršni podskup konačnog sistema 53 Discipline objedinjenog procesa Faze procesa razvoja Discipline procesa razvoja Inception Elaboration Construction Transition Poslovno modeliranje (Business Modeling) Specifikacija zahteva (Requirements) Važnost specifikacie zahteva Analiza i projektovanje (Analysis&Design) Implementacija (Implementation) Testianje (Test) Isporuka (Deployment) Pomoćne discipline procesa razvoja Upravljanje konfiguracijom (Configuration Menagment) Menadžment (Management) Čovekova okolina (Environment) Preliminarne Iteracije Iter. 1 Iter. 2 Iter. n Iteracije Iter. n+1 Iter. n+2 Iter. m Iter. m+1 54 Discipline i faze Sve iteracije podrazumevaju vremenski promenljiv rad na većini disciplina prve iteracije se pretežno bave zahtevima i projektovanjem, a naredne u sve manjoj meri Aktivnosti i rezultati nisu obavezni u svakom projektu, osim kôda rezultati razvoja se određuju prema konkretnim potrebama projekta 55 5.2 Početna faza razvoja (Inception): šta treba razviti Odgovara na veći bro
