1 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 1 Specyfikacja formalna l Przedstawienie metod specyfikacji formalnej, których można użyć do uszczegóławiania specyfikacji wymagań systemowych,

2 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 2 Cele l Wiedzieć, dlaczego metody specyfikacji formalnej pomagają w znajdowaniu błędów w wymaganiach systemowych. l Znać ryzyko związane z używaniem metod algebraicznych specyfikacji formalnej do definiowania specyfikacji interfejsów. l Wiedzieć, jak do specyfikacji zachowania można użyć metod formalnych opartych na modelach.

3 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 3 Zawartość l Specyfikacja formalna w procesie tworzenia oprogramowania l Specyfikacja interfejsu l Specyfikacja zachowania

4 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 4 Metody formalne l Analiza matematyczna stanowi rutynową składową procesu opracowywania i zatwierdzania projektu produktu. l Tak zwane „metody formalne” budowy oprogramowania nie są szeroko stosowane w przemysłowym wytwórstwie oprogramowania. l Pojęcie „metod formalnych” obejmuje: specyfikowanie formalne systemu, analizowanie i dowodzenie specyfikacji, proces tworzenia z przekształceniem, weryfikowanie programów.

5 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 5 Problemy z akceptacją l Przewidywania, że w XXI wieku duża część oprogramowania powstaje z użyciem metod formalnych nie sprawdziła się z powodów: sukcesów inżynierii oprogramowania, zmiany rynku, ograniczonego zasięgu metod formalnych, ograniczonej skalowalności metod formalnych.

6 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 6 Użycie metod formalnych l Specyfikacja formalna jest doskonałym sposobem na wykrycie błędów w specyfikacji i przedstawienie specyfikacji systemu w sposób jednoznaczny. l W systemach, w których nie można dopuścić do awarii, użycie metod formalnych może być uzasadnione i opłacalne. l Metody formalne są coraz częściej stosowane w wyspecjalizowanej dziedzinie tworzenia systemów krytycznych.

7 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 7 Specyfikacja formalna w procesie tworzenia oprogramowania l Nie obejmuje detali implementacyjnych, ale powinna stanowić pełny model matematyczny systemu. l We wczesnych etapach procesu najważniejsza jest specyfikacja nastawiona na użytkownika. l Końcowy etap procesu, który obejmuje stworzenie pełnej, spójnej i precyzyjnej specyfikacji, jest jednak zasadniczo zadaniem zleceniobiorcy. Stanowi on podstawę implementacji systemu. Ta precyzyjna specyfikacja może być specyfikacja formalną.

8 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 8 Specyfikowanie i projektowanie Rosnący udział zleceniobiorcy Malejący udział klienta Definiowanie wymagań użytkownika Specyfikowanie wymagań systemowych Projektowanie architektoniczne Specyfikowanie formalne Projektowanie na wysokim poziomie Specyfikowanie Projektowanie

9 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 9 Specyfikowanie formalne w procesie budowania oprogramowania Definiowanie wymagań użytkownika Modelowanie systemu Specyfikowanie formalne Specyfikowanie wymagań systemowych Projekt architektoniczny Projektowanie na wysokim poziomie

10 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 10 Dwa podejścia do specyfikacji formalnej l Podejście algebraiczne Opisuje się system w kategoriach operacji i związków. l Podejście oparte na modelach Buduje się model systemu za pomocą pojęć matematycznych, takich jak zbiory i ciągi. Operacje systemu definiuje się przez wywoływane przez nie zmiany stanu systemu.

11 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 11 Języki specyfikacji formalnej Sekwencyjne Współbieżne Algebraiczne Larch (Guttag i inni, 1995, 1993) Lotos (Bolognesi OBJ (Futatsugi i inni, 1995) i Brinksma, 1987) Oparte na Z (Spivey, 1992) CSP (Hoare, 1995) modelach VDM (Jones, 1980) Sieci Petriego (Peterson, 1981) B (Wordsworth, 1996)

12 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 12 Użycie specyfikacji formalnej l Zwiększa początkowe koszty budowy oprogramowania. l Gdy zastosuje się konwencjonalny proces, koszty zatwierdzania stanowią 50% kosztu budowania, a koszty implementacji i projektowania są wyższe niż koszty specyfikowania. l Jeżeli użyje się specyfikacji formalnych, to koszty specyfikowania i implementacji są porównywalne, ale koszty zatwierdzania są znacząco obniżone. l Opracowanie specyfikacji formalnej umożliwia wykrycie błędów w wymaganiach, unika się więc powtarzania prac w celu poprawienia tych błędów po zaprojektowaniu systemu.

13 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 13 Koszty budowania oprogramowania ze specyfikacją formalną Bez specyfikacji formalnej Ze specyfikacją formalną Koszt Specyfikowanie Projektowanie i implementacja Zatwierdzanie Specyfikowanie Projektowanie i implementacja Zatwierdzanie

14 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 14 Specyfikacja interfejsu l Wielkie systemy zwykle składają się z niezależnie budowanych podsystemów. l Podsystemy korzystają z innych podsystemów, a zatem zasadniczą częścią procesu specyfikowania jest definiowanie interfejsów podsystemów. l Po uzgodnieniu i określeniu tych interfejsów podsystemy można budować niezależnie.

15 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 15 Obiekty interfejsu między podsystemami. Podsyste Obiekty interfejsu Podsystem A Podsystem B

16 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 16 Składowe specyfikacji l Wstęp Deklaruje się rodzaj (nazwę typu) specyfikowanego bytu. l Część opisowa Nieformalnie przedstawia się operacje. l Część sygnaturowa Definiuje składnię interfejsu klasy obiektów lub abstarkcyjnego typu danych. l Część aksjomatyczna Definiuje znaczenie operacji przez podanie zbioru aksjomatów, które charakteryzują zachowanie abstrakcyjnego typu danych.

17 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 17 Struktura specyfikacji algebraicznej rodzaj imports Nieformalny opis rodzaju i jego operacji Sygnatury operacji ustalające ich nazwy i typy parametrów Aksjomaty definiujące operacje na tym rodzaju

18 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 18 Proces budowy specyfikacji formalnej l Proces budowy specyfikacji formalnej podsystemu powinien obejmować następujące czynności: strukturalizację specyfikacji, nazwanie specyfikacji, wybór operacji, specyfikowanie nieformalne operacji, definiowanie składni, definiowanie aksjomatów.

19 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 19 Klasy operacji na abstrakcyjnym typie danych l Operacje konstruktorowe, które tworzą lub modyfikują byty rodzaju definiowanego w specyfikacji. Zwykle maja nazwy takie jak Utwórz, Zmień, Dodaj albo tak jak w tym wypadku Kons znaczące konstruuj. l Operacje inspekcyjne, które obliczają atrybuty rodzaju zdefiniowanego w specyfikacji. Zwykle ich nazwy odpowiadają nazwom atrybutów lub mają nazwy takie jak Oblicz, Pobierz.

20 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 20 Specyfikacja listy l Operacjami konstruktorowymi są Utwórz, Kons i Ogon, które budują listy. l Operacjami inspekcyjnymi są Głowa i Długość, które służą do odczytu atrybutów listy. l Nie ma więc potrzeby definiowania aksjomatów operacji Ogon dla operacji Głowa i Długość, natomiast operacja Ogon musi być zdefiniowana za pomocą konstruktorów podstawowych.

21 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 21 Prosta specyfikacja listy LISTA (Elem) rodzaj Lista imports INTEGER Definiuje listę, do której dodaje się elementy na końcu, a usuwa na początku. Operacjami są Utwórz, która powoduje utworzenie pustej listy, Kons, która tworzy nową listę z dodatkowym elementem, Długość, która wyznacza długość listy, Głowa, która podaje pierwszy element na liście, i Ogon, która tworzy nową listę przez usunięcie głowy ze swojej listy wejściowej. Niezdefiniowane reprezentuje niezdefiniowaną wartość typu Elem. UtwórzLista Kons (Lista, Elem)Lista Głowa (Lista)Elem Długość (Lista)Integer Ogon (Lista)Lista Głowa (Utwórz) = Niezdefiniowane exception (lista pusta) Głowa (Kons (L, w)) = if L = Utwórz then w else Głowa (L) Długość (Utwórz) = o Długość (Kons(L, w)) = Długość (L) + 1 Ogon(Utwórz) = Utwórz Ogon (Kons (L, w)) = if L = Utwórz then Utwórz else kons (Ogon (L), w)

22 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 22 Specyfikacje rekurencyjne l W specyfikacjach algebraicznych często używa się rekurencji. l Wartością operacji Ogon jest lista utworzona przez wzięcie listy wejściowej i usunięcie jej głowy. l W definicji operacji Ogon pokazano, jak używać rekurencji do budowy specyfikacji algebraicznych. Ogon ([5, 7, 9]) = Ogon (Kons ([5, 7], 9)) = Kons (Ogon ([5, 7, 9])) = Kons (Ogon (Kons ([5]), 7)), 9) = Kons (Kons (Ogon ([5]), 7, 9) = Kons (Kons (Ogon (Kons ([], 5)), 7), 9) = Kons (Kons (Utwórz, 7), 9) = Kons ([7], 9) = [7, 9]

23 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 23 System kontroli lotów l Załóżmy, że w systemie kontroli lotów zaprojektowano obiekt reprezentujący sektor kontrolowanej przestrzeni powietrznej. l Każdy taki sektor może zawierać kilka samolotów, z których każdy ma inny identyfikator. l Ze względów bezpieczeństwa samoloty muszą być od siebie oddalone o co najmniej 300 metrów w pionie. l System ma ostrzec kontrolera, gdy nastąpi próba umieszczenia samolotu, który łamie te ograniczenia.

24 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 24 Operacje na obiekcie-sektorze l Krytyczne operacje, które można na tym obiekcie wykonywać: Wejście. Ta operacja dodaje samolot (reprezentowany przez identyfikator) do przestrzeni powietrznej na podanej wysokości. Wyjście. Ta operacja usuwa wskazany samolot z kontrolowanego sektora. Przestrzeń. Ta operacja przesuwa samolot z jednej wysokości na inną. Znajdź. Ta operacja podaje bieżący pułap samolotu o zadanym identyfikatorze w podanym sektorze.

25 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 25 Proste operacje l Łatwiej będzie wyspecjalizować te operacje, jeśli wprowadzimy kilka innych operacji interfejsu: Utwórz. Reprezentuje on sektor, w którym nie ma ani jednego samolotu. Umieść. Dodaje samolot do sektora bez sprawdzania skojarzonych z nim ograniczeń. W-przestrzeni. Dla zadanego sygnału rozpoznawczego samolotu ta operacja przekazuje wartość logiczna prawdy, jeśli samolot jest w kontrolowanym sektorze, i fałsz w przeciwnym wypadku. Zajęta. Dla zadanej wysokości ta operacja przekazuje wartość logiczną prawdy, jeśli w trzystumetrowym otoczeniu tej wysokości znajduje się jakikolwiek samolot, i fałsz w przeciwnym wypadku.

26 Specyfikacja kontrolowanego sektora SEKTOR rodzaj Sektor imports INTEGER, BOOLEAN Wejście - dodaje samolot do sektora, o ile zachowane są ograniczenia bezpieczeństwa Wyjście - usuwa samolot z sektora Przesuń - przenosi samolot z jednej wysokości na inną, o ile jest to bezpiecznie Znajdź - podaje wysokość samolotu w sektorze Utwórz – tworzy pusty sektor Umieść – dodaje samolot do sektora bez sprawdzania ograniczeń W-przestrzeni – sprawdza, czy samolot jest już w sektorze Zajęta – sprawdza, czy podana wysokość jest dostepna Wejście (Sektor, Sygnał, Wysokość)Sektor Wyjście (Sektor, Sygnał)Sektor Przesuń (Sektor, Sygnał, Wysokość)Sektor Znajdź (Sektor, Sygnał)Sektor UtwórzSektor Umieść (Sektor, Sygnał, Wysokość)Sektor W-przestrzeni (Sektor, Sygnał)Boolean Zajęta (Sektor, Wysokość)Boolean Wejście (Sek, Syg, W) = if W-przestrzeni (Sek, Syg) then Sek exception (Samolot już jest w sektorze elsif Zajęta (Sek, W) then Sek exception (Komunikat wysokości) else Umieść (Sek, Syg, W) Wyjście (Utwórz, Syg) = Utwórz exception (Samolotu nie ma w sektorze) Wyjście (Umieść (Sek, Syg1, W1), Syg) = if Syg = Syg1 then Sek else Umieść (Wyjście (Syk, Syg), Syg1, W1) Przesuń (Sek, Syg, W) = if Sek = Utwórz then Utwórz excepition (w sektorze nie ma żadnego samolotu) elsif not W-przestrzeni (Sek, Syg) then Sek exception (Samolotu nie ma w sektorze) elsif Zajęta (Sek, W) then Sek exception (Konflikt wysokości) else Umieść (Wyjście (Sek, Syg), Syg, W) -NIE-WYSOKOŚĆ oznacza, że nie da się przekazać sensownej wysokości Znajdź (Utwórz, Syg) = NIE-WYSOKOŚĆ exception (Samolotu nie ma w sektorze) Znajdź (Umieść (Sek, Syg1, W1), Syg) = if Syg = Syg1 then W1 else Znajdź (Sek, Syg) Zajęta (Utwórz, W) = false Zajęta (Umieść (Sek, Syg1, W1), W) = if (W1 > W and W1 – W W1 and W – W1

27 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 27 Uwagi do specyfikowania l Głównych operacji konstruktowych Utwórz i Umieść używamy w specyfikacjach pozostałych operacji. l Zajęta i W-przestrzeni są operacjami sprawdzającymi, które zdefiniowano za pomocą Utwórz i Umieść.

28 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 28 Specyfikacje oparte na modelach l Alternatywnym podejściem do specyfikacji formalnych, które powszechnie stosowano już w przedsięwzięciach przemysłowych, są specyfikacje oparte na modelach. l W notacji Z system jest modelowany za pomocą zbiorów i relacji między zbiorami. Z rozszerza pojęcia matematyczne o konstrukcje szczególnie przydatne w specyfikacji oprogramowania.

29 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 29 Struktura schematu Z Nazwa schematuSygnatura schematuPredykat schematu Zbiornik zawartość: N pojemność: N zawartość ≤ pojemność

30 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 30 Diagram blokowy pompy insulinowej Zbiornik insuliny Zasilanie Sterownik Pompa Miernik Igła Alarm Wyświetlacz 2 Wyświetlacz 1 Zegar

31 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 31 Modelowanie pompy insulinowej l Stan wymodelowano za pomocą kilku zmiennych stanowych: odczyt? dawka, dawka_całkowita o0, o1, o2 zapas alarm! pompa! wyświetlacz1!, wyświetlacz2!

32 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 32 Niezmienniki schematu l Z schemat definiuje niezmienniki, które są zawsze spełnione. l Warunki nałożone na schemat pompy insulinowej, które musza być zawsze spełnione to: Dawka nie może być większa niż zapas, tzn. nie da podać więcej insuliny niż obecnie jest w zbiorniku. Żadna dawka nie może być większa niż 5 jednostek insuliny, a całkowita dawka podana w okresie nie może przekroczyć 50 jednostek. Są to warunki bezpieczeństwa. Wartość zmiennej wyświetlacz1! Jest komunikatem o stanie zbiornika insuliny.

33 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 33 Schemat pompy insulinowej Pompa insulinowa odczyt? : N dawka, dawka_całkowita : N o0, o1,o2 : N // służą do przechowywania ostatnich trzech odczytów zapas : N alarm! : {włączony, wyłączony} pompa! : N wyświetlacz1!, wyświetlacz2! : STRING dawka = 10 wyświetlacz1! = „Niski poziom insuliny” zapas

34 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 34 Obliczanie dawkowania l Pompa insulinowa sprawdza poziom glukozy we krwi co 10 minut i (w uproszczeniu) podaje insulinę, jeśli tempo zmiany poziomu glukozy rośnie. l Ilość insuliny do wstrzyknięcia jest obliczana, tak jak pokazano na schemacie DAWKOWANIE. l Jeśli tempo zmiany jest stałe, to podaje się stałą ilość insuliny. l Na podstawie tego schematu można wywnioskować, że istnieją różne sytuacje wpływające na wielkość dawki.

35 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 35 Schemat DAWKOWANIE DAWKOWANIE ΔPompa_insulinowa ( dawka = 0 ^ ( ((o1 >= o0) ^ (o2 = o1)) v ((o1 > o0) ^ (o2

36 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 36 Schematy opisujące dane wyjściowe l Wymodelowano wyświetlacze maszyny i wbudowany alarm. l W schemacie WYŚWIETLANIE stwierdzono, że wyświetlacz2! Pokazuje obliczoną dawkę (Liczba_na_napis to funkcja konwersji) l Wyświetlacz1! Pokazuje komunikat ostrzegawczy, albo słowo „OK”. l W schemacie ALARM ustalono warunki, w których alarm jest uruchamiany. Włącza się go, gdy odczyt poziomu glukozy jest zbyt niski (mniej niż 3) lub zbyt wysoki (więcej niż 30).

37 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 37 Schematy wyjściowe WYŚWIETLANIE ΔPompa_insulinowa wyświetlacz2!’ = Liczba_na_napis(dawka) ^ odczyt?

38 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 38 Sprawdzenie wewnętrznej zgodność systemu l W ogólnym schemacie Pompa_insulinowa napisano, że wyświetlacz1! Powinien wskazywać stan zbiornika insuliny. l W schemacie WYŚWIETLANIE stwierdzono jednak, że ten wyświetlacz ma pokazywać różne komunikaty ostrzegawcze lub informację, że poziom glukozy we krwi mieści się w akceptowalnym przedziale. Występuje tu konflikt. l Wyjawienie problemów, które należy rozwiązać, jest jedną z głównych zalet stosowania specyfikacji formalnych.

39 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 39 Główne tezy l Metody specyfikacji formalnej systemów uzupełniają metody specyfikacji nieformalnej. Można ich użyć do udoskonalenia szczegółowej, ale specyfikacji nieformalnej wymagań systemowych. Pomagają zatem w zasypaniu przepaści między wymaganiami, a projektowaniem. l Specyfikacje formalne są dokładne i jednoznaczne. Usuwają ze specyfikacji obszary wątpliwe i pozwalają uniknąć niektórych problemów z niewłaściwą interpretacją języka. Niespecjaliści mogą mieć jednak trudności ze zrozumieniem specyfikacji formalnych. l Zasadniczą korzyścią z zastosowania metod formalnych w procesie budowania oprogramowania jest wymuszanie analizy wymagań systemowych już we wczesnej fazie. Poprawianie błędów w tej fazie jest tańsze niż modyfikacja gotowego systemu.

40 ©Ian Sommerville 2000Inżynieria oprogramowania, Rozdział 9 Slide 40 Główne tezy l Metody specyfikacji formalnej najbardziej przydają się przy budowaniu systemów krytycznych, w których bezpieczeństwo, niezawodność i zabezpieczenia są szczególnie istotne. Można ich także użyć do określania standardów. l Metody algebraiczne specyfikacji formalnej są szczególnie przydatne do specyfikowania interfejsów, przy czym przez interfejs rozumie się zbiór klas obiektów lub abstrakcyjny typ danych. W tych metodach ukrywa się stan systemu, a system specyfikuje się w kategoriach związków między operacjami interfejsu. l W metodach opartych na modelach system przedstawia się za pomocą pojęć matematycznych, takich jak zbiory i funkcje. Można w nich odwołać się do stanu systemu, co upraszcza niektóre rodzaje specyfikacji zachowania.