Seminarium Instytutu

Zapraszamy na seminarium w poniedziałek 10 marca w godz. 12:10-13:00 w sali 3/40. Dr Agnieszka Małgorzata Zbrzezny z Uniwersytetu Warmińsko-Mazurskiego w Olsztynie wygłosi referat na temat „Systemy współbieżne z czasem – modelowanie i weryfikacja”.

Streszczenie

Systemy współbieżne odgrywają bardzo ważną rolę we współczesnej informatyce. Znajdują one zastosowanie w systemach czasu rzeczywistego, systemach wieloagentowych, układach cyfrowych i protokołach bezpieczeństwa. Ich poprawne działanie jest istotne dla zapewnienia bezpieczeństwa i niezawodności wielu krytycznych zastosowań, takich jak wspomaganie kontroli ruchu lotniczego, w systemach stosowanych klinicznie, czy infrastruktura telekomunikacyjna.

W ramach wystąpienia zostaną omówione sposoby modelowania oraz metody weryfikacji tych systemów, ze szczególnym uwzględnieniem ograniczonej weryfikacji modelowej oraz ich zastosowania w analizie systemów wieloagentowych i protokołów bezpieczeństwa.

Pierwsza część wystąpienia będzie dotyczyła na wprowadzeniu do modelowania systemów współbieżnych z czasem. Przedstawione zostaną formalizmy, takie jak automaty z czasem [1] oraz czasowe systemy interpretowane [2], które umożliwiają precyzyjne modelowanie zachowań systemów. Następnie zostanie omówiona idea ograniczonej weryfikacji modelowej – automatycznej techniki sprawdzania poprawności działania systemów współbieżnych, oraz jej zastosowanie w analizie własności tychże systemów.

W drugiej części zostanie omówione jedno z autorskich narzędzi do weryfikacji protokołów bezpieczeństwa, VerSecTis [3], które umożliwia analizę zależności czasowych w protokołach i wykrywanie potencjalnych luk w ich bezpieczeństwie.

Wystąpienie zakończy podsumowanie dotychczasowych osiągnięć oraz perspektyw badawczych w obszarze weryfikacji modelowej systemów współbieżnych z uwzględnieniem czasu.

[1] Rajeev Alur, David L. Dill. A Theory of Timed Automata. Theoretical Computer Science, 126(2):183–235, 1994.
[2] Bożena Woźna-Szcześniak. Checking EMTLK properties of timed interpreted systems
via bounded model checking. Ana L. C. Bazzan, Michael N. Huhns, Alessio Lomuscio, Paul Scerri, redaktorzy, International conference on Autonomous Agents and Multi-Agent Systems, AAMAS ’14, Paris, France, May 5-9, 2014, strony 1477–1478. IFAAMAS/ACM, 2014.
[3] Agnieszka M. Zbrzezny, Andrzej Zbrzezny, Sabina Szymoniak, Olga Siedlecka-Lamch, Miroslaw Kurkowski. VerSecTis – an agent based model checker for security protocols. Amal El Fallah Seghrouchni, Gita Sukthankar, Bo An, Neil Yorke-Smith, redaktorzy, Proceedings of the 19th International Conference on Autonomous Agents and Multiagent Systems, AAMAS ’20, Auckland, New Zealand, May 9-13, 2020, strony 2123–2125. International Foundation for Autonomous Agents and Multiagent Systems, 2020.