Doktoraty Wydziału IET

mgr inż. Jerzy Biernacki

Promotor: prof. dr hab. Marcin Szpyrka (AGH)
Dyscyplina: Informatyka

Przedstawiona rozprawa doktorska dotyczy metod formalnej weryfikacji modeli systemów wyspecyfikowanych w języku Alvis. Metody formalne mają szczególne zastosowanie w odniesieniu do systemów w stosunku do których oczekiwane jest zapewnienie bardzo wysokich gwarancji spełnienia wskazanych własności. Szczególnym przykładem są tutaj systemy krytyczne ze względu na bezpieczeństwo, których awarie lub błędy mogą mieć wpływ na życie lub zdrowie ludzi, środowisko naturalne czy też spowodować istotne straty ekonomiczne. Problemem większości popularnych metod formalnych jest jednak ich nieprzystępność dla przeciętnych inżynierów oprogramowania.

Język Alvis powstał w wyniku poszukiwań formalnego języka modelowania, który będzie łatwy w użytkowaniu dla inżynierów oprogramowania. W tym celu Alvis łączy w sobie zalety języków programowania wysokiego poziomu z graficznymi językami modelowania zależności pomiędzy komponentami (agentami) w systemach współbieżnych. Jednym z podstawowych założeń języka jest umożliwienie formalnej analizy modeli w nim utworzonych. Przed rozpoczęciem prac opisanych w niniejszej rozprawie, jedyną możliwością formalnej analizy modeli Alvis była weryfikacja w pakiecie CADP Evaluator. Ogromną wadą tego podejścia jest utrata przy eksporcie wszystkich informacji przechowywanych w stanach systemu, w tym w szczególności wartości zmiennych.

Celem rozprawy było zaproponowanie i implementacja alternatywnego podejścia do analizy, umożliwiającego skuteczną formalną weryfikację modeli Alvis w oparciu o stany, wykorzystując postać pośrednią modelu w języku Haskell. Postawiono również założenie, że proponowane podejście powinno umożliwiać analizę modeli o liczbie stanów przekraczającej 10^6, na sprzęcie dostępnym dla przeciętnego inżyniera w akceptowalnym przedziale czasu. Ponadto, aby ułatwić wykorzystanie rozwiązania, w ramach pracy miał zostać opracowany język zapytań umożliwiający intuicyjną weryfikację wybranych własności modeli, bez konieczności znajomości wewnętrznej reprezentacji modelu czy języka Haskell. Dodatkowo, opracowane w ramach pracy narzędzia miały rozszerzać opracowany już wcześniej proces, integrując się z istniejącym pakietem narzędzi Alvis.

Cele te zostały zrealizowane poprzez opracowanie i implementację języka zapytań Alvis Query Language, umożliwiającego weryfikację modelu operując na postaci IHR. Dodatkowo zaproponowane zostało komplementarne podejście do weryfikacji modeli w narzędziu nuXmv oraz rozszerzenie możliwości weryfikacji obu podejść, poprzez wykorzystanie chmur obliczeniowych.

Rozprawa zawiera także studium przypadków formalnej weryfikacji modeli systemów współbieżnych i czasu rzeczywistego przy wykorzystaniu proponowanych podejść. Na podstawie pomiarów zebranych podczas weryfikacji tych modeli przygotowana została analiza porównawcza opracowanych metod.

Praca udostępniona publicznie:
Zastosowanie paradygmatu funkcyjnego do formalnej analizy systemów modelowanych w języku Alvis.pdf

Recenzje:
dr hab. Bożena Woźna-Szcześniak, prof. UJD
dr hab. inż. Lesław Gniewek, prof. PRz

Ważniejsze publikacje doktoranta:

1. Szpyrka M., Wypych M., Biernacki J., Podolski Ł.: Discrete-time systems modeling and verification with Alvis language and tools. IEEE Access. ISSN 2169-3536. — 2018 vol. 6, s. 78766–78779.
2. Szpyrka M., Biernacki J., Matyasik P., Wypych M.: A survey of Alvis communication modes. International Journal of Microelectronics and Computer Science. ISSN 2080-8755. — 2017 vol. 8 no. 1, s. 1–9.
3. Szpyrka M., Biernacki J., Biernacka A.: Tools and methods for RTCP-nets modeling and verification. Archives of Control Sciences. ISSN 1230-2384. — 2016 vol. 26 no. 3, s. 339–365.
4. Szpyrka M., Biernacka A., Biernacki J., Wypych M.: Priority management in Alvis language. MIXDES 2016. e-ISBN: 978-8-3635-7808-4. — S. 131.
5. Szpyrka M., Matyasik P., Biernacki J., Biernacka A., Wypych M., Kotulski L.: Hierarchical communication diagrams. Computing and Informatics. ISSN 1335-9150. 2016 vol. 35 no. 1, s. 55–83.
6. Matyasik P., Szpyrka M., Wypych M., Biernacki J.: Communication between agents in Alvis language. MIXDES 2016. e-ISBN: 978-8-3635-7808-4. — S. 128.
7. Biernacki J.: Alvis models of safety critical systems state-base verification with nuXmv. FedCSIS : abstracts of the Federated Conference on Computer Science and Information Systems. ISBN: 978-836081090-3. — S. 124.
8. Biernacka A., Biernacki J., Szpyrka M.: State-based verification of RTCP-nets with nuXmv. ICCMSE 2015. ISBN: 978-0-7354-1349-8. — S. 100011-1–100011-4.
9. Biernacki J., Biernacka A., Szpyrka M.: Action-based verification of RTCP-nets with CADP. ICCMSE 2015. ISBN: 978-0-7354-1349-8. — S. 100010-1–100010-4.
10. Szpyrka M., Biernacka A., Biernacki J.: Methods of translation of Petri nets to NuSMV language. CEUR Workshop Proceedings. ISSN 1613-0073. — 2014 vol. 1269, s. 245–256.