Gerçek Zaman Sistemlerinin Model Sınama ile Doğrulanması

                      Tolga Ovatman, İstanbul Teknik Üniversitesi



   Özet: Gerçek zaman sistemleri çoğu zaman kritik gereksinimlere sahip olan ve yüksek
   doğrulukla çalışması beklenen yazılım bileşenleri içermektedir. Bu nedenle gerçek zaman
   sistemlerinde kullanılan yazılımların biçimsel yöntemlerle modellenerek model sınama
   gibi yüksek kesinlik sağlayan yöntemlerle doğrulanması sıklıkla uygulanan bir
   yaklaşımdır. Bu oturumda, gerçek zamanlı modelleme yöntemlerinden biri olan zamanlı
   otomatlar ve zamanlı sistem gereksinimlerinin belirtimine imkan sağlayan CTL belirtim
   dili gözden geçirilerek gerçek zamanlı sistemlerin model sınaması üzerine bir genel bakış
   sunulacaktır. Oturumda, model sınama sürecinin temel özellikleri, bu kapsamda kullanılan
   temel yöntemler ve model sınama sürecinde karşılaşılan durum uzayı patlaması problemi
   tartışılacaktır. Sonrasında, literatürde sıklıkla kullanılan UPPAAL model sınama aracı ile
   örnekler sunularak diğer model sınama araçları ve kullanım alanları üzerine bilgiler
   verilecek, model sınama alanında güncel çalışmalar ve farklı uygulama alanları
   incelenecektir.



 Verification of Real-Time Systems Using Model Checking

                      Tolga Ovatman, İstanbul Teknik Üniversitesi



   Abstract: Real time systems usually contain software components that have critical
   requirements on working with high accuracy. Because of this reason, it is often the case
   that such components are modeled and then verified using formal methods that can provide
   guaranteed safety properties when applied correctly. In this session, a broad overview on
   formal verification by model checking will be provided using timed automata as means of
   real time system modeling formalism. Moreover, in order to demonstrate real time
   requirements specification computation tree logic variants will be discussed as time-logics
   to be used during model checking process. Discussion topics of the session includes basic
   elements of model checking process, methods applied in model checking and the problem
   of state space explosion that can be faced during model checking process. Additionally,
   example verification cases will be presented using UPPAAL model checker and
   contemporary model checkers will be overviewed to provide insight about the current
   practices and application areas on real time model checking approach.