Topic of PhD thesis

Advisor:Vojnar Tomáš, prof. Ing., Ph.D.
Student:Smrčka Aleš, Ing.
Topic:Verification of Modern Hardware Systems
Start:2003/2004
Date of Defense:2010-12-15
Title of Dissertation:Verification of Asynchronous and Parametrized Hardware Designs
PhD thesis subject:

Cílem výzkumu je další rozvoj pokročilých metod určených pro formální analýzu a verifikaci vlastností komplikovaných paralelních systémů s neomezenými řídicími či datovými strukturami, parametry, složitou a případně dynamicky proměnlivou architekturou, apod. Mezi systémy tohoto typu lze zahrnout například paralelní objektově-orientované programy či komunikační protokoly. Měly by být uvažovány metody založené na symbolické representaci stavových prostorů (např. při využití teorie jazyků a automatů), automatické abstrakci, redukci na konečné podproblémy, aj. Analyzované či verifikované systémy mohou být popsány pomocí různých modelovacích jazyků (objektově orientované Petriho sítě, sítě rozšířených automatů, vhodné programovací jazyky, atd.). Uvedený výzkum má charakter teoretického bádání s možným ověřením navrhovaných přístupů prototypovou implementací.

Part of research project:
Related publications:
2001ČEŠKA Milan, JANOUŠEK Vladimír and VOJNAR Tomáš. Generating and Using State Spaces of Object-Oriented Petri Nets. International Journal of Computer Systems Science and Engineering. 2001, vol. 16, no. 3, pp. 183-193. ISSN 0267-6192.
2000ČEŠKA Milan, JANOUŠEK Vladimír and VOJNAR Tomáš. Towards Verifying Distributed Systems Using Object-Oriented Petri Nets. Lecture Notes in Computer Science. 2000, vol. 2000, no. 1798, pp. 90-104. ISSN 0302-9743.