Burcu Külahçıoğlu, “Analysis of Real Time Systems using Timed Automata”, 05 Ocak 2012

Bilgisayar Mühendisliği Bölümü Semineri:

	Başlık:	Analysis of Real Time Systems using Timed Automata
	Konuşmacı:	Burcu Külahçıoğlu, Yaşar Üniversitesi, Bilgisayar Müh. Böl.
	Tarih:	05 Ocak 2012
	Saat:	16:30-18:00
	Yer:	Bilgisayar Ağları Laboratuvarı
	Sunum Dili:	İngilizce

Timed Automata introduces time into the classical automata and allows for modeling of time sensitive properties. Correct functioning of real time systems depend on the timing properties, thus including time into the modeling and verification of these systems is necessary to guarantee their correctness. This study presents the use of model checking timed automata for the analysis of real time systems in two different areas. First, its use as a verification tool for real time systems is analyzed on a case study on Neuman-Stubblebine Repeated Authentication Protocol. The flaws of the protocol are examined and it is commented on the benefits and challenges of the model. Then, a novel approach to the worst case execution time (WCET) analysis using model checking is briefly introduced by reviewing recent studies on this direction.