zet Biimsel do§rulama bir sistemin do§rulanmasnn tasarm a‡amasnda yaplmasna izin veren ve son yllarda kullanm hzla artan bir yntemdir. Bu bildiride alma planlayc bile‡eni tasarmnn gerek zaman gereksinimleri dahil edilerek biimsel do§rulanmas sunulmaktadr. Bu kapsamda saysal alma planlayc bile‡eninin biimsel modelinin ve gereksinimlerinin UPPAAL model denetim arac ile belirtimi ve do§rulanmas ele alnmaktadr. Anahtar Kelimeler Model Denetim, Gerek Zamanl Yazlm, Biimsel Do§rulama
GR
Elektronik taarruz [
Bu bildiride saysal alma planlayc bile‡eninin biimsel do§rulanmas sunulmaktadr. Blm 2’de biimsel do§rulama ve model denetim anlatlmaktadr. Blm 3’te alma planlayc tasarm, sistem bile‡eni modelleri ve sistem gereksinimlerinin biimsel belirtimi sunulmaktadr. Blm 4’te ise de§erlendirme ve sonu sunulmu‡tur. 2
Biimsel do§rulama, sistem davran‡nn sistem gereksinimlerine gre
matemetiksel modeller ve belirtimler kullanlarak do§rulanmasn sa§layan bir
yntemdir. Biimsel do§rulamann en byk avantaj tasarmn erken a‡amalarda
do§rulanmasna olanak sa§lamasdr. Model denetimi [
Zaman-kritik ve gerek-zamanl sistemlerin do§rulanmasnda sistemin i‡levsel
do§rulu§unun yan sra zamansal zelliklerinin do§rulanmas da gerekmektedir.
Dolaysyla sistem davran‡n belirten biimsel modelde zamansal davran‡larn
da belirtimi gerekmektedir. Zamanlanm‡ otomatlar [
UPPAAL [
ALMA˙ PLANLAYICI BLEEN DORULANMASI
Alma Planlayc Bile‡eni Tasarm Alma planlayc bile‡eni iin i‡levsel gereksinimler ‡u ‡ekildedir: Alma planlayc bile‡eni; 1. Atanan yaynlar iin tarama rejimini olu‡turacaktr. 2. Tarama rejimi admlarn almata uygulayacaktr. 3. Yayn listesinde de§i‡iklik oldu§u zaman mevcut tarama rejimini iptal edecek ve yeni bir tarama rejimi olu‡turacaktr. (a) Yayn listesi de§i‡ikli§i tarama adm uyguland§ srada gerekle‡irse, yeni tarama rejimi uygulanan tarama adm bitti§inde olu‡turulacak ve uygulanmaya ba‡layacaktr. 4. Tarama rejiminde tarama admlar arasnda en az anahtarlama sresi (400 s) kadar bo‡luk olacaktr. 5. Saysal almata bir tarama adm uygulanrken yeni bir tarama adm uygulanmayacaktr.
Tarama admlar, tarama rejimi dinamik olarak olu‡turuldu§undan ve tarama adm periyotlarnda gecikmeler olabilece§inden dolay periyodik grevler ile tasarlanamamaktadr. Buna ek olarak i‡lemci kartlarnda harici saat says snrldr. Bundan dolay alma planlayc bile‡eni, tarama rejimi olu‡turma ve uygulama i‡levlerini bir grevin ba§lamnda dizisel olarak zaman tetikli bir tasarmla yrtmektedir. Alma planlayc zaman gelen bir tarama admn uygulamak iin nce saysal almaca alma ayarlama mesajn gnderir. Almacn ayarland§na dair geribildirim mesajn ald§nda ise kal‡ sresini gndererek tarama admn ba‡latr. Tarama admnn zaman geldi§inde tarama admn uygulamadan nce admn kal‡ sresi 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 yrtmeye ba‡lar. ekil 1 ard‡k tarama admlarnn uygulanmasn gstermektedir.
Tarama admlar arasndaki anahtarlama sresi boyunca sayssal almacn ayarlanmas ve saysal almatan alnan DTK’larn yerel belle§e kopyalanmas i‡lemleri gerekle‡tirilir. Saysal alma, gnderilen parametreler ile gerekli ayarlamalar gerekle‡tirir. Alma ayarlama i‡lemi belirli bir sre almaktadr. Buna ek olararak DTKlarn yerel belle§e kopyalanmas da DTK saysna ba§l olarak de§i‡en bir sreye sahiptir. Yaplan lmler do§rultusunda bu i‡lemler iin 200 s’lik sreler ayrlm‡tr. Bu i‡lemlerden herhangi birisinin beklenen sreden uzun srmesi ard‡k iki tarama adm uygulanrken ardl adm iin yukarda belirtilen 5. i‡levsel gere§in yerine getirilememesine yol aar. 3.2
Sistem Modeli Belirtimi Alma planlayc bile‡eninin do§rulanmas iin sistem modeli alma planlayc bile‡eninin hem i‡levsel hem de zamansal davran‡n belirtmelidir. Bu kapsamda sistem modelinin sistemin i‡levsel ve zamansal davran‡larn belirtebilmesi iin saysal alma, alma kontrol ve sistem kontrol bile‡enlerinin modellerinden olu‡mas gerekmektedir. Denklem 1 sistemin bile‡enlerini tanmlamaktadr.
S = CSayisalAlmacjjCAlmacKontroljjCSistemKontrol (1) Alma kontrol bile‡eni alma planlayc, denetleyici, algoritma, sistem kontrol haberlesme (SistemKontHab) ve saysal alma haberle‡me (SayAlmacHab) bile‡enlerinin paralel bile‡imidir. Denklem 2 alma planlaycnn bile‡enlerini gsekil 1: Tarama Admlar Mesaj Ak‡ emas termektedir.
CAlmacKontrol = CDenetleyicijjCAlmacP lanlayici jjCAlgoritmajjCZamanlayicijjCSayAlmacHab (2) Saysal Alma Modeli Saysal alma modeli (ekil 2) taAlmacAyarla ile tetiklendi§inde saati alma ayarlama sresine kurar. Zaman doldu§unda taAlmacAyarlaACK ’i tetikler. taBasla ile tetiklendi§inde ise saati alma kontrol yazlmndan gnderilen kal‡ sresine kurar. Kal‡ sresi zaman doldu§unda alma kontrol yazlmn taDTK ile tetikler.
Sistem Kontrol Modeli Sistem kontrol modeli (ekil 3) sistem kontrol yazlmnn soyutlanm‡ halidir. Sistem kontrol modeli HIKomut ile alma kontrol bile‡enini tetikleyerek en fazla iki yayn iin hedef izleme ba‡latr. Bu iki yayn planlamalar arasnda anahtarlama sresi olacak kadar tanmlanm‡tr. HIKomutACK ile tetiklendikten sonra alma kontrol bile‡eninin retti§i raporlar almaya ba‡lar. Daha sonra herhangi bir zamanda tm yaynlar ya da bir yayn ekil 2: Saysal Alma Modeli iin HIKomut ile alma kontrol bile‡enini tetikleyerek alma kontrol yazlmnda mevcut yaynlar iin tarama rejimi planlanr ve uygulanrken yayn listesi de§i‡ikli§i gerekle‡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 modelinden gnderilen HIKomut ile tetiklenerek alma planlayc modelinin durumuna gre mevcut tarama rejiminin durdurulmasn sa§lar. Alma planlaycnn tarama rejimini durdurmas ile gnderdi§i PlanlamaDurdu ile tetiklendi§inde, e§er yayn listesinde halen izlenmesi gereken bir yayn varsa PlanlamaBaslat ile 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 uygulanmasn ba‡latr. TAPLANLAMA durumuna geerken mevcut yaynlar iin tarama 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‡ sresine zaman kurarak tarama admn uygulamaya ba‡lar. TAUYGULAMA durumuna getikten sonra sras ile almac ayarlar ve almata tarama admnn kal‡ sresi kadar uygulanacak tarama admn ba‡latr. Alma planlayc modeli tarama admnn planlanan biti‡ zaman geldi§inde sistem durumuna gre 3 farkl duruma geebilir: TRBITTI durumuna tarama rejiminde uygulanacak ba‡ka bir adm kalmad§nda, TAPLANLAMA durumuna tarama rejiminde uygulanacak ba‡ka admlar oldu§unda ve UYGDUR durumuna ise tarama adm uygulanrken yayn listesi de§i‡ikli§i gerekle‡ti§inde gei‡ yaplr. Alma planlayc modelinde PLANDUR durumuna tarama rejimindeki bir adm uygulanmad§ esnada yayn listesi de§i‡ikli§i gerekle‡ti§i zaman geilir 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 gei‡i yoktur. Alma planlayc modelinde AYRIKSI durum 5. gereksinimi gereklemek amac ile tanmlanm‡tr. E§er almata uygulanan bir tarama adm mevcutken yeni bir tarama admnn ba‡latlmas sz konusu ise model AYRIKSI durumuna geerek uygulanmaya al‡lan adm atlayarak tarama rejimindeki ardl adma geer.
Alma Kontrol Saysal Alma Haberle‡me Bile‡eni Modeli Saysal alma haberle‡me modeli (ekil 6) saysal almatan DTK’lar alnd§nda DTK’larn yerel belle§e kopyalanmas iin gereken DTK says ile de§i‡en zamansal davran‡ modeller. Model taDTK ile tetiklendikten sonra iMinDTKKopyalamaSuresi ve iMaxDTKKopyalamaSuresi arasnda bir sre 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 almatan alnan DTK’lar ile al‡trlan algoritmalar modeller. Model taYerelDTK ile tetiklendikten sonra iMinAlgoritmaSuresi ve iMaxDTKAlgoritmaSuresi arasnda bir sre bekledikten sonra rapor ile Sistem kontrol modelini tetikler. Algoritmalarn yrtme sresi DTK says ve DTK’larn ieri§i ile de§i‡ebilmektedir. iMinAlgoritmaSuresi ve iMaxDTKAlgoritmaSuresi de§i‡kenleri de§i‡en bu sreyi belirtmektedir.
Zamanlayc Bile‡eni Modeli Zamanlayc bile‡eni modeli (ekil 8) s znrlkte bir zamanlayc modellemektedir. Zamanlayc modeli alma planlayc ve saysal alma modelleri tarafndan srelerin kurulmas iin kullanlmaktadr. Biimsel do§rulama iin sistem kongrasyonunda her iki modelin kullanm iin zamanlayc modelinin iki farkl rne§i kullanlmaktadr.
UPPAAL aracnda bir do§al say en fazla 32768 de§erini alabildi§inden zaman planlayc bile‡eninin istenilen znrl§ elde etmek amac ile farkl bir tasarma ihtiyac vardr. Bu amala Zamanlayc bile‡eni typedef structfint s; int ms; int us; gzaman_t; yapsn kullanr. Modelde zamann s ve ms de§erleri iin soldaki dng kullanlrken, s de§erler iin sa§daki dng kullanlr.
ekil 8: Zamanlayc Bile‡eni Modeli 3.3
Sistem zellikleri Belirtimi Model denetim ile biimsel do§rulamada modellenen sistem davran‡nn sistem zelliklerini kar‡layp kar‡lamad§ denetlenir. Sistem davran‡ sistem modelinde belirtilen e‡ zamanl bile‡enlerin durumlarnn kresel bir durum uzayna evrilmesi ile olu‡turulur. Model denetimi ile kresel durum uzayndaki her bir durumun belirtilen sistem zelli§ini sa§layp sa§lamad§ kontrol edilir. Bu kapsamda Blm 3.1’da tanml sistem gereksinimlerinin denetimi iin bu gereksinimlerin belirtimi gerekmektedir. Bu belirtimler alma planlayc bile‡eninin do§rulanmasnda iki ksma ayrlm‡tr. Birinci ksm sistem davran‡nn herhangi bir kilitlenme olmadan i‡ledi§inin denetlendi§i 1. ve 2. sistem gereksinimlerinin belirtimini iermektedir. kinci ksm ise alma planlayc zelinde 3., 4. ve 5. sistem gereksinimlerinin belirtimini iermektedir. Sistem zellikleri belirtimi a‡a§da gsterilmi‡tir. 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 gsteririr. 1.b.’den 1.e.’ye kadar olan zellikler model denetimi esnasnda alma planlayc modelindeki TROLUSTURMA, TAPLANLAMA, TAUYGULAMA ve TRBITTI durumlarna gei‡lerin oldu§unu ve durumlarn ula‡labilirli§inin do§ruland§n gsterir. 2.a zelli§i ile planlayici bile‡enin PlanlaycDurum de§i‡keninin hibir sistem durumdaAYRIKSI de§erini almad§n ve dolays ile planlayici bile‡enin TAAYRIKSI durumuna gemedi§ini ifade eder. Bu zelli§in sa§lanmas anahtarlama sresinin yeterli uzunlukta oldu§unun do§ruland§n gsterir. Bu zelli§in sa§lanamamas saysal almata mevcut bir tarama adm uygulanrken yeni bir tarama admnn saysal almata planland§n ve 4. gereksinimin sistemin zamansal kstlar ile uyumlu olmad§n gsterir. 2.b ve 2.c zellikleri Planlayici bile‡eninin UYGDUR ve PLANDUR durumlarna eri‡tikten sonra Sistem Kontrol bile‡eninin DUR durumuna geece§ini ifade eder. Bu zelliklerin sa§lanmas ise 3. sistem gereksiniminin do§ruland§n gsterir. 4
Biimsel do§rulama bir sistemin gereksinimlerine gre do§rulanmasna tasarm gibi erken a‡amalarda olanak sa§layan matematiksel temele sahip bir do§rulama yntemdir. Bu bildiride alma kontrol yazlmnn temel bile‡eni olan alma planlayc bile‡eninin model denetim kullanlarak biimsel do§rulanmas sunulmu‡tur. Alma planlayc bile‡eni i‡levsel ve zamansal gereksinimleri birlikte yerine getirmesi gereken gerek-zamanl bir yazlm bile‡enidir. Alma planlayc do§rulamasnn yaplmas iin, alma planlayc davran‡ modeli evresel bile‡en ve grevlerin davran‡lar ile birlikte modellenmi‡, sistem gereksinimlerinin metematiksel zellikler ile belirtimi yaplm‡ ve model denetim uygulanm‡tr. Zamansall§n modellenmesi iin ise sistemin znrlk gereksinimleri gz nnde tutularak bir zamanlayc modeli olu‡turulmu‡tur.
Model denetimi ko‡ut zamanl davran‡ modellerinin tm durumlarnn sistem zellikleri ba§lamnda denenmesine dayanr. Bundan dolay model denetiminde ok sayda ko‡ut zamanl model olmas durum uzay patlamasna yol aabilir. Alma planlayc bile‡eni do§rulanmasndaki zamansall§n modellenmesinde sistemin zamansal belirtimleri iinde mikrosaniye znrl§n ok d‡k olmasndan dolay bu sorun ile kar‡la‡lmakta ve do§rulama sreci uzun srebilmektedir.
Sistem modelinde modellenmi‡ denetleyici, algoritma, saysal alma haberle‡me ve alma planlayc bile‡enleri alma kontrol yazlmnda birer grev olarak tasarlanmaktadr. Bu grevler ayn i‡lemci kayna§n kullanmakta ve bir grevin i‡lemciyi kullanmas di§er grevlerin yrtlmesinde gecikmeye yol aabilmektedir. Alma planlayc bile‡eni en yksek ncelikli grev olarak tasarland§ndan di§er grevlerin bu grevde herhangi bir gecikmeye yol amas mmkn de§ildir. Alma planlayc bile‡enin biimsel do§rulanmas asndan bu durumun yaplm‡ do§rulamaya olumsuz bir etkisi yoktur. Ancak algoritma sreleri ile ilgili gereksinimlerin de do§rulanmasnn yaplmas iin grevlerin birbirleri ile olan etkile‡imleri do§rulama srasnda dikkate alnmaldr. Bu adan gelecekte i‡letim 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 biimsel do§rulamas gereklenmi‡tir. Bu biimsel do§rulama srecinde grlen ancak testlerde grlemeyen 3. gereksinim ile ilgili baz durumlar tasarma eklenmi‡ ve ciddi bir fayda elde edilmi‡tir.