Gömülü TV Yazılımı Modelinin Kontrolunde Ortaya Çıkan Durum Patlaması Problemine Çözüm Yaklaşımı

Abstract

Üniversitelerde yazılan makale sayıları gün geçtikçe daha da artıyor. Bunun yanında bilime ayrılan önem ve bütçe de gittikçe artıyor. Dolayısıyla artık neredeyse hergün bilimin ürünü olan yeni bir bilgi üretiliyor. Bunun sayesinde teknoloji de her zaman olduğundan daha da hızlı bir şekilde gelişmeye devam ediyor. Teknolojinin gelişmesi tüketici elektroniği sektörünün arkasındaki rüzgarı da arttırarak kullandığımız elektronik ürünlerin daha fonksiyonel ve işe yarar olmasına katkıda bulunuyor. 2007 yıllarında daha tüplü TV’ler kullanılıyorken, kimyasal ve elektronik araştırmalar neticesinde önce LCD ve Plazma daha sonra da LED TV’ler piyasaya sunuldu. Bu teknolojiler sayesinde TV panel kalınlıklarında dramatik bir düşüş meydana geldi ve TV’lerin gereksiz yer israfı bitti. Görüntüleme (display) teknolojilerindeki araştırmalar sonucu 3 boyutlu filmler hem sinemalarda hem de evde TV’lerde izlenmeye başladı. Bu konudaki araştırmalar ile TV’lerin 3 boyutlu yayınlardaki görünü derinliği ve görüntü kalitesi yazılan yeni algoritmalar ve görüntüleme tekniğindeki gelişmeler ile daha da arttı. Internet kullanımının artması ve yazılımsal gelişmeler sonucu internet TV’lerde de yer almaya başladı. Bu sayede TV’lerden internet sitelerine girilebilmeye, videolar filmler izlenebilmeye başlandı. Bluetooth teknolojisindeki gelişmeler ile TV’ler A2DP protokolünü kullanarak diğer bluetooth hoporlor cihazlara kablosuz ses iletmeye, AVRCP protokolünü kullanarak bu cihazlardan geribildirim almaya ve HID protokolünü kullanarak oyun konsolu vb… cihazlar ile kumanda edilmeye başlandı. TV’lere birden fazla tuner bağlanarak ve özel gözlükler kullanılarak iki farklı yayının aynı anda izlenebilmesi sağlandı. Full HD TV’lerin 4 katı çözünürlüğe sahip 4K paneller kullanılmaya başlandı. 2015 CES fuarında Sharp firması 8K panele sahip TVsini tanıttı. Yeni teknolojiler, firmalar arası rekabet ve artan talep doğrultusunda TV fonksiyonalitesi çok gelişti ve dolayısıyla TV’lerin gömülü sistem yazılımı çok büyüdü ve karmaşıklaştı. Dolayısıyla TV gömülü yazılımı test ve doğrulama sürecide daha da zorlaştı. Bu tez içerisinde TV gömülü yazılımı test ve doğrulama sürecinin hızlandırılabilmesi maksadıyla TV gömülü yazılım bileşenlerinin modellenerek, model üzerinde yapılacak sorgular ile test ve doğrulama sürecinde bir alternatif oluşturulması düşünüldü. Dolayısyla bu tez içerisinde TV gömülü sistem yazılımı ses ile ilgili kısımların bir kısmı SMV dili kullanılarak modellendi. Model içersinde TV’lerin genellikle kullanıcı ses menüsü altında bulunan bileşenler bu tez çalışması için kullanıldı.Model içerisinde gerçek bir kullanıcının modellenebilmesi maksadıyla deterministic olmayan bir kullanıcı (a nondeterministic user agent) modellendi. Deterministik olmayan kullanıcı modelimiz TV kumanda şablonunda belirtilen 35 adet tuşun herhangi birine herhangi bir zamanda basabilecek şekilde modellendi. Bununla birlikte modelde kullanılan TV ses bileşenleri şunlardır: * Kullanıcı seçimi doğrultusunda TV sesinin iyileştirilmesi için kullanılan “Sound Mode” bileşeni modele eklendi. * Gece geç vakitlerde kullanıcıların komşularını rahatsız etmeden TV izlemelerini ses seviyesinin otomatik minimize edilmesi ile sağlayan “Night Mode” bileşeni modele eklendi. * Bluetooth A2DP protokolü kullanılarak harici cihazlara kablosuz ses gönderme işlevini sağlayan “Bluetooth” bileşeni modele eklendi. • TV Ses performansının, TV’nin ayakta konumunda bulunmasına göre ya da duvara asılı konumda bulunmasına göre maksimize edilmesini sağlayan “TV Location” bileşeni eklendi. * HDMI kablosu üzerinden ters yönde ses gönderimini sağlayan “ARC” (Audio Return Channel) bileşeni modele eklendi. * TV Scart ses çıkışı seviyesinin ayarlanmasına olanak sağlayan “Scart Volume” bileşeni modele eklendi. * Birden fazla kanala sahip ses bilgisinin kaliteli bir biçimde harici ses sistemlerine aktarılmasında görev alan “Optic Out” bileşeni modele eklendi. * TV Ses ayarlarının fabrika ayarlarına ayarlanabilmesine olanak sağlayan “RestoreToDefault” bileşeni modele eklendi. * Modele eklenen TV giriş kaynakları şunlardır: HDMI (High Definition Multimedia Interface), SCART (Radio and Television Receiver Manufacturers' Association), Component ( YPbPr - Component Video), Cable (DVB-C), Terrestrial (DVB-T), Satellite (DVB-S), ATV(Analog TV), USB girişi (Universal Serial Bus) ve PC girişi. * Kanal geçiş mekanizması, sayısal ses yükselticinin, ses yollarının ve ses çözücülerinin ayarlanması ile ilgili kısımlar da modele eklendi. Tasarlanan model 48 GB hafızaya sahip 12 çekirdekli güçlü bir server bilgisayar üzerinde denendi. Modelden yaratılan durum uzayını belirten BDD’nin (Binary Decision Diagram) çapı bilgisini de verebilme yeteneğine sahip olan NuSMV Model denetçisi kullanıldı. Bu tez de çap ve model denetimi süreleri bilgileri üzerinde çalışma yapılarak BDD çapının ve model denetim sürelerinin azaltılması sağlandı. Bu tez de, modelin 2 adet Canlılık (Liveness) ve 2 adet Güvenlik (Safety) özellikleri kontrol edildi. Fakat NuSMV üzerinde koşulan sorguların çok fazla zaman alabildiği görüldü. Bu saatler bazından eğer model biraz daha büyütülürse günler bazına kadar bile çıkabilmektedir. Bunun nedeni durum uzayı patlaması (State-Space Explosion) problemidir. “State-Space Explosion” problemini çözmek amacıyla 3 adet yöntem geliştirildi ve bu tez de tanıtıldı. Bu problemin çözümünü içeren 3 adet yöntem içerisinde beşeri testçilerin manual testlerindeki TV kumanda tuşları geçmişini içeren TV logları üzerinde çalışıldı. Faklı model TVlerin kumanda tuş içerikleri arasındaki farklılıklardan dolayı bir şablon üzerinde karar kılındı ve bu şablon kullanıldı. Şablon içerisinde 35 adet TV kumanda tuşu bulunmaktadır. TV kumanda tuşu geçmişlerini içeren loglar şablonda belirlenen 35 farklı tuştan herhangi birilerini içerebilmektedir. Bu üç adet yöntem içerisinde, model içerisinde modellenmiş olan ve deterministik olmayan kullanıcı temsilinin yerine TV logları kullanılarak deterministic olmayan bir kullanıcı temsili oluşturulmaya çalışılmış ve sorgu süresi ve BDD çapı düşürülmeye çalışılmıştır. Tez içerisinde “State–Space Explosion” problemine çözüm olarak sunulan ilk yöntem “Direct log based specification” yaklaşımıdır. Bu yöntem içerisinde temsili kullanıcı direkt olarak TV logları kullanılarak oluşturulmaktadır. Bu yöntem içerisinde, log dosyası içerisinde belirtilen her kumanda tuşu bilgisi, kullanıcı modülünde ki herbir farklı durum geçişine dönüştürülmektedir. Bu yaklaşımda log dosyaları kullanıcı modülüne direkt olarak dönüştürülmektedir. Dolayısyla bu yaklaşımın avantajı olarak sorgu süresi ve durum uzayı BDD çapı düşürülmüştür. Fakat bu yaklaşımın dezavantajı olarak, modelde kullanılan kullanıcı modülü deterministik olmama özelliğini tamamen kaybederek tamamen deterministik olmuştur. Dolayısıyla kullanılan kullanıcı temsili, beşeri kullanıcı özelliklerinden tamamen uzaklaşmıştır. “Direct log based specification” yaklaşımının dezavantajı olan tamamen deterministik kullanıcı temsilinin, deterministik olmayan bir kullanıcı temsiline dönüştürülmesi ve dolayısyla beşeri bir kullanıcı davranışına yaklaşması amacıyla bu tezde ikinci yöntem “Injecting Non-determinism to Log Based Specification” geliştirildi ve tanıtıldı. Bu yaklaşımda log dosyası içerisindeki herbir tuş bilgisinin log dosyası içerisinde tekrar edilme frekansı hesaplanıyor. Her bir farklı tuş bilgisi eğer frekansı 1 ise, her bir farklı durum geçişine dönüştürülüyor. Eğer tuş bilgisinin frekansı 1’den yüksek ise, o tuş bilgisi deterministik olmayan bir durum geçişine dönüştürülüyor. Bu mantık ile deterministik olmayan bir kullanıcı temsili oluşturulmaya çalışıldı. Log dosyası kullanılarak deterministik olmayan bir kullanıcı temsili modellenmesi ve ayrıca sorgu süreleri ve BDD çapının düşürülmesi “Injecting Non-determinism to Log Based Specification” yaklaşımının avantajı olarak belirtildi. Farklı TV kullanıcıların kumanda tuşuna basma geçmişlerini içeren log dosyalarından oluşturulan kullanıcı temsili modullerinin birleştirilmesi ile elde edilen deterministik olmayan kullanıcı temsilinin modellenmesi içeren son metod “Combinin log based specifications” bu çalışmada geliştirildi ve bu tez de tanıtıldı. Bu yaklaşımda, iki adet log dosyasının içerisindeki tuş bilgilerinin frekansları kendi log dosyaları bazında hesaplandı. Herbir tuş, frekanslarına göre, diğer log dosyasından oluşturulan modelin durumlarına erişebilecek şekilde, deterministik olacak şekilde ve deterministik olmayacak şekilde durum geçişlerine modellendi. Tez de tanıtılan bu yaklaşım ile birlikte kullanıcı temsili modülünün deterministik olmama seviyesi daha da arttırıldı. Ayrıca, model üzerinde ki sorgu tamamlanma süresi ve BDD çapı düşürüldü. Bu tez içerisinde State- Space Explosion problemine çözüm olarak 3 adet yöntem geliştirilmiş ve sonuçları karşılaştırılmıştır.

Digital technology is developing rapidly. Thus the demand of new features for the TVs is increasing speedily. Besides, this increasing demand causes stronger competition. As a result of strong competition and increasing demand for the new features, embedded TV software of current TV sets is getting more complicated. Therefore, the test and verification process of the embedded TV software is getting harder. Logic of model checking is to algorithmically check if a model satisfies a specification. A model generally expressed as a directed graph including vertices and edges. The vertices specify the states of the model and the edges specify the state transitions due to a given condition. It is a widely accepted practice to use model checking in verification of embedded systems. On the other hand, it is seriously affected by the exponential increase in the number of states during the verification process. Modelling a fully non-deterministic TV-user is the one of the main reason for the exponential increase in the number of states. For the purpose of shrinking the state space being observed during the model checking process of TV, three methods are proposed in this thesis. TV logs are used to generate partly non-deterministic TV-user (user agent) models for all three methods that are proposed. The TV logs includes the Remote Controller (RC) keystroke histories recorded during the manual testing of the TV. The first method is “Direct Log Based Specification”. In this method, the user agent is designed directly from the TV log. The number of states are decreased in this method whereas the user agent model became fully deterministic. The second method is “Injecting non-determinism to Log Based Specifications”. In this methodthe first method is improved and a more non-determinictic user agent is produced according to the given TV log. The Third method is “Combining Log Based Specifications”. In this method we used two different TV logs to construct a more non-deterministic user-agent. Our results show that by using partly non-deterministic user agents we can significantly decrease the verification time of certain safety and liveness properties.