Firma Y Soft ve spolupráci s LaBAK (Laboratoř bezpečnosti a aplikované kryptografie) vytváří nový komunikační protokol pro platební styk. Cílem této práce je zjistit potenciál různých přístupů k automatizované verifikaci protokolů platebního systému. Práce bude konzultována zástupcem firmy YSoft.

Konkrétními úkoly studentky je:

• nastudování dokumentace aktuálního návrhu protokolu,
• specifikace zamýšlených vlastností protokolu,
• nalezení a opravení nekonzistencí ve specifikaci,
• vypracování modelu platebního protokolu,
• analýza použitelnosti nástrojů k verifikaci vybraných vlastností,
• vybrání vhodného verifikačního nástroje a ověření správnosti modelu vzhledem k zamýšleným vlastnostem protokolu.

Literatura

• B. Berard, M. Bidoit, A. Finkel and F. Laroussinie. Systems and Software Verification: Model-Checking Techniques and Tools. Springer, 2001.
• C. Baier, J.P. Katoen, K.G. Larsen. Principles of Model Checking. The MIT Press, 2008.
• M. Bezděka, O. Bouda, Ľ. Korenčiak, M. Madzin, and V. Řehák. Sequence Chart Studio. In Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD'12), pages 148-153. IEEE, 2012.
• J. Barnat and L. Brim and M. Češka and P. Ročkai: DiVinE: Parallel Distributed Model Checker (Tool paper). Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi/PDMC 2010), IEEE, 2010, 4-7.

Práce je vypisována v rámci projektu OP VpK s názvem Platforma výzkumné a vzdělávací spolupráci FI MU v oblasti zpracování dat, reg. číslo CZ.1.07/2.4.00/12.0049, a aktivit SPP.