=Paper=
{{Paper
|id=Vol-1483/66_Bildiri
|storemode=property
|title=Sayısal Almaç Planlayıcı Bileşeninin Biçimsel Doğrulanması
|pdfUrl=https://ceur-ws.org/Vol-1483/66_Bildiri.pdf
|volume=Vol-1483
|dblpUrl=https://dblp.org/rec/conf/uyms/DursunK15
}}
==Sayısal Almaç Planlayıcı Bileşeninin Biçimsel Doğrulanması==
<pdf width="1500px">https://ceur-ws.org/Vol-1483/66_Bildiri.pdf</pdf>
<pre>
    Saysal Almaç Planlayc Bile³eninin Biçimsel

                             Do§rulanmas


                      Mustafa DURSUN, Özgür KIZILAY


                     REHS EH Görev Yazlmlar Müdürlü§ü,

                         ASELSAN A.., Ankara, Türkiye

                       {mdursun,ozgurk}@aselsan.com.tr

    Özet Biçimsel do§rulama bir sistemin do§rulanmasnn tasarm a³amasnda
yaplmasna izin veren ve son yllarda kullanm hzla artan bir yöntemdir. Bu

bildiride almaç planlayc bile³eni tasarmnn gerçek zaman gereksinimleri da-

hil edilerek biçimsel do§rulanmas sunulmaktadr. Bu kapsamda saysal almaç

planlayc bile³eninin biçimsel modelinin ve gereksinimlerinin UPPAAL model

denetim arac ile belirtimi ve do§rulanmas ele alnmaktadr.

    Anahtar Kelimeler Model Denetim, Gerçek Zamanl Yazlm, Biçimsel
Do§rulama


1    GR
Elektronik taarruz [1, 2] i³levi için taarruz uygulanacak yaynlarn parametre-

lerinin izlenmesi ve güncellenmesi gerekmektedir. Hedef izleme i³levinin do§ru

ve verimli yaplabilmesi, izlemeyi sa§layan planlamann sistem kstlarna göre

dinamik olarak yaplmasna ve yaplan planlamann saysal almaçta [1] do§ru

zamanlamayla uygulanmasna ba§ldr. Almaç kontrol yazlmnn saysal almaç

planlayc bile³eni [3], hedef izleme i³levi kapsamnda dinamik olarak almaç plan-

lamann olu³turulmas ve olu³turulan planlama admlarnn uygulanmasn ger-

çekleyen gerçek-zamanl [4] yazlm kongürasyon birimidir. Almaç planlayc

bile³eni sistemin i³levsel ve zamansal gereksinimlerini sa§lamas amac ile za-

man tetikli özel bir durum ve görev tasarmna sahiptir. Saysal almaç planlayc

bile³eni, dinamik olarak tarama rejimi [3] olu³turmakta ve olu³turulan tarama

rejimlerinin admlarn saysal almaçta uygulamaktadr. Saysal almaç planlayc

bile³eninin do§rulu§u, tarama rejiminin saysal almaçta do§ru zamanlarda uygu-

lanmasna ve saysal almaç ile saysal almaç planlayc bile³eninin durum tutarl-

l§nn sa§lanmasna ba§ldr. Saysal almaç planlayc bile³eninin do§rulanmas

dinamik bir planlama yapmasndan, gerçek zaman kstlarna sahip olmasndan

ve almaç kontrol yazlmndaki di§er görevler ile ba§mll§nn bulunmasndan

dolay yüksek bir test maliyetine sahiptir. Bir yazlmn tasarm a³amasnda do§-

rulama yaplmasn, test maliyetini dü³ürecek bir etkendir. Yazlmlarn tasarm

a³amasnda do§rulanmasna imkan veren biçimsel do§rulama, yaygn olarak kul-

lanlan etkin bir yöntemdir [9].

    Bu bildiride saysal almaç planlayc bile³eninin biçimsel do§rulanmas su-

nulmaktadr. Bölüm 2'de biçimsel do§rulama ve model denetim anlatlmaktadr.

Bölüm 3'te almaç planlayc tasarm, sistem bile³eni modelleri ve sistem gerek-


                                       645
sinimlerinin biçimsel belirtimi sunulmaktadr. Bölüm 4'te ise de§erlendirme ve

sonuç sunulmu³tur.


2      BÇMSEL DORULAMA VE MODEL DENETM
Biçimsel do§rulama, sistem davran³nn sistem gereksinimlerine göre mateme-

tiksel modeller ve belirtimler kullanlarak do§rulanmasn sa§layan bir yöntem-

dir. Biçimsel do§rulamann en büyük avantaj tasarmn erken a³amalarda do§-

rulanmasna olanak sa§lamasdr. Model denetimi [5], biçimsel do§rulamay ger-

çekle³tiren otomatik bir tekniktir. Model denetimi, sistemin sonlu durum model-

lerinin biçimsel özellikleri (gereksinimleri) ile tutarll§n kontrol ederek biçimsel

do§rulamay gerçekle³tirir [6]. Biçimsel do§rulamay model denetim tekni§i ile

gerçekle³tirmek için sistemin biçimsel modeline, sistem gereksinimlerinin biçim-

sel belirtimine ve bir model denetim aracna ihtiyaç vardr. Biçimsel do§rulama-

nn etkinli§i sistem modeli ve belirtiminin do§rulu§una ba§ldr.

      Zaman-kritik ve gerçek-zamanl sistemlerin do§rulanmasnda sistemin i³levsel

do§rulu§unun yan sra zamansal özelliklerinin do§rulanmas da gerekmektedir.

Dolaysyla sistem davran³n belirten biçimsel modelde zamansal davran³larn

da belirtimi gerekmektedir. Zamanlanm³ otomatlar [7] gerçek zamanl sistem-

lerin davran³larn zaman kavram ile modellemek için kullanlan sonlu durum

otomatlardr. Zamanlanm³ otomatlar ile zaman kavramnn modellenmesi için

her bir otomata ait saat tanmlamak mümkümdür.

      UPPAAL [8] zamanlanm³ otomatlar kullanarak biçimsel do§rulama sa§la-

yan bir model denetim aracdr. UPPAAL ile bir sistemin modellenmesi, haber-

le³en zamanlanm³ otomatlar ile sa§lanr. Her bir zamanlanm³ otomat ko³ut

zamanl bir sistem bile³enini belirtir. Bu bile³enler gerçek zamanl bir sistemin

ayn i³lemcide yürütülen görevleri olabilece§i gibi farkl i³lemci ve FPGA'lerde

yürütülen sistem bile³enleri veya haberle³me protokolleri de olabilir. Zamanlan-

m³ otomatlar arasndaki senkronizasyon kanallar kullanlarak, haberle³me ise

payla³lan de§i³kenler ile sa§lanmaktadr. Buna ek olarak her bir otomat için

özel de§i³kenler de tanmlanabilmektedir. Zamanlanm³ otomatlarn haberle³-

mesi ve sistemde tanml saatlerin ilerleyi³i senkron olarak gerçekle³tirilir.


3      ALMAÇ PLANLAYICI BLEEN DORULANMASI
3.1     Almaç Planlayc Bile³eni Tasarm


Almaç planlayc bile³eni için i³levsel gereksinimler ³u ³ekildedir: Almaç planla-

yc bile³eni;


 1. Atanan yaynlar için tarama rejimini olu³turacaktr.

 2. Tarama rejimi admlarn almaçta uygulayacaktr.

 3. Yayn listesinde de§i³iklik oldu§u zaman mevcut tarama rejimini iptal edecek

      ve yeni bir tarama rejimi olu³turacaktr.


                                         646
      (a) Yayn listesi de§i³ikli§i tarama adm uyguland§ srada gerçekle³irse,

          yeni tarama rejimi uygulanan tarama adm bitti§inde olu³turulacak ve

          uygulanmaya ba³layacaktr.

 4. Tarama rejiminde tarama admlar arasnda en az anahtarlama süresi (400

      µs) kadar bo³luk olacaktr.
 5. Saysal almaçta bir tarama adm uygulanrken yeni bir tarama adm uygu-

      lanmayacaktr.


Tarama admlar, tarama rejimi dinamik olarak olu³turuldu§undan ve tarama

adm periyotlarnda gecikmeler olabilece§inden dolay periyodik görevler ile ta-

sarlanamamaktadr. Buna ek olarak i³lemci kartlarnda harici saat says snrl-

dr. Bundan dolay almaç planlayc bile³eni, tarama rejimi olu³turma ve uygu-

lama i³levlerini bir görevin ba§lamnda dizisel olarak zaman tetikli bir tasarmla

yürütmektedir. Almaç planlayc zaman gelen bir tarama admn uygulamak

için önce saysal almaca almaç ayarlama mesa jn gönderir. Almacn ayarland-

§na dair geribildirim mesa jn ald§nda ise kal³ süresini göndererek tarama ad-

mn ba³latr. Tarama admnn zaman geldi§inde tarama admn uygulamadan

önce admn kal³ süresi kadar saati kurar. Saat doldu§unda tarama rejiminde

bulunan bir sonraki tarama admnn ba³langç zamanna kadar saati yeniden

kurar. E§er ba³latlacak ba³ka bir tarama adm yoksa yeni bir tarama rejimini

olu³turur ve yeni tarama rejmini yürütmeye ba³lar. ekil 1 ard³k tarama adm-

larnn uygulanmasn göstermektedir.

      Tarama admlar arasndaki anahtarlama süresi boyunca sayssal almacn

ayarlanmas ve saysal almaçtan alnan DTK'larn yerel belle§e kopyalanmas

i³lemleri gerçekle³tirilir. Saysal almaç, gönderilen parametreler ile gerekli ayar-

lamalar gerçekle³tirir. Almaç ayarlama i³lemi belirli bir süre almaktadr. Buna

ek olararak DTKlarn yerel belle§e kopyalanmas da DTK saysna ba§l ola-

rak de§i³en bir süreye sahiptir. Yaplan ölçümler do§rultusunda bu i³lemler için

200   µs'lik süreler ayrlm³tr. Bu i³lemlerden herhangi birisinin beklenen süre-
den uzun sürmesi ard³k iki tarama adm uygulanrken ardl adm için yukarda

belirtilen 5. i³levsel gere§in yerine getirilememesine yol açar.


3.2     Sistem Modeli Belirtimi


Almaç planlayc bile³eninin do§rulanmas için sistem modeli almaç planlayc bi-

le³eninin hem i³levsel hem de zamansal davran³n belirtmelidir. Bu kapsamda

sistem modelinin sistemin i³levsel ve zamansal davran³larn belirtebilmesi için

saysal almaç, almaç kontrol ve sistem kontrol bile³enlerinin modellerinden olu³-

mas gerekmektedir. Denklem 1 sistemin bile³enlerini tanmlamaktadr.


                 S = CSayisalAlmac ||CAlmacKontrol ||CSistemKontrol             (1)


Almaç kontrol bile³eni almaç planlayc, denetleyici, algoritma, sistem kontrol

haberlesme (SistemKontHab) ve saysal almaç haberle³me (SayAlmacHab) bi-

le³enlerinin paralel bile³imidir. Denklem 2 almaç planlaycnn bile³enlerini gös-


                                        647
                  ekil 1: Tarama Admlar Mesaj Ak³ emas


termektedir.


  CAlmacKontrol = CDenetleyici ||CAlmacP lanlayici
                                    ||CAlgoritma ||CZamanlayici ||CSayAlmacHab   (2)


Saysal Almaç Modeli Saysal almaç modeli (ekil 2) taAlmacAyarla ile te-
tiklendi§inde saati almaç ayarlama süresine kurar. Zaman doldu§unda     taAlma-
cAyarlaACK 'i tetikler. taBasla ile tetiklendi§inde ise saati almaç kontrol yaz-
lmndan gönderilen kal³ süresine kurar. Kal³ süresi zaman doldu§unda almaç

kontrol yazlmn   taDTK ile tetikler.


Sistem Kontrol Modeli Sistem kontrol modeli (ekil 3) sistem kontrol yaz-
lmnn soyutlanm³ halidir. Sistem kontrol modeli    HIKomut ile almaç kontrol
bile³enini tetikleyerek en fazla iki yayn için hedef izleme ba³latr. Bu iki yayn

planlamalar arasnda anahtarlama süresi olacak kadar tanmlanm³tr.HIKo-
mutACK ile tetiklendikten sonra almaç kontrol bile³eninin üretti§i raporlar
almaya ba³lar. Daha sonra herhangi bir zamanda tüm yaynlar ya da bir yayn


                                           648
                            ekil 2: Saysal Almaç Modeli


için   HIKomut ile almaç kontrol bile³enini tetikleyerek almaç kontrol yazlmnda
mevcut yaynlar için tarama rejimi planlanr ve uygulanrken yayn listesi de§i-

³ikli§i gerçekle³tirilir.


                       ekil 3: Sistem Kontrol Bile³eni Modeli


Almaç Kontrol Denetleyici Modeli Almaç kontrol denetleyici modeli (ekil
4) yayn listesinde herhangi bir de§i³iklik oldu§u zaman sistem kontrol mode-

linden gönderilen    HIKomut ile tetiklenerek almaç planlayc modelinin duru-
muna göre mevcut tarama rejiminin durdurulmasn sa§lar. Almaç planlaycnn

tarama rejimini durdurmas ile gönderdi§i    PlanlamaDurdu ile tetiklendi§inde,
                                                           PlanlamaBaslat ile
e§er yayn listesinde halen izlenmesi gereken bir yayn varsa

planlamay tekrar ba³latr ve sistem kontrol modelinde HIKomutACK 'i tetikler.


Almaç Kontrol Almaç Planlayc Modeli Almaç planlayc modeli (ekil
5)   PlanlamaBaslat ile tetiklenerek tarama rejimi olu³turulmas ve uygulanma-
sn ba³latr.TAPLANLAMA durumuna geçerken mevcut yaynlar için tarama

                                        649
                      ekil 4: Denetleyici Bile³eni Modeli


                   ekil 5: Almaç Planlayc Bile³eni Modeli


rejimini olu³turur ve zaman ilk tarama admnn ba³langcna kurarak zamann

dolmasn bekler. Zaman doldu§unda planlanm³ tarama admnn biti³ süresine

zaman kurarak tarama admn uygulamaya ba³lar.      TAUYGULAMA durumuna
geçtikten sonra sras ile almac ayarlar ve almaçta tarama admnn kal³ süresi

kadar uygulanacak tarama admn ba³latr. Almaç planlayc modeli tarama ad-

mnn planlanan biti³ zaman geldi§inde sistem durumuna göre 3 farkl duruma

         TRBITTI durumuna tarama rejiminde uygulanacak ba³ka bir adm
geçebilir:

kalmad§nda, TAPLANLAMA durumuna tarama rejiminde uygulanacak ba³ka
admlar oldu§unda ve UYGDUR durumuna ise tarama adm uygulanrken ya-

yn listesi de§i³ikli§i gerçekle³ti§inde geçi³ yaplr. Almaç planlayc modelinde

PLANDUR durumuna tarama rejimindeki bir adm uygulanmad§ esnada yayn

                                       650
listesi de§i³ikli§i gerçekle³ti§i zaman geçilir ve 3. gereksinimi kar³lamak amac

ile e§er yayn listesi bo³ de§ilse yeni bir tarama rejimi olu³turulur. 3.a gereksinimi

kar³lamak amac ile tarama adm biti³ine dek herhangi ba³ka bir durum geçi³i

yoktur. Almaç planlayc modelinde    AYRIKSI durum 5. gereksinimi gerçeklemek
amac ile tanmlanm³tr. E§er almaçta uygulanan bir tarama adm mevcutken

yeni bir tarama admnn ba³latlmas söz konusu ise model     AYRIKSI durumuna
geçerek uygulanmaya çal³lan adm atlayarak tarama rejimindeki ardl adma

geçer.


Almaç Kontrol Saysal Almaç Haberle³me Bile³eni Modeli Saysal al-
maç haberle³me modeli (ekil 6) saysal almaçtan DTK'lar alnd§nda DTK'larn

yerel belle§e kopyalanmas için gereken DTK says ile de§i³en zamansal davra-

n³ modeller. Model   taDTK ile tetiklendikten sonra iMinDTKKopyalamaSuresi
ve iMaxDTKKopyalamaSuresi arasnda bir süre bekledikten sonra almac me³gul

durumundan çkartarak     taYerelDTK ' tetikler.


                   ekil 6: Almaç Haberle³me Bile³eni Modeli


                        ekil 7: Algoritma Bile³eni Modeli


Almaç Kontrol Algoritma Bile³eni Modeli                Algoritma modeli (ekil 7)

saysal almaçtan alnan DTK'lar ile çal³trlan algoritmalar modeller. Model


                                         651
taYerelDTK ile tetiklendikten sonra iMinAlgoritmaSuresi ve iMaxDTKAlgorit-
maSuresi arasnda bir süre bekledikten sonra rapor ile Sistem kontrol modelini

tetikler. Algoritmalarn yürütme süresi DTK says ve DTK'larn içeri§i ile de-

§i³ebilmektedir. iMinAlgoritmaSuresi ve iMaxDTKAlgoritmaSuresi de§i³kenleri

de§i³en bu süreyi belirtmektedir.


Zamanlayc Bile³eni Modeli Zamanlayc bile³eni modeli (ekil 8) µs çözü-
nürlükte bir zamanlayc modellemektedir. Zamanlayc modeli almaç planlayc

ve saysal almaç modelleri tarafndan sürelerin kurulmas için kullanlmaktadr.

Biçimsel do§rulama için sistem kongürasyonunda her iki modelin kullanm için

zamanlayc modelinin iki farkl örne§i kullanlmaktadr.

      UPPAAL aracnda bir do§al say en fazla 32768 de§erini alabildi§inden za-

man planlayc bile³eninin istenilen çözünürlü§ü elde etmek amac ile farkl bir

tasarma ihtiyac vardr. Bu amaçla Zamanlayc bile³eni   typedef struct{int s;
int ms; int us; }zaman_t; yapsn kullanr. Modelde zamann s ve ms de§erleri
için soldaki döngü kullanlrken, µs de§erler için sa§daki döngü kullanlr.


                       ekil 8: Zamanlayc Bile³eni Modeli


3.3     Sistem Özellikleri Belirtimi


Model denetim ile biçimsel do§rulamada modellenen sistem davran³nn sistem

özelliklerini kar³layp kar³lamad§ denetlenir. Sistem davran³ sistem mode-

linde belirtilen e³ zamanl bile³enlerin durumlarnn küresel bir durum uzayna

çevrilmesi ile olu³turulur. Model denetimi ile küresel durum uzayndaki her bir

durumun belirtilen sistem özelli§ini sa§layp sa§lamad§ kontrol edilir. Bu kap-

samda Bölüm 3.1'da tanml sistem gereksinimlerinin denetimi için bu gerek-

sinimlerin belirtimi gerekmektedir. Bu belirtimler almaç planlayc bile³eninin

do§rulanmasnda iki ksma ayrlm³tr. Birinci ksm sistem davran³nn her-

hangi bir kilitlenme olmadan i³ledi§inin denetlendi§i 1. ve 2. sistem gereksinim-

lerinin belirtimini içermektedir. kinci ksm ise almaç planlayc özelinde 3., 4. ve

5. sistem gereksinimlerinin belirtimini içermektedir. Sistem özellikleri belirtimi

a³a§da gösterilmi³tir.


                                         652
 1. (a) A[] not deadlock
    (b) E<> pPlanlayici.TROLUSTURMA
    (c) E<> pPlanlayici.TAPLANLAMA

    (d) E<> pPlanlayici.TAUYGULAMA

    (e) E<> pPlanlayici.TRBITTI

 2. (a) A[] PlanlayiciDurum!=AYRIKSI

    (b) pPlanlayici.UYGDUR>pSISKI.DUR

    (c) pPlanlayici.PLANDUR>pSISKI.DUR


    Model denetiminde 1.a özelli§inin sa§lanmas sistem davran³nn herhangi

bir kilitlenme olmadan çal³abildi§inin do§rulanmasn gösteririr. 1.b.'den 1.e.'ye

kadar olan özellikler model denetimi esnasnda almaç planlayc modelindeki

TROLUSTURMA, TAPLANLAMA, TAUYGULAMA ve TRBITTI durumla-
rna geçi³lerin oldu§unu ve durumlarn ula³labilirli§inin do§ruland§n gösterir.

           planlayici bile³enin PlanlaycDurum de§i³keninin hiçbir sistem
2.a özelli§i ile

      AYRIKSI de§erini almad§n ve dolays ile planlayici bile³enin TA-
durumda

AYRIKSI durumuna geçmedi§ini ifade eder. Bu özelli§in sa§lanmas anahtar-
lama süresinin yeterli uzunlukta oldu§unun do§ruland§n gösterir. Bu özelli§in

sa§lanamamas saysal almaçta mevcut bir tarama adm uygulanrken yeni bir

tarama admnn saysal almaçta planland§n ve 4. gereksinimin sistemin za-

                                                                     Planlayici
mansal kstlar ile uyumlu olmad§n gösterir. 2.b ve 2.c özellikleri

bile³eninin UYGDUR ve PLANDUR durumlarna eri³tikten sonra Sistem Kont-
rol bile³eninin DUR durumuna geçece§ini ifade eder. Bu özelliklerin sa§lanmas
ise 3. sistem gereksiniminin do§ruland§n gösterir.


4    DEERLENDRME VE SONUÇ
Biçimsel do§rulama bir sistemin gereksinimlerine göre do§rulanmasna tasarm

gibi erken a³amalarda olanak sa§layan matematiksel temele sahip bir do§rulama

yöntemdir. Bu bildiride almaç kontrol yazlmnn temel bile³eni olan almaç plan-

layc bile³eninin model denetim kullanlarak biçimsel do§rulanmas sunulmu³-

tur. Almaç planlayc bile³eni i³levsel ve zamansal gereksinimleri birlikte yerine

getirmesi gereken gerçek-zamanl bir yazlm bile³enidir. Almaç planlayc do§-

rulamasnn yaplmas için, almaç planlayc davran³ modeli çevresel bile³en ve

görevlerin davran³lar ile birlikte modellenmi³, sistem gereksinimlerinin mete-

matiksel özellikler ile belirtimi yaplm³ ve model denetim uygulanm³tr. Za-

mansall§n modellenmesi için ise sistemin çözünürlük gereksinimleri göz önünde

tutularak bir zamanlayc modeli olu³turulmu³tur.

    Model denetimi ko³ut zamanl davran³ modellerinin tüm durumlarnn sis-

tem özellikleri ba§lamnda denenmesine dayanr. Bundan dolay model dene-

timinde çok sayda ko³ut zamanl model olmas durum uzay patlamasna yol

açabilir. Almaç planlayc bile³eni do§rulanmasndaki zamansall§n modellen-

mesinde sistemin zamansal belirtimleri içinde mikrosaniye çözünürlü§ün çok dü-

³ük olmasndan dolay bu sorun ile kar³la³lmakta ve do§rulama süreci uzun

sürebilmektedir.


                                       653
   Sistem modelinde modellenmi³ denetleyici, algoritma, saysal almaç haber-

le³me ve almaç planlayc bile³enleri almaç kontrol yazlmnda birer görev olarak

tasarlanmaktadr. Bu görevler ayn i³lemci kayna§n kullanmakta ve bir görevin

i³lemciyi kullanmas di§er görevlerin yürütülmesinde gecikmeye yol açabilmekte-

dir. Almaç planlayc bile³eni en yüksek öncelikli görev olarak tasarland§ndan

di§er görevlerin bu görevde herhangi bir gecikmeye yol açmas mümkün de§ildir.

Almaç planlayc bile³enin biçimsel do§rulanmas açsndan bu durumun yapl-

m³ do§rulamaya olumsuz bir etkisi yoktur. Ancak algoritma süreleri ile ilgili

gereksinimlerin de do§rulanmasnn yaplmas için görevlerin birbirleri ile olan

etkile³imleri do§rulama srasnda dikkate alnmaldr. Bu açdan gelecekte i³le-

tim sistemi (vxWorks) ve geli³tirme ortam (UML-Rhapsody) davran³larnn

belirtimlerine sistem modelinde yer verilmesi gerekmektedir.

   Makalede sunulan sistem modeli ve özellikleri ile almaç planlayc bile³eninin

biçimsel do§rulamas gerçeklenmi³tir. Bu biçimsel do§rulama sürecinde görülen

ancak testlerde görülemeyen 3. gereksinim ile ilgili baz durumlar tasarma ek-

lenmi³ ve ciddi bir fayda elde edilmi³tir.


Kaynaklar
 1. F. Neri, "Inroduction to Electronic Defense Systems", 2nd ed., MA, USA:Artech

    House, 2006.

 2. Ç. Turan, G. Kahraman, C. Uzuno§lu, "RFKS Yazlm Mimarisi ve Arka Plan

    Yönetimi", TTD Konferans,2012.

 3. M. Dursun, Ö. Kzlay, "Zaman Tetikli Almaç Planlayc Yazlm Bile³eni Tasa-

    rm", UYMS, 2014.

 4. Jane W.S. Lui, Real-Time Systems,Prentice Hall,2000

 5. E. M.Clarke, ,O. Jr. Grumberg, D. A. Peled, "Model Checking". s.l. : The MIT

    Press, 1999.

 6. C. Baier, J. P. Katoen, "Principles of Model Checking", The MIT Press, 2008

 7. R. Alur, D. L. Dill, " A Theory of Timed Automata", Theoritical Computer Science

    126.2, 1994

 8. J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, W. Yi. "UPPAAL - A Tool

    Suite for the Automatic Verication of Real-Time Systems", Hybrid Systems III,

    LNCS 1066, pages 232-243. Springer-Verlag, 1996

 9. B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebe-

    len, "Systems and Software Verication: Model-Checking Techniques and Tools",

    Springer Publishing Company, Incorporated, 2010


                                          654

</pre>