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.
Ö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.