Metody Formalnej Analizy Systemów Wbudowanych Czasu Rzeczywistego

mgr inż. Jarosław Baniewicz

Promotor: prof. dr hab. Marcin Szpyrka
Dyscyplina: Informatyka


W niniejszej rozprawie zastosowano nowatorski język modelowania formalnego Alvis. Język ten został opracowany i jest nadal rozwijany w Katedrze Informatyki Stosowanej na Wydziale Elektrotechniki, Automatyki, Informatyki i Inżynierii Biomedycznej Akademii Górniczo-Hutniczej w Krakowie.

Głównym celem niniejszej rozprawy było opracowanie rozszerzenia języka Alvis na potrzeby modelowania wbudowanych systemów czasu rzeczywistego, z założeniem, że działają one na platformie jednoprocesorowej.

W tym celu opracowano nową warstwę systemowa języka Alvis, która przede wszystkim uwzględnia aspekty związane z czasem oraz definiuje algorytm szeregowania zadań systemu czasu rzeczywistego. Na potrzeby stosowania nowej warstwy systemowej opracowano i zaimplementowano nowy algorytm wyznaczania etykietowanych systemów przejść. Implementacja jest rozszerzeniem stosowanej w środowisku Alvis reprezentacji IHR (Intermediate Haskell Representation), przez co stanowi naturalny etap rozwoju języka Alvis i wspierającego go oprogramowania.

Niniejsza rozprawa zawiera także studium przypadków, w którym pokazano praktyczne wykorzystanie Alvisa do tworzenia modeli formalnych, dla dwóch systemów czasu rzeczywistego.

Język modelowania Alvis powstał z założeniem stworzenia takiego formalizmu, który z jednej strony byłby prosty do opanowania przez inżyniera informatyka, a z drugiej strony stwarzałby możliwość formalnej analizy projektowanego przez niego systemu. Język Alvis został opracowany i jest nadal rozwijany w Katedrze Informatyki Stosowanej na Wydziale Elektrotechniki, Automatyki, Informatyki i Inżynierii Biomedycznej Akademii Górniczo-Hutniczej w Krakowie. Główne cechy języka Alvis to:

• możliwość weryfikacji modelu formalnego stworzonego dla danego systemu;
• graficzny język umożliwiający modelowanie struktury tworzonego systemu z uwzględnieniem przepływu informacji i sterowania.
• możliwość graficznej hierarchizacji modelu;
• język wysokiego poziomu definiujący dynamikę elementów składowych (agentów) modelu;

Język Alvis powstał jako następca języka XCCS, który z kolei rozszerza algebry procesów CCS o możliwość graficznego modelowania połączeń miedzy agentami. Alvis zapożycza termin agent z algebr procesów i przypisuje go każdemu elementowi systemu, który stanowi wybraną, trwającą w czasie funkcjonalność danego systemu. Dodatkowo agent jest niepodzielną jednostką systemu (ang. entity), której można przypisać stan. Stan modelu składającego się ze skończonego zbioru agentów jest ciągiem stanów wszystkich agentów. W celu zdefiniowania dynamiki agentów, zamiast równań algebraicznych, w Alvisie używa się imperatywnego języka wysokiego poziomu oraz języka Haskell. Kod agenta składa się z pojedynczych instrukcji, które dla wersji czasowych Alvisa posiadają zdefiniowany czas ich wykonywania. Cecha ta jest istotna dla niniejszej rozprawy, gdyż umożliwia uwzględnienie aspektów czasowych w modelu. Użycie składni języka Haskell daje projektantowi możliwość zdefiniowania typów danych oraz operatorów i funkcji działających na tych typach. Warstwa graficzna języka Alvis umożliwia prezentację interfejsów poszczególnych agentów, którymi są odpowiednio porty wejściowe, wyjściowej i dwukierunkowe. Dzięki tym interfejsom agenty mogą się ze sobą komunikować, wymieniać dane lub po prostu synchronizować się na wzajem. Mechanizm komunikacji został oparty na idei spotkań, zaczerpniętej z języka Ada. Agent inicjalizujący spotkanie czeka, aż inny agent dołączy i zacznie z nim wymieniać dane lub zsynchronizuje się.
Z punktu widzenia tej rozprawy ważną kwestią jest dostępność dla agentów zasobów procesora. Agent, który je przejął i czeka na reakcje ze strony innego agenta, przechodzi w stan oczekiwania. W przypadku portów wejściowych agent oczekuje wartości o konkretnym typie lub sygnału, w przypadku komunikacji polegającej na synchronizowaniu się agentów. Jeżeli komunikacja odbywa się na porcie wyjściowym agenta, oznacza to, że agent próbuje wysłać wartość danego typu, lub sygnał. Podobnie jak dla portu wejściowego agent również oczekuje na agenta, który pobierze tą wartość albo sygnał z portu wyjściowego agenta, który tą komunikację rozpoczął. Mamy tutaj do czynienia ze współbieżnym wykonywaniem akcji przez agenty, ponieważ agent rozpoczynający spotkanie zwalnia zasoby procesora, w celu umożliwienia przejęcia tychże przez innego agenta i dokończenia spotkania. Dodatkowo agenty posiadają swoje priorytety, co sprawia, że agent, który jest oczekiwany, wcale nie musi być tym, który w danym momencie czasowym zostanie wypromowany do stanu aktywnego, umożliwiającego mu przejecie zasobów procesora i co za tym idzie wykonywanie swoich akcji.
Dzięki warstwie graficznej projektant może również zadecydować o hierarchicznych zależnościach pomiędzy elementami systemu. Cecha ta wprowadza do modelu modułowość systemu, czyli pozwala uwzględnić potencjalne podsystemy danego systemu. Kolejną ważną składową języka Alvis, z uwagi na weryfikację systemu, jest warstwa systemowa modelu. Pozwala ona zdefiniować kwestie sprzętowe projektowanego systemu, co ma istotny wpływ na budowany docelowo etykietowany system przejść. Poszczególne wersje systemowe różnią się od siebie poprzez to, że definiują określoną liczbę dostępnych procesorów oraz uwzględniają bądź nie kwestie związane z domeną czasu. Wersje warstwy systemowej przyjęto oznaczać symbolem α_s^n , gdzie:

• n ∈ N oznacza liczbę procesorów dostępnych dla danej platformy sprzętowej;
• s jest nazwą danej wersji, która odróżnia wersje, w przypadku gdy mamy do czynienia z wersjami, które mają tą samą ilość dostępnych procesorów. Jest to uzasadnione tym, że nie ma takiego wymagania, aby istniała tylko jedna wersja dla np. platform jednoprocesorowych. Przykładowo projektant może stworzyć dwie wersje α_s1^3 i α_s2^3, które różnią się sposobem szeregowania agentów, ale obie będą przystosowane do platform sprzętowych opartych na trzech procesorach.

Warstwa podstawowa w Alvisie jest oznaczana jako α^0. Warstwa ta każdemu agentowi w modelu przydziela swobodny dostęp do procesora. Oznacza to, że agenty ani przez chwilę nie rywalizują pomiędzy sobą o dostęp do zasobów procesora. W warstwie tej główny nacisk kładziony jest na współbieżność wykonywanych akcji. Warstwa systemowa języka modelowania Alvis pozwala wyznaczyć etykietowany system przejść, który stanowi reprezentację przestrzeni stanów danego modelu.

Jako podstawowy cel podjętych badań przyjęto próbę opracowania formalnego opisu modeli w języku Alvis, stosujących warstwę systemową α_FPPS^1. Za nazwę tej wersji wzięto nazwę algorytmu szeregującego (ang. scheduler) – Fixed Priority Preemptive Scheduling. Poszczególne człony tej nazwy określają następujące założenia algorytmu szeregowania agentów w warstwie α_FPPS^1:

• Fixed Priority – stały, ustalony priorytet agenta, niezmienny w czasie;
• Preemptive Scheduling – zarządzanie dostępem do zasobów procesora poprzez wywłaszczanie jednych agentów na rzecz drugich, posiadających większy priorytet.

Pod względem sprzętowym warstwa ta miała wspierać modelowanie systemów wbudowanych czasu rzeczywistego uruchomionych na platformach jednoprocesorowych, a więc takich, w których istnieje ciągła rywalizacja pomiędzy agentami o przejęcie kontroli nad zasobami procesora. W celach weryfikacji modelu opracowano opisany algorytm tworzenia etykietowanego systemu przejść dla modeli z warstwą systemową α_FPPS^1. Dodatkowo zaproponowane rozwiązanie jest zgodne z podstawowymi założeniami języka Alvis i wpisuje się w obowiązujące rozwiązania i definicje. Oznacza to, że powstała warstwa systemowa α_FPPS^1 jest rozszerzeniem dla już istniejących warstw – α^0 i jej wersji czasowej. Formalnie tezę rozprawy zdefiniowano następująco:
Język Alvis, wsparty odpowiednimi narzędziami komputerowymi, może być efektywnie użyty do modelowania systemów wbudowanych, umożliwiając jednocześnie formalną analizę modelu z zastosowaniem metod i narzędzi typowych dla technik weryfikacji modelowej.
Dla uzasadnienia tezy w rozprawie pokazano, że warstwa systemowa α_FPPS^1 rozszerza język modelowania Alvis w następujących aspektach:

• możliwe jest modelowanie systemów wbudowanych czasu rzeczywistego działających na platformie jednoprocesorowej;
• algorytm szeregowania zadań uwzględnia priorytety występujących w modelu agentów i na tej podstawie dokonuje wywłaszczania agentów o niższych priorytetach na rzecz tych agentów, których priorytety są wyższe;
• możliwe jest wygenerowanie etykietowanego systemu przejść, który stanowi reprezentację przestrzeni stanów dla modelu systemu wbudowanego czasu rzeczywistego.

Rozprawa Doktorska

1. J. Baniewicz and M. Szpyrka. Detekcja zakleszczenia w systemie ABS z zastosowaniem języka Alvis. In L. Trybus and S. Samolej, editors, Projektowanie, analiza i implementacja systemów czasu rzeczywistego, volume 300, chapter 6, pages 77–86. Wydawnictwo Komunikacji i Łączności, 2011.
2. J. Baniewicz and M. Szpyrka. Priority inversion detection in Alvis model. In Proc. of Mixdes 2011, the 18th International Conference Mixed Design of Integrated Circuits and Systems, page 162, Gliwice, Poland, June 16–18 2011.
3. Szpyrka, M. and Matyasik, P. and Mrówka, R. and Witalec, W. and Baniewicz, J. and Balicki, K. Introduction to Alvis modelling language. In Measurement Automation and Monitoring (PAK) journal, year 2011, volume 57, number 9, pages 1086-1089.
4. Szpyrka, M. and Matyasik, P. and Mrówka, R. and Witalec, W. and Baniewicz, J. and Kotulski, L. Introduction to modelling embedded systems with Alvis. In Automatyka journal, year 2011, volume 15, number 2, pafes 435-442.

• dr hab. inż. Andrzej Karatkiewicz, prof. UZ Recenzja nr 1
• prof. dr hab. inż. Tomasz Szmuc Recenzja nr 2