Doktoraty Wydziału IET

mgr inż. Michał Wypych

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

Niniejsza rozprawa doktorska dotyczy metod weryfikacji formalnej i modelowania systemów rozproszonych w języku modelowania formalnego Alvis. W dzisiejszym świecie rozproszonych systemów komputerowych standardowe metody testowania zawodzą i nie są w stanie zagwarantować jakości i poprawności systemu współbieżnego. Problemy ze współbieżnością są z natury trudne do za modelowania i poprawnego rozwiązania z pominięciem problemów. Co więcej, błędy ze współbieżnym lub rozproszonym przetwarzaniem mogą ukrywać się podczas normalnego działania systemu i ujawniać się tylko wtedy, gdy system doświadcza skrajnie rzadkich scenariuszy. Metody formalne są szczególnie przydatne w weryfikacji systemów, które składają się ze współbieżnych lub rozproszonych jednostek przetwarzania, ponieważ umożliwiają wyczerpującą eksplorację wszystkich możliwych scenariuszy, nawet tych najrzadszych, z jakimi może się spotkać system w trakcie działania.

Język Alvis został zaprojektowany jako próba stworzenia formalnego języka modelowania, który byłby łatwy do nauki i użycia dla inżynierów oprogramowania. Aby osiągnąć ten cel, Alvis umożliwia określenie zachowania modeli w języku programowaniu wysokiego poziomu. Zależności pomiędzy rozproszonymi jednostkami są modelowane i wizualizowane w środowisku graficznym. Co więcej, różne scenariusze wykonania mogą być modelowane za pomocą różnych warstw systemowych. Jednym z głównych celów projektu Alvis jest umożliwienie formalnej i automatycznej weryfikacji dowolnych modeli.

Przed rozpoczęciem badań przedstawionych w niniejszej rozprawie Alvis był głównie projektem teoretycznym. Zaproponowano już podstawy matematyczne i udostępniono narzędzie umożliwiające graficzne modelowanie systemu. Brakowało natomiast narzędzia do automatycznej weryfikacji zaprojektowanego modelu, gdyż nie było narzędzia do konwersji model określonego w języku wysokiego poziomu do reprezentacji przystosowanej do weryfikacji modelowej. Jedna z takich reprezentacji to etykietowany system przejść (LTS).

Głównym celem niniejszej rozprawy było zaproponowanie, zaprojektowanie i wdrożenie narzędzia, które odpowiadałoby za automatyczne, szybkie i nienadzorowane generowanie etykietowanych systemów przejść na podstawie wysokopoziomowego opisu modelu w języku Alvis. Cel ten został osiągnięty dzięki stworzeniu kompilatora języka Alvis, który umożliwia generowanie LTS'ów składający się z $10^8$ stanów na przeciętnym współczesnym komputerze stacjonarnym. Cały proces jest realizowany zaledwie w ciągu kilku godzin. Kompilator generuje LTS w dwuetapowym podejściu, znanym z podobnych narzędzi. Pierwszym etapem jest stworzenie niejawnej reprezentacji LTS w języku ogólnego przeznaczenia - Haskell, znanym jako pośrednia reprezentacja w Haskellu (IHR). Drugi etap to kompilacja i uruchomienie programu IHR w celu utworzenia wynikowego grafu LTS. Proponowane podejście cechuje się ogromną elastycznością i wysoką ekspresywnością.

Cel rozprawy został osiągnięty z powodzeniem i porównany z dobrze znanym narzędziem do weryfikacji modelowej - Spin. Kompilator Alvisa osiąga podobną wydajność jak dobrze znane narzędzia.

Praca udostępniona publicznie:
Metody generowania etykietowanych systemów przejść dla języka Alvis.pdf

Recenzje:
dr hab. Bożena Woźna-Szcześniak, prof. UJD
dr hab. inż. Remigiusz Wiśniewski, prof. UZ

Ważniejsze publikacje doktoranta:

• Modelling and verification of real-time systems with Alvis / Marcin SZPYRKA, Łukasz PODOLSKI, Michał WYPYCH / W: Towards a synergistic combination of research and practice in software engineering : 19th KKIO software engineering conference (KKIO) : Rzeszow, Poland, September 14-16, 2017. — Switzerland : Springer, cop. 2018. — (Studies in Computational Intelligence; ISSN 1860-949X; vol. 733). — ISBN: 978-3-319-65207-8 — S. 165–178.
• Discrete-time systems modeling and verification with Alvis language and tools / Marcin SZPYRKA, Michał WYPYCH, Jerzy BIERNACKI, Łukasz PODOLSKI / IEEE Access [Dokument elektroniczny]. — Czasopismo elektroniczne ; ISSN 2169-3536. — 2018 vol. 6, s. 78766–78779. — Wymagania systemowe: Adobe Reader. — Bibliogr. s. 78778–78779
• Supporting BPMN process models with UML sequence diagrams for representing time issues and testing models / Anna Suchenia (Mroczek), Krzysztof KLUZA, Krystian JOBCZYK, Piotr WIŚNIEWSKI, Michał WYPYCH, Antoni LIGĘZA / W: Artificial Intelligence and Soft Computing : 16th International Conference : ICAISC 2017 Zakopane, Poland, June 11–15, 2017 : proceedings, Pt. 2 / eds. Leszek Rutkowski, [et al.]. — Switzerland : Springer International Publishing, cop. 2017. — (Lecture Notes in Computer Science; ISSN 0302-9743. Lecture Notes in Artificial Intelligence ; LNAI 10246). — Toż na Dysku Flash. — ISBN: 978-3-319-59059-2 ; e-ISBN: 978-3-319-59060-8. — S. 589–598. — Bibliogr. s. 597–598, Abstr.. — K. Jobczyk - dod. afiliacja: University of Caen, France
• Simulation of multi-agent systems with Alvis Toolkit / Marcin SZPYRKA, Piotr Matysiak, Łukasz PODOLSKI, Michał WYPYCH / W: Artificial Intelligence and Soft Computing : 16th International Conference : ICAISC 2017 Zakopane, Poland, June 11–15, 2017 : proceedings, Pt. 2 / eds. Leszek Rutkowski, [et al.]. — Switzerland : Springer International Publishing, cop. 2017. — (Lecture Notes in Computer Science ; ISSN 0302-9743. Lecture Notes in Artificial Intelligence ; LNAI 10246). — Toż na Dysku Flash. — ISBN: 978-3-319-59059-2 ; e-ISBN: 978-3-319-59060-8. — S. 599–608. — Bibliogr. s. 607–608, Abstr.
• A survey of Alvis communication modes / Marcin SZPYRKA, Jerzy BIERNACKI, Piotr MATYASIK, Michał WYPYCH / International Journal of Microelectronics and Computer Science ; ISSN 2080-8755. — 2017 vol. 8 no. 1, s. 1–9. — Bibliogr. s. 8–9, Abstr..
• Priority management in Alvis language / Marcin SZPYRKA, Agnieszka BIERNACKA, Jerzy BIERNACKI, Michał WYPYCH / W: MIXDES 2016 [Dokument elektroniczny] : Mixed Design of integrated circuits and systems : Łódź, Poland, June 23–25, 2016 : book of abstracts of 23rd international conference / ed. by Andrzej Napieralski. — Wersja do Windows. — Dane tekstowe. — Łódź : Lodz University of Technology. Department of Microelectronics and Computer Science, cop. 2016. — Dysk Flash. — e-ISBN: 978-8-3635-7808-4. — S. 131
• Hierarchical communication diagrams / Marcin SZPYRKA, Piotr MATYASIK, Jerzy BIERNACKI, Agnieszka BIERNACKA, Michał WYPYCH, Leszek KOTULSKI / Computing and Informatics / Slovak Academy of Sciences. Institute of Informatics ; ISSN 1335-9150. — Tytuł poprz.: Computers and Artificial Intelligence. — 2016 vol. 35 no. 1, s. 55–83. — Bibliogr. s. 80–82, Abstr.
• Communication between agents in Alvis language / Piotr MATYASIK, Marcin SZPYRKA, Michał WYPYCH, Jerzy BIERNACKI / W: MIXDES 2016 [Dokument elektroniczny] : Mixed Design of integrated circuits and systems : Łódź, Poland, June 23–25, 2016 : book of abstracts of 23\textsuperscript{rd} international conference / ed. by Andrzej Napieralski. — Wersja do Windows. — Dane tekstowe. — Łódź : Lodz University of Technology. Department of Microelectronics and Computer Science, cop. 2016. — Dysk Flash. — e-ISBN: 978-8-3635-7808-4. — S. 128
• Generation of Java code from Alvis model / Piotr MATYASIK, Marcin SZPYRKA, Michał WYPYCH / W: ICCMSE 2015 : International Conference of Computational Methods in Sciences and Engineering 2015 : Athens, Greece, 20–23 March 2015 / eds. Theodore E. Simos, Zacharoula Kalogiratou, Theodore Monovasilis. — [USA] : AIP Publishing LLC, 2015. — (AIP Conference Proceedings ; ISSN 0094-243X ; 1702). — ISBN: 978-0-7354-1349-8. — S. 100013-1–100013-4. — Bibliogr. s. 100013-4, Abstr.
• Extension of Alvis Compiler front-end / Michał WYPYCH, Marcin SZPYRKA, Piotr MATYASIK / W: ICCMSE 2015 : International Conference of Computational Methods in Sciences and Engineering 2015 : Athens, Greece, 20–23 March 2015 / eds. Theodore E. Simos, Zacharoula Kalogiratou, Theodore Monovasilis. — [USA] : AIP Publishing LLC, 2015. — (AIP Conference Proceedings ; ISSN 0094-243X ; 1702). — ISBN: 978-0-7354-1349-8. — S. 100015\-1–100015-4. — Bibliogr. s. 100015-4, Abstr.
• Generation of labelled transition systems for Alvis models using Haskell model representation / Marcin SZPYRKA, Piotr MATYASIK, Michał WYPYCH / W: CS&P'2013 [Dokument elektroniczny] : proceedings of the international workshop : Warsaw, 25–27 September 2013 / eds. Marcin Szczuka, Ludwik Czaja, Magdalena Kacprzak. — Wersja do Windows. — Dane tekstowe. — Białystok : Białystok University of Technology, 2013. — 1 dysk optyczny. — e-ISBN: 978-83-62582-42-6. — S. [1–12]. — Wymagania systemowe: Adobe Reader ; napęd CD-ROM. — Bibliogr. s. [11–12], Abstr.. — W bazie Scopus wersja wydana w ramach serii: CEUR Workshop Proceedings ; ISSN 1613-0073, vol. 1032 s. 409–420
• Alvis language with time dependence / Marcin SZPYRKA, Piotr MATYASIK, Michał WYPYCH / W: FedCSIS : abstracts of the Federated Conference on Computer Science and Information Systems : September 8–11, 2013, Kraków, Poland. — [Piscataway : IEEE], [2013]. — Opis częśc. wg okł.. — ISBN: 978-1-4673-4471-5. — S. 114. — Pełny tekst na dołączonym Dysku Flash. — S. 1615–1620. — Wymagania systemowe: Adobe Reader. — Bibliogr. s. 1620, Abstr.. — W bazie Web of Science wersja drukowana: 2013 Federated Conference on Computer Science and Information Systems. — ISBN 978-1-4673-4471-5. — S. 1565–1570