Topic of PhD thesis 2014/2015

Advisor:Češka Milan, prof. RNDr., CSc.
Topic:Formal analysis and verification of systems specified by high-level visual languages
Start:2012/2013
PhD thesis subject:

Použití vysokoúrovňových vizuálních jazyků (např. Statecharts, Petri nets) v procesu modelem řízeného návrhu systémů je v současné době velmi aktuálním tématem (viz např. Executable UML). Naproti tomu současný trend ve formální analýze a verifikaci se dosud stále pragmaticky soustřeďuje na  nízkoúrovňové jazyky, protože na nich je postavena drtivá většina soudobých informačních technologií. Jako perspektivní se jeví možnost provádět verifikaci nikoliv na úrovni jazyků blízkých stroji, ale v pojmech velmi vysokoúrovňových vizuálních jazyků, které jsou bližší způsobu, jakým o systémech uvažuje člověk. Očekává se, že proces tvorby bezpečných systémů s využitím FAV na této úrovni bude efektivnější.
Předpokládá se použití existujících standardních verifikačních nástrojů, do kterých se budou překládat Petriho sítě (různých typů) a Statecharts.

Part of research project:
Related publications:
2011ČEŠKA Milan, FIEDOR Jan and GACH Marek. A Novel Approach to Modechart Verification of Real-Time systems. In: Proceedings of the 13th International Conference on Computer Aided Systems Theory. Universidad de Las Palmas de Canaria: The Universidad de Las Palmas de Gran Canaria, 2011, pp. 338-339. ISBN 978-84-693-9560-8.