Original title:
Návrh a implementace nástroje pro formální verifikaci systémů specifikovaných jazykem RT logiky
Translated title:
Design and Implementation of a Tool for Formal Verification of Systems Specified in RT-Logic Language
Authors:
Fiedor, Jan ; Straka, Martin (referee) ; Strnadel, Josef (advisor) Document type: Master’s theses
Year:
2009
Language:
cze Publisher:
Vysoké učení technické v Brně. Fakulta informačních technologií Abstract:
[cze][eng]
Protože komplexnost systémů pořád roste a s tím také riziko výskytu chyb, je potřeba tyto chyby efektivně a spolehlivě opravovat. U řady systémů reálného času tato potřeba platí dvojnásob, jelikož byť jediná chyba může způsobit jejich úplné zhroucení, které může mít katastrofální důsledky. Formální verifikace, na rozdíl od jiných metod, umožňuje spolehlivé ověřování požadavků kladených na určitý systém.
As systems complexity grows, so grows the risk of errors, that's why it's necessary to effectively and reliably repair those errors. With most of real-time systems this statement pays twice, because a single error can cause complete system crash which may result in catastrophe. Formal verification, contrary to other methods, allows reliable system requirements verification.
Keywords:
ANTLR; constraint graph; CORBA; design pattern; DFS; Formal verification; QF_UFIDL; Real-Time Logic; RTL; ANTLR; CORBA; DFS; Formální verifikace; graf omezení; Logika reálného času; návrhový vzor; QF_UFIDL; RTL
Institution: Brno University of Technology
(web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library. Original record: http://hdl.handle.net/11012/53893