Niezawodność systemów współbieżnych i obiektowych

seminaria magisterskie

Tematem seminarium są modele matematyczne, metody, algorytmy i narzędzia pozwalające na zwiększenie niezawodności oprogramowania.

Skupimy się przede wszystkim na analizie programów współbieżnych oraz obiektowych.

Centralną tematyką seminarium jest niezawodność systemów informatycznych, obejmująca takie aspekty systemu jak poprawność funkcjonalna, bezpieczeństwo, efektywność, jakość oprogramowania, itp. Naszą motywacją jest obserwowany ostatnio systematyczny wzrost zainteresowania przemysłu metodami pozwalającymi na zwiększenie niezawodność programów. Tematem seminarium są modele matematyczne, metody, algorytmy i narzędzia temu służące. Dalekosiężnym celem

seminarium jest opracowanie nowych metod i zbudowanie własnych narzędzi, np. w ramach doktoratu, więc serdecznie zapraszamy osoby

zainteresowane studiami doktoranckimi.

Ze względu na ich wagę i powszechność, koncentrujemy się przede wszystkim na dwóch kategoriach systemów informatycznych: (i) systemy

współbieżne i rozproszone; (ii) systemy obiektowe.

Tematyka seminarium obejmuje m.in.:

a. matematyczne modele systemów współbieżnych i rozproszonych (sieci Petriego, rozszerzone automaty, algebra procesów, itp.);

b. metody weryfikacji formalnej wspomaganej komputerowo: weryfikacja modelowa (ang. model checking), analiza statyczna, dowodzenie poprawności;

c. problemy decyzyjne w weryfikacji (np. bezpieczeństwo, żywotność, sprawiedliwość) -- algorytmy i złożoność obliczeniowa;

d. elementy teorii automatów (automaty czasowe, omega-automaty, itp);

e. narzędzia do weryfikacji.

* E.M. Clarke, O. Grumberg, D.A. Peled, Model Checking. MIT Press, 2002.

* B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen, P. McKenzie, Systems and Software Verification. Springer, 2001.

* C. Baier, J.-P. Katoen , Principles of Model Checking. MIT Press, 2008.

* K.R. Apt, E.-R. Olderog, Verification of Sequential and Concurrent Programs, Springer; 2nd edition (May 13, 1997)

* B. Beckert, R. Haehnle, P.H. Schmitt Verification of Object-Oriented Software. The KeY Approach, Springer; 1 edition (February 21, 2007)

Wiedza

Umiejętności

1. Posiada pogłębioną umiejętność przygotowania wystąpień ustnych, w języku polskim i języku obcym, w zakresie informatyki lub w obszarze leżącym na pograniczu różnych dyscyplin naukowych (K_U11).

2. Potrafi opisywać wybrane problemy informatyczne i ich rozwiązania w sposób zrozumiały dla nieinformatyka; potrafi przygotować prezentację (artykuł) z użyciem narzędzi informatycznych (K_U12).

3. Potrafi przygotować (także w języku angielskim) opracowanie naukowe z wybranej dziedziny informatyki (K_U13).

4. Ma umiejętności językowe w zakresie informatyki zgodne z wymaganiami określonymi dla poziomu B2+ Europejskiego Systemu Opisu Kształcenia Językowego (K_U14).

5. Potrafi określić kierunki dalszego uczenia się i zrealizować proces samokształcenia (K_U15).

Kompetencje

1. Zna ograniczenia własnej wiedzy i rozumie potrzebę dalszego kształcenia, w tym zdobywania wiedzy pozadziedzinowej (K_K01).

2. Potrafi precyzyjnie formułować pytania, służące pogłębieniu własnego zrozumienia danego tematu (w szczególności w kontaktach z nieinformatykiem) lub odnalezieniu brakujących elementów rozumowania (K_K02).

3. Potrafi pracować zespołowo, w tym w zespołach interdyscyplinarnych; rozumie konieczność systematycznej pracy nad wszelkimi projektami, które mają długofalowy charakter (K_K03).

4. Potrafi formułować opinie na temat podstawowych zagadnień informatycznych (K_K06).

5. Zna najważniejsze organizacje zawodowe w swoje dziedzinie (ACM, IEEE, PTI) i rozumie korzyści z członkostwa (K_K07).

6. Rozumie potrzebę systematycznego zapoznawania się z czasopismami naukowymi i popularnonaukowymi w celu poszerzania i pogłębiania wiedzy (K_K08).

7. Potrafi myśleć i działać w sposób przedsiębiorczy (K_K09).

Przedstawienie wymaganej liczby referatów, przesłanie (i ew. poprawienie wg uwag) ich wersji elektronicznej. Aktywność na zajęciach. Spełnienie warunków formalnych (zatwierdzenie tematu pracy magisterskiej na 1. roku, złożenie pracy magisterskiej na 2. roku).