Saysal Almaç Planlayc Bile³eninin Biçimsel Do§rulanmas Mustafa DURSUN, Özgür KIZILAY REHS EH Görev Yazlmlar Müdürlü§ü, ASELSAN A.“., Ankara, Türkiye {mdursun,ozgurk}@aselsan.com.tr Özet Biçimsel do§rulama bir sistemin do§rulanmasnn tasarm a³amasnda yaplmasna izin veren ve son yllarda kullanm hzla artan bir yöntemdir. Bu bildiride almaç planlayc bile³eni tasarmnn gerçek zaman gereksinimleri da- hil edilerek biçimsel do§rulanmas sunulmaktadr. Bu kapsamda saysal almaç planlayc bile³eninin biçimsel modelinin ve gereksinimlerinin UPPAAL model denetim arac ile belirtimi ve do§rulanmas ele alnmaktadr. Anahtar Kelimeler Model Denetim, Gerçek Zamanl Yazlm, Biçimsel Do§rulama 1 GR“ Elektronik taarruz [1, 2] i³levi için taarruz uygulanacak yaynlarn parametre- lerinin izlenmesi ve güncellenmesi gerekmektedir. Hedef izleme i³levinin do§ru ve verimli yaplabilmesi, izlemeyi sa§layan planlamann sistem kstlarna göre dinamik olarak yaplmasna ve yaplan planlamann saysal almaçta [1] do§ru zamanlamayla uygulanmasna ba§ldr. Almaç kontrol yazlmnn saysal almaç planlayc bile³eni [3], hedef izleme i³levi kapsamnda dinamik olarak almaç plan- lamann olu³turulmas ve olu³turulan planlama admlarnn uygulanmasn ger- çekleyen gerçek-zamanl [4] yazlm kongürasyon birimidir. Almaç planlayc bile³eni sistemin i³levsel ve zamansal gereksinimlerini sa§lamas amac ile za- man tetikli özel bir durum ve görev tasarmna sahiptir. Saysal almaç planlayc bile³eni, dinamik olarak tarama rejimi [3] olu³turmakta ve olu³turulan tarama rejimlerinin admlarn saysal almaçta uygulamaktadr. Saysal almaç planlayc bile³eninin do§rulu§u, tarama rejiminin saysal almaçta do§ru zamanlarda uygu- lanmasna ve saysal almaç ile saysal almaç planlayc bile³eninin durum tutarl- l§nn sa§lanmasna ba§ldr. Saysal almaç planlayc bile³eninin do§rulanmas dinamik bir planlama yapmasndan, gerçek zaman kstlarna sahip olmasndan ve almaç kontrol yazlmndaki di§er görevler ile ba§mll§nn bulunmasndan dolay yüksek bir test maliyetine sahiptir. Bir yazlmn tasarm a³amasnda do§- rulama yaplmasn, test maliyetini dü³ürecek bir etkendir. Yazlmlarn tasarm a³amasnda do§rulanmasna imkan veren biçimsel do§rulama, yaygn olarak kul- lanlan etkin bir yöntemdir [9]. Bu bildiride saysal almaç planlayc bile³eninin biçimsel do§rulanmas su- nulmaktadr. Bölüm 2'de biçimsel do§rulama ve model denetim anlatlmaktadr. Bölüm 3'te almaç planlayc tasarm, sistem bile³eni modelleri ve sistem gerek- 645 sinimlerinin biçimsel belirtimi sunulmaktadr. 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³nn sistem gereksinimlerine göre mateme- tiksel modeller ve belirtimler kullanlarak do§rulanmasn sa§layan bir yöntem- dir. Biçimsel do§rulamann en büyük avantaj tasarmn erken a³amalarda do§- rulanmasna olanak sa§lamasdr. 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 tutarll§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 aracna ihtiyaç vardr. Biçimsel do§rulama- nn etkinli§i sistem modeli ve belirtiminin do§rulu§una ba§ldr. Zaman-kritik ve gerçek-zamanl sistemlerin do§rulanmasnda sistemin i³levsel do§rulu§unun yan sra zamansal özelliklerinin do§rulanmas da gerekmektedir. Dolaysyla sistem davran³n belirten biçimsel modelde zamansal davran³larn da belirtimi gerekmektedir. Zamanlanm³ otomatlar [7] gerçek zamanl sistem- lerin davran³larn zaman kavram ile modellemek için kullanlan sonlu durum otomatlardr. Zamanlanm³ otomatlar ile zaman kavramnn modellenmesi için her bir otomata ait saat tanmlamak mümkümdür. UPPAAL [8] zamanlanm³ otomatlar kullanarak biçimsel do§rulama sa§la- yan bir model denetim aracdr. UPPAAL ile bir sistemin modellenmesi, haber- le³en zamanlanm³ otomatlar ile sa§lanr. 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 arasndaki senkronizasyon kanallar kullanlarak, haberle³me ise payla³lan de§i³kenler ile sa§lanmaktadr. Buna ek olarak her bir otomat için özel de§i³kenler de tanmlanabilmektedir. Zamanlanm³ otomatlarn haberle³- mesi ve sistemde tanml saatlerin ilerleyi³i senkron olarak gerçekle³tirilir. 3 ALMAÇ PLANLAYICI BLE“EN DO‡RULANMASI 3.1 Almaç Planlayc Bile³eni Tasarm Almaç planlayc bile³eni için i³levsel gereksinimler ³u ³ekildedir: Almaç planla- yc bile³eni; 1. Atanan yaynlar için tarama rejimini olu³turacaktr. 2. Tarama rejimi admlarn almaçta uygulayacaktr. 3. Yayn listesinde de§i³iklik oldu§u zaman mevcut tarama rejimini iptal edecek ve yeni bir tarama rejimi olu³turacaktr. 646 (a) Yayn listesi de§i³ikli§i tarama adm uyguland§ srada gerçekle³irse, yeni tarama rejimi uygulanan tarama adm bitti§inde olu³turulacak ve uygulanmaya ba³layacaktr. 4. Tarama rejiminde tarama admlar arasnda en az anahtarlama süresi (400 µs) kadar bo³luk olacaktr. 5. Saysal almaçta bir tarama adm uygulanrken yeni bir tarama adm uygu- lanmayacaktr. Tarama admlar, tarama rejimi dinamik olarak olu³turuldu§undan ve tarama adm periyotlarnda gecikmeler olabilece§inden dolay periyodik görevler ile ta- sarlanamamaktadr. Buna ek olarak i³lemci kartlarnda harici saat says snrl- dr. Bundan dolay almaç planlayc bile³eni, tarama rejimi olu³turma ve uygu- lama i³levlerini bir görevin ba§lamnda dizisel olarak zaman tetikli bir tasarmla yürütmektedir. Almaç planlayc zaman gelen bir tarama admn uygulamak için önce saysal almaca almaç ayarlama mesa jn gönderir. Almacn ayarland- §na dair geribildirim mesa jn ald§nda ise kal³ süresini göndererek tarama ad- mn ba³latr. Tarama admnn zaman geldi§inde tarama admn uygulamadan önce admn kal³ süresi kadar saati kurar. Saat doldu§unda tarama rejiminde bulunan bir sonraki tarama admnn ba³langç zamanna kadar saati yeniden kurar. E§er ba³latlacak ba³ka bir tarama adm yoksa yeni bir tarama rejimini olu³turur ve yeni tarama rejmini yürütmeye ba³lar. “ekil 1 ard³k tarama adm- larnn uygulanmasn göstermektedir. Tarama admlar arasndaki anahtarlama süresi boyunca sayssal almacn ayarlanmas ve saysal almaçtan alnan DTK'larn yerel belle§e kopyalanmas i³lemleri gerçekle³tirilir. Saysal almaç, gönderilen parametreler ile gerekli ayar- lamalar gerçekle³tirir. Almaç ayarlama i³lemi belirli bir süre almaktadr. Buna ek olararak DTKlarn yerel belle§e kopyalanmas da DTK saysna ba§l ola- rak de§i³en bir süreye sahiptir. Yaplan ölçümler do§rultusunda bu i³lemler için 200 µs'lik süreler ayrlm³tr. Bu i³lemlerden herhangi birisinin beklenen süre- den uzun sürmesi ard³k iki tarama adm uygulanrken ardl adm için yukarda belirtilen 5. i³levsel gere§in yerine getirilememesine yol açar. 3.2 Sistem Modeli Belirtimi Almaç planlayc bile³eninin do§rulanmas için sistem modeli almaç planlayc bi- le³eninin hem i³levsel hem de zamansal davran³n belirtmelidir. Bu kapsamda sistem modelinin sistemin i³levsel ve zamansal davran³larn belirtebilmesi için saysal almaç, almaç kontrol ve sistem kontrol bile³enlerinin modellerinden olu³- mas gerekmektedir. Denklem 1 sistemin bile³enlerini tanmlamaktadr. S = CSayisalAlmac ||CAlmacKontrol ||CSistemKontrol (1) Almaç kontrol bile³eni almaç planlayc, denetleyici, algoritma, sistem kontrol haberlesme (SistemKontHab) ve saysal almaç haberle³me (SayAlmacHab) bi- le³enlerinin paralel bile³imidir. Denklem 2 almaç planlaycnn bile³enlerini gös- 647 “ekil 1: Tarama Admlar Mesaj Ak³ “emas termektedir. CAlmacKontrol = CDenetleyici ||CAlmacP lanlayici ||CAlgoritma ||CZamanlayici ||CSayAlmacHab (2) Saysal Almaç Modeli Saysal 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- lmndan gönderilen kal³ süresine kurar. Kal³ süresi zaman doldu§unda almaç kontrol yazlmn taDTK ile tetikler. Sistem Kontrol Modeli Sistem kontrol modeli (“ekil 3) sistem kontrol yaz- lmnn soyutlanm³ halidir. Sistem kontrol modeli HIKomut ile almaç kontrol bile³enini tetikleyerek en fazla iki yayn için hedef izleme ba³latr. Bu iki yayn planlamalar arasnda anahtarlama süresi olacak kadar tanmlanm³tr.HIKo- mutACK ile tetiklendikten sonra almaç kontrol bile³eninin üretti§i raporlar almaya ba³lar. Daha sonra herhangi bir zamanda tüm yaynlar ya da bir yayn 648 “ekil 2: Saysal Almaç Modeli için HIKomut ile almaç kontrol bile³enini tetikleyerek almaç kontrol yazlmnda mevcut yaynlar için tarama rejimi planlanr ve uygulanrken yayn 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) yayn listesinde herhangi bir de§i³iklik oldu§u zaman sistem kontrol mode- linden gönderilen HIKomut ile tetiklenerek almaç planlayc modelinin duru- muna göre mevcut tarama rejiminin durdurulmasn sa§lar. Almaç planlaycnn tarama rejimini durdurmas ile gönderdi§i PlanlamaDurdu ile tetiklendi§inde, PlanlamaBaslat ile e§er yayn listesinde halen izlenmesi gereken bir yayn varsa planlamay tekrar ba³latr ve sistem kontrol modelinde HIKomutACK 'i tetikler. Almaç Kontrol Almaç Planlayc Modeli Almaç planlayc modeli (“ekil 5) PlanlamaBaslat ile tetiklenerek tarama rejimi olu³turulmas ve uygulanma- sn ba³latr.TAPLANLAMA durumuna geçerken mevcut yaynlar için tarama 649 “ekil 4: Denetleyici Bile³eni Modeli “ekil 5: Almaç Planlayc Bile³eni Modeli rejimini olu³turur ve zaman ilk tarama admnn ba³langcna kurarak zamann dolmasn bekler. Zaman doldu§unda planlanm³ tarama admnn biti³ süresine zaman kurarak tarama admn uygulamaya ba³lar. TAUYGULAMA durumuna geçtikten sonra sras ile almac ayarlar ve almaçta tarama admnn kal³ süresi kadar uygulanacak tarama admn ba³latr. Almaç planlayc modeli tarama ad- mnn planlanan biti³ zaman geldi§inde sistem durumuna göre 3 farkl duruma TRBITTI durumuna tarama rejiminde uygulanacak ba³ka bir adm geçebilir: kalmad§nda, TAPLANLAMA durumuna tarama rejiminde uygulanacak ba³ka admlar oldu§unda ve UYGDUR durumuna ise tarama adm uygulanrken ya- yn listesi de§i³ikli§i gerçekle³ti§inde geçi³ yaplr. Almaç planlayc modelinde PLANDUR durumuna tarama rejimindeki bir adm uygulanmad§ esnada yayn 650 listesi de§i³ikli§i gerçekle³ti§i zaman geçilir ve 3. gereksinimi kar³lamak amac ile e§er yayn listesi bo³ de§ilse yeni bir tarama rejimi olu³turulur. 3.a gereksinimi kar³lamak amac ile tarama adm biti³ine dek herhangi ba³ka bir durum geçi³i yoktur. Almaç planlayc modelinde AYRIKSI durum 5. gereksinimi gerçeklemek amac ile tanmlanm³tr. E§er almaçta uygulanan bir tarama adm mevcutken yeni bir tarama admnn ba³latlmas söz konusu ise model AYRIKSI durumuna geçerek uygulanmaya çal³lan adm atlayarak tarama rejimindeki ardl adma geçer. Almaç Kontrol Saysal Almaç Haberle³me Bile³eni Modeli Saysal al- maç haberle³me modeli (“ekil 6) saysal almaçtan DTK'lar alnd§nda DTK'larn yerel belle§e kopyalanmas için gereken DTK says ile de§i³en zamansal davra- n³ modeller. Model taDTK ile tetiklendikten sonra iMinDTKKopyalamaSuresi ve iMaxDTKKopyalamaSuresi arasnda 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) saysal almaçtan alnan DTK'lar ile çal³trlan algoritmalar modeller. Model 651 taYerelDTK ile tetiklendikten sonra iMinAlgoritmaSuresi ve iMaxDTKAlgorit- maSuresi arasnda bir süre bekledikten sonra rapor ile Sistem kontrol modelini tetikler. Algoritmalarn yürütme süresi DTK says ve DTK'larn içeri§i ile de- §i³ebilmektedir. iMinAlgoritmaSuresi ve iMaxDTKAlgoritmaSuresi de§i³kenleri de§i³en bu süreyi belirtmektedir. Zamanlayc Bile³eni Modeli Zamanlayc bile³eni modeli (“ekil 8) µs çözü- nürlükte bir zamanlayc modellemektedir. Zamanlayc modeli almaç planlayc ve saysal almaç modelleri tarafndan sürelerin kurulmas için kullanlmaktadr. Biçimsel do§rulama için sistem kongürasyonunda her iki modelin kullanm için zamanlayc modelinin iki farkl örne§i kullanlmaktadr. UPPAAL aracnda bir do§al say en fazla 32768 de§erini alabildi§inden za- man planlayc bile³eninin istenilen çözünürlü§ü elde etmek amac ile farkl bir tasarma ihtiyac vardr. Bu amaçla Zamanlayc bile³eni typedef struct{int s; int ms; int us; }zaman_t; yapsn kullanr. Modelde zamann s ve ms de§erleri için soldaki döngü kullanlrken, µs de§erler için sa§daki döngü kullanlr. “ekil 8: Zamanlayc Bile³eni Modeli 3.3 Sistem Özellikleri Belirtimi Model denetim ile biçimsel do§rulamada modellenen sistem davran³nn sistem özelliklerini kar³layp kar³lamad§ denetlenir. Sistem davran³ sistem mode- linde belirtilen e³ zamanl bile³enlerin durumlarnn küresel bir durum uzayna çevrilmesi ile olu³turulur. Model denetimi ile küresel durum uzayndaki her bir durumun belirtilen sistem özelli§ini sa§layp sa§lamad§ kontrol edilir. Bu kap- samda Bölüm 3.1'da tanml sistem gereksinimlerinin denetimi için bu gerek- sinimlerin belirtimi gerekmektedir. Bu belirtimler almaç planlayc bile³eninin do§rulanmasnda iki ksma ayrlm³tr. Birinci ksm sistem davran³nn her- hangi bir kilitlenme olmadan i³ledi§inin denetlendi§i 1. ve 2. sistem gereksinim- lerinin belirtimini içermektedir. kinci ksm ise almaç planlayc ö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³nn herhangi bir kilitlenme olmadan çal³abildi§inin do§rulanmasn gösteririr. 1.b.'den 1.e.'ye kadar olan özellikler model denetimi esnasnda almaç planlayc modelindeki TROLUSTURMA, TAPLANLAMA, TAUYGULAMA ve TRBITTI durumla- rna geçi³lerin oldu§unu ve durumlarn ula³labilirli§inin do§ruland§n gösterir. planlayici bile³enin PlanlaycDurum de§i³keninin hiçbir sistem 2.a özelli§i ile AYRIKSI de§erini almad§n ve dolays 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 saysal almaçta mevcut bir tarama adm uygulanrken yeni bir tarama admnn saysal almaçta planland§n ve 4. gereksinimin sistemin za- Planlayici mansal kstlar ile uyumlu olmad§n gösterir. 2.b ve 2.c özellikleri bile³eninin UYGDUR ve PLANDUR durumlarna 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§rulanmasna tasarm gibi erken a³amalarda olanak sa§layan matematiksel temele sahip bir do§rulama yöntemdir. Bu bildiride almaç kontrol yazlmnn temel bile³eni olan almaç plan- layc bile³eninin model denetim kullanlarak biçimsel do§rulanmas sunulmu³- tur. Almaç planlayc bile³eni i³levsel ve zamansal gereksinimleri birlikte yerine getirmesi gereken gerçek-zamanl bir yazlm bile³enidir. Almaç planlayc do§- rulamasnn yaplmas için, almaç planlayc davran³ modeli çevresel bile³en ve görevlerin davran³lar ile birlikte modellenmi³, sistem gereksinimlerinin mete- matiksel özellikler ile belirtimi yaplm³ ve model denetim uygulanm³tr. Za- mansall§n modellenmesi için ise sistemin çözünürlük gereksinimleri göz önünde tutularak bir zamanlayc modeli olu³turulmu³tur. Model denetimi ko³ut zamanl davran³ modellerinin tüm durumlarnn sis- tem özellikleri ba§lamnda denenmesine dayanr. Bundan dolay model dene- timinde çok sayda ko³ut zamanl model olmas durum uzay patlamasna yol açabilir. Almaç planlayc bile³eni do§rulanmasndaki zamansall§n modellen- mesinde sistemin zamansal belirtimleri içinde mikrosaniye çözünürlü§ün çok dü- ³ük olmasndan dolay bu sorun ile kar³la³lmakta ve do§rulama süreci uzun sürebilmektedir. 653 Sistem modelinde modellenmi³ denetleyici, algoritma, saysal almaç haber- le³me ve almaç planlayc bile³enleri almaç kontrol yazlmnda birer görev olarak tasarlanmaktadr. 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ç planlayc 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ç planlayc bile³enin biçimsel do§rulanmas açsndan bu durumun yapl- m³ do§rulamaya olumsuz bir etkisi yoktur. Ancak algoritma süreleri ile ilgili gereksinimlerin de do§rulanmasnn yaplmas için görevlerin birbirleri ile olan etkile³imleri do§rulama srasnda dikkate alnmaldr. Bu açdan gelecekte i³le- tim sistemi (vxWorks) ve geli³tirme ortam (UML-Rhapsody) davran³larnn belirtimlerine sistem modelinde yer verilmesi gerekmektedir. Makalede sunulan sistem modeli ve özellikleri ile almaç planlayc 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 tasarma 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 Yazlm Mimarisi ve Arka Plan Yönetimi", TTD Konferans,2012. 3. M. Dursun, Ö. Kzlay, "Zaman Tetikli Almaç Planlayc Yazlm Bile³eni Tasa- rm", 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 Verication 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 Verication: Model-Checking Techniques and Tools", Springer Publishing Company, Incorporated, 2010 654