Doktoraty Wydziału IET

Ta strona jest tylko do odczytu. Możesz wyświetlić źródła tej strony ale nie możesz ich zmienić.
.


^   **DZIEKAN i RADA WYDZIAŁU**    \\    **INFORMATYKI, ELEKTRONIKI I TELEKOMUNIKACJI**    \\    **AKADEMII GÓRNICZO-HUTNICZEJ im. ST. STASZICA W KRAKOWIE**   ^^
|   zapraszają na    \\    publiczną dyskusję nad rozprawą doktorską    \\      \\   //mgr inż. Michała Wypycha//      \\                 ||
|  **Metody generowania etykietowanych systemów\\ przejść dla języka Alvis**  ||
^  Termin:|4 lutego 2022 roku o godz. 11:00  |
^  Miejsce:|Online: [[https://bit.ly/phd2022|link ]] |
^  **PROMOTOR:**|Prof. dr hab. Marcin Szpyrka, Akademia Górniczo-Hutnicza |
^  ** RECENZENCI:**|dr hab. Bożena Woźna-Szcześniak, prof. UJD, Uniwersytet Humanistyczno-Przyrodniczy im. Jana Długosza w Częstochowie  |
^  **            **|dr hab. inż. Remigiusz Wiśniewski, prof. UZ, Uniwersytet Zielonogórski |
|  Z rozprawą doktorską i opiniami recenzentów można się zapoznać \\ w Czytelni   Biblioteki Głównej AGH, al. Mickiewicza 30  ||


\\
----

\\

==== Methods of generation of transition systems for Alvis language ====
     
\\

//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:** 
\\
{{ :2022:micwypych:michal_wypych__metody_generowania_etykietowanych_systemow_przejsc_dla_jezyka_alvis.pdf | Metody generowania etykietowanych systemów przejść dla języka Alvis.pdf}} 
\\

 **Recenzje:** 
\\
{{ :2022:micwypych:recenzja-michal_wypych_prof_Wozna_Szczesniak.pdf | dr hab. Bożena Woźna-Szcześniak, prof. UJD}}
\\
{{ :2022:micwypych:recenzja_michal_wypych_prof_wisniewski.pdf | 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

----
Doktoraty Wydziału IET

Narzędzia użytkownika

Narzędzia witryny

Narzędzia strony
