1 Formalizacja i uwiarygodnianie Iteracyjny proces syntezy modelina podstawie artykułu Jörga Desela „Formalization and Validation. An Iterative Process in Model Synthesis”

2 Plan prezentacji Wstęp i postawienie problemu Uwiarygodnianie modeluRozwój systemu w oparciu o model Sposób modelowania Uwiarygodnianie wymagań Sieci Petriego Semantyka sekwencyjna i semantyka zależności Sieci procesów Lemat Przykładowy przebieg Rozszerzenia, doświadczenia, wnioski VIPtool

3 Postawienie problemu Chcemy uzyskać formalny model systemu kontrolowanego automatycznie na podstawie nieformalnego opisu części systemu mającej podlegać kontroli oraz wymagań dotyczących funkcjonowania całości Rozwój systemów komputerowych działających w określonym środowisku technicznym w oparciu o modele Specyfikacja wymagań dotyczących systemu Formalna specyfikacja Specyfikacja oparta o model

4 Uwiarygodnianie modelu (ang. model validation)Proces uwiarygodniania jest zwykle powiązany z samymi systemami Uwiarygodnianie – „Czy zbudowaliśmy właściwy system?” Weryfikacja – „Czy zbudowaliśmy system właściwie?” Ewaluacja – „Czy system jest użyteczny? Czy system spełni oczekiwania docelowych użytkowników?” system = model

5 Rozwój systemu w oparciu o modelanaliza i projektowanie świat rzeczywisty kodowanie system model abstrahuje od nieistotnych szczegółów abstrahuje od szczegółów implementacyjnych

6 Formalizacja i specyfikacjamodel świata rzeczywistego świat rzeczywisty świat rzeczywisty specyfikacja specyfikacja wymagań specyfikacja projektowa implementacja systemu wymagania systemu formalizacja specyfikacja formalizacja

7 Uwiarygodnianie, weryfikacja i ewaluacjamodel świata rzeczywistego świat rzeczywisty świat rzeczywisty weryfikacja specyfikacja wymagań specyfikacja projektowa implementacja systemu wymagania systemu uwiarygodnianie weryfikacja uwiarygodnianie

8 Sposób modelowania Modelowanie jest procesem kreatywnym.Założenia: dynamiczne zachowanie procesów, ekspert. Kolejne kroki formalizacji: model istniejącego środowiska uwiarygodnianie modelu środowiska poprzez symulację iteracyjna formalizacja i uwiarygodnianie kolejnych wymagań tworzonego systemu

9 Uwiarygodnianie wymagańwymaganie 1 model 1 symulacja zachowanie modelu 1 zachowanie z wymaganiem 1 filtr

10 Uwiarygodnianie wymagańwymaganie 1 model 1 wdrożenie model 2 wymaganie 2 symulacja zachowanie z wymaganiem 2 zachowanie modelu 2 filtr

11 Sieci Petriego

12 Sieci Petriego

13 Przykładowa sieć Petriegopodgrzej wydaj włóż żeton odrzuć żeton akceptuj żeton ciepły zimny gotowy licznik włożony zaakceptowany

14 Opis zachowania sieci PetriegoDwie różne techniki opisu zachowania sieci Petriego. Przebieg może być opisany przez ciąg nazw przejść sieci (reprezentujący następujące po sobie zdarzenia) lub przez przyczynowy uporządkowany zbiór zdarzeń. Pierwsza technika opisywana przez ciągi wystąpień (ang. occurrence sequences) jest oparta o semantykę sekwencyjną sieci Petriego (ang. sequential semantics). Druga używa sieci procesów (ang. process nets) reprezentujących przyczynowe przebiegi (c-przebiegi, ang. causal runs) i jest oparta o semantykę zależności sieci Petriego (ang. causal semantics).

15 Semantyka sekwencyjnaJedną z głównych zalet jest prostota. Każdy z ciągów wystąpień może być postrzegany jako sekwencja stanów systemu i transformacji prowadząca od jednego stanu do innego. Formalnie stany nie występują w ciągu wystąpień (mamy jedynie nazwy przejść) Przykładowy ciąg wystąpień: włóż żeton, akceptuj żeton, podgrzej, wydaj, włóż żeton, akceptuj żeton, podgrzej, wydaj prowadzi do stanu różniącego się od wyjściowego jedynie liczbą żetonów w liczniku.

16 Semantyka zależności Jedną z głównych zalet jest wyraźna reprezentacja przyczynowej zależności zdarzeń. Zdarzenia zależne połączone są ścieżką w sieci procesów. Zdarzenia współbieżne nie mają połączenia.

17 Sieci procesów

18 Sieci procesów

19 Sieci procesów Warunek c reprezentuje pojawienie się pionka na miejscu α(c). Zdarzenie e reprezentuje wystąpienie przejścia β(c). W przebiegu, każdy pionek jest produkowany (pochłaniany) przez co najwyżej jedno wystąpienie przejścia. W związku z tym warunki w sieci procesów mają co najwyżej jedno wejście i jedno wyjście. Pre- i post-zbiory zdarzeń są zachowywane. W początkowym stanie tylko elementy minimalne zawierają pionki. Początkowy stan odpowiada początkowej konfiguracji.

20 Przykładowe sieci procesówgotowy ciepły włożony licznik zaakceptowany włóż żeton akceptuj wydaj podgrzej zimny zimny zimny gotowy ciepły zimny włożony licznik zaakceptowany włóż żeton akceptuj wydaj podgrzej

21 Lemat

22 Lemat

23 Przykładowy przebieg włóż żeton ciepły gotowy włożony licznik podgrzejwydaj odrzuć żeton zimny zaakceptowany akceptuj żeton akceptuj żeton akceptuj żeton licznik licznik wydaj wydaj gotowy włóż żeton włożony zaakceptowany gotowy włóż żeton włożony zaakceptowany gotowy ciepły ciepły ciepły zimny podgrzej zimny podgrzej zimny

24 Przykładowy przebieg włóż żeton ciepły gotowy włożony licznik podgrzejwydaj odrzuć żeton zimny zaakceptowany akceptuj żeton akceptuj żeton akceptuj żeton licznik licznik wydaj wydaj gotowy włóż żeton włożony zaakceptowany gotowy włóż żeton włożony zaakceptowany gotowy ciepły ciepły ciepły zimny podgrzej zimny podgrzej zimny

25 Przykładowy przebieg włóż żeton ciepły gotowy włożony licznik podgrzejwydaj odrzuć żeton zimny zaakceptowany akceptuj żeton akceptuj żeton akceptuj żeton licznik licznik wydaj wydaj gotowy włóż żeton włożony zaakceptowany gotowy włóż żeton włożony zaakceptowany gotowy ciepły ciepły ciepły zimny podgrzej zimny podgrzej zimny

26 Przykładowy przebieg włóż żeton ciepły gotowy włożony licznik podgrzejwydaj odrzuć żeton zimny zaakceptowany akceptuj żeton akceptuj żeton akceptuj żeton licznik licznik wydaj wydaj gotowy włóż żeton włożony zaakceptowany gotowy włóż żeton włożony zaakceptowany gotowy ciepły ciepły ciepły zimny podgrzej zimny podgrzej zimny

27 Przykładowy przebieg włóż żeton ciepły gotowy włożony licznik podgrzejwydaj odrzuć żeton zimny zaakceptowany akceptuj żeton akceptuj żeton akceptuj żeton licznik licznik wydaj wydaj gotowy włóż żeton włożony zaakceptowany gotowy włóż żeton włożony zaakceptowany gotowy ciepły ciepły ciepły zimny podgrzej zimny podgrzej zimny

28 Przykładowy przebieg włóż żeton ciepły gotowy włożony licznik podgrzejwydaj odrzuć żeton zimny zaakceptowany akceptuj żeton akceptuj żeton akceptuj żeton licznik licznik wydaj wydaj gotowy włóż żeton włożony zaakceptowany gotowy włóż żeton włożony zaakceptowany gotowy ciepły ciepły ciepły zimny podgrzej zimny podgrzej zimny

29 Przykładowy przebieg włóż żeton ciepły gotowy włożony licznik podgrzejwydaj odrzuć żeton zimny zaakceptowany akceptuj żeton akceptuj żeton akceptuj żeton licznik licznik wydaj wydaj gotowy włóż żeton włożony zaakceptowany gotowy włóż żeton włożony zaakceptowany gotowy ciepły ciepły ciepły zimny podgrzej zimny podgrzej zimny

30 Przykładowy przebieg włóż żeton ciepły gotowy włożony licznik podgrzejwydaj odrzuć żeton zimny zaakceptowany akceptuj żeton akceptuj żeton akceptuj żeton licznik licznik wydaj wydaj gotowy włóż żeton włożony zaakceptowany gotowy włóż żeton włożony zaakceptowany gotowy ciepły ciepły ciepły zimny podgrzej zimny podgrzej zimny

31 Przykładowy przebieg włóż żeton ciepły gotowy włożony licznik podgrzejwydaj odrzuć żeton zimny zaakceptowany akceptuj żeton akceptuj żeton akceptuj żeton licznik licznik wydaj wydaj gotowy włóż żeton włożony zaakceptowany gotowy włóż żeton włożony zaakceptowany gotowy ciepły ciepły ciepły zimny podgrzej zimny podgrzej zimny

32 Symulacja poprzez konstruowanie przebiegówPrzez symulację rozumiemy generowanie przebiegów modelu. Uwiarygodnianie przez symulację wymaga kontrolowania całego procesu przez eksperta w danej dziedzinie. Graficzna reprezentacja przebiegów. Takie aspekty zachowania systemu jak przepływ sterowania, przepływ dóbr, możliwe współbieżne zachowania, itp. są widoczne w sieci procesów a zatracone w ciągach wystąpień. Liczba ciągów wystąpień odpowiadająca pojedynczej sieci procesów rośnie bardzo szybko wraz ze wzrostem możliwych współbieżnych zachowań systemu.

33 Cele i fakty Cel (ang. goal) – wystąpienie określonej sytuacji.Fakt (ang. fact) – własność zachodząca dla wszystkich osiągalnych stanów systemu. Opracowane są algorytmy, które w oparciu o sieci procesów badają czy określone cele mogą zostać osiągnięte lub czy fakty dotyczące projektowanego systemu są zawsze spełnione.

34 Rozszerzenia, doświadczenia, wnioskiużycie kolorowanych sieci Petriego (ang. Colored Petri Nets) sygnały modularyzacja VIPtool (http://www.informatik.ku-eichstaett.de/projekte/vip/) Projekt dla Audi AG – zastosowanie przedstawionych metod w praktyce.