Byyen Ksmi Yol Kstlaryla Konkolik Test

Abstract

zet. Otomatik birim testler sayesinde programlarn kapsama orann arttrmak mmkndr. Konkolik test metodu (concolic testing) otomatik birim test yaratm iin kullanlan bir yazlm testi tekni§idir. Ancak, yol patlamas (path explosion) ve kst zmlerinin (constraint solving) yaratt§ darbo§az nedeniyle, leklenebilir bir otomatik konkolik testi geli‡tirmek zor olmu‡tur. Bu tekni§i leklenebilir hale getirebilmek iin bu makalede kst zcye daha ok ama daha kk sorgular gnderilerek zme zerindeki yk haetecek bir yol nerilmi‡tir. Yapt§mz deneyler altta yatan kst zcye yaplan sorgu uzunluklarn d‡rerek bu hedefe yakla‡ld§n gsteriyor. Anahtar Kelimeler: Konkolik Test (Concolic Testing), Hedef Ynelimli Test (Goal Directed Testing), Dallanma Zorlamas (Branch Enforcement), Kst ˙zm (Constraint Solving)

-

Konkolik testte ama test edilen programn yollarn dola‡acak girdileri otomatik olarak olu‡turmaktr. Buna rnek olarak bir gen snandrma programn d‡nelim. Bu program test edilirken btn olas sonularn (e‡itkenar, ikizkenar, e‡kenar, gen de§il) bir ‡ekilde ortaya karlmasn sa§layacak test girdileri retilmesini bekleriz. Tm yollar kapsayacak ‡ekilde bir test retmek zor ve uzun vakit alan bir i‡tir. Bu i‡in hzlanabilmesi, daha byk programlarda da otomatik test retimini mmkn klacaktr. Konkolik testin daha hzl al‡mas iin nerdi§imiz yntem kst zcye yaplan sorgu uzunluklarn d‡rerek bu amaca hizmet etmeyi ngren bir n al‡madr. Konkolik test metodu program al‡masn (program execution) istenilen yollara ynlendiren girdileri yaratmaya al‡r. Bu girdileri yaratabilmek iin, istenilen yollarn yol kstlar (path constraint) bulunur. Byle kstlar sa§layan girdileri bulmak kst sa§lama problemi (constraint satisfaction problem) olarak bilinen ok zor bir problemdir. Bu problemleri zmek genelde girdinin byy‡yle ssel oranda vakit alr. Bu yzden kst sa§lama iin yapmay planlad§mz ‡ey mmknse kst zcye yaplan sorgu saysn artrmak pahasna sorgular ksaltmaktr. Bir byk kstn zm iin daha kk kstlarn zmn kullanmak zerinde al‡lm‡ bir kirdir [ 1 ]. Kst zcleri bu ‡ekilde kullanmak yazlm do§rulamas (verication) alannda nerilmi‡tir [ 2 ]. Yntemimizi CREST adl konkolik test programnda gerekle‡tirdik. Yapt§mz ilk deneysel al‡malarda daha kk denemeler ile ayn kapsama oranna ula‡labildi§ini grdk. Makalenin geri kalan ‡u ‡ekilde dzenlenmi‡tir. Blm 2 konkolik test zerine yaplm‡ di§er al‡malar aklamaktadr. Blm 3 konkolik test ve geli‡tirilmi‡ yeni yntem hakknda detayl bilgi vermektedir. Blm 4 ise nerilen metodun yararl oldu§u bir rne§i iermektedir. Blm 5 ise kk programlar zerindeki deneysel sonular gsterirken bu sonular tart‡maktadr. Blm 6 ise ‡imdiye kadar gelinmi‡ olan noktay belirtirken Blm 7 ise daha ileride yaplabilecekleri anlatmaktadr. 2

lgili ˙al‡malar

Konkolik test verilen bir programn istenilen ksmlarn al‡trmak iin gerekli girdileri reten ve programlar somut olarak bu girdilerle al‡tran yazlm testi temelli bir yakla‡mdr. Konkolik test program istenilen tek bir hedefe ynlendirilebilir [ 3 ] veya olas btn hedeere varmaya al‡abilir [ 4 ] [ 5 ] [ 6 ]. Java [ 7 ] [ 8 ], C [ 5 ] ve C# [ 6 ] gibi bilinen dillerin o§unda kullanlm‡tr. Konkolik test byk programlarda al‡trlamad§ndan bu yntemin farkl ba§lamlarda geli‡tirilmesi iin al‡malar yaplm‡tr [ 9 ]. Konkolik testte kullanlan yakla‡mlar zerine detayl bir ara‡trma bulunmaktadr [ 5 ]. Geleneksel konkolik testin znde tm program yollar zerinde derinlik ncelikli arama (depth rst search) vardr [ 4 ]. Bu aramalarda uygulamann somut al‡m sonucu hesaplanm‡ sembolik yollar kullanlr. Bu yakla‡mda yol zerinde denenmemi‡ en son dallanma tersine evrilmeye al‡lr. En ok uygulanan alternatif yakla‡mlardan biri ise geni‡lik ncelikli aramadr (breadth rst search) [ 1 ] [ 10 ]. Bu yakla‡mda algoritma rastgele bir girdiden ba‡lar ve yol zerinde denenmemi‡ ilk dallanmada sapmaya neden olacak girdileri bulmaya al‡r. lk seviyedeki dallanmalar bitti§inde bir sonraki dallanmalara geilir ve yeni girdiler olu‡turulurken nceki yaratlm‡ girdilerden faydalanlr. Bu yakla‡m ba‡ta ok kk yol kstlar yaratr ve kstl bir test yapma yakla‡mna olanak sa§lar. Ba‡ka bir arama alternati de kontrolak‡ ynlendirmeli (control-ow directed) testtir [ 5 ]. Algoritma program istatistiki olarak kontrol-ak‡ izelgesindeki en yakn ifadelere ynlendirmeye al‡r. Program al‡ma yollar zerinde arama yaptka algoritmann yava‡lad§ grlm‡, bu yzden rastgele yeniden ba‡lamalar kullanlm‡tr. Rastgele-dallanma test yakla‡m uygulamann somut al‡m sonucu hesaplanm‡ sembolik yol zerindeki herhangi bir dallanmay rastgele olarak seer [ 5 ]. Rastgele-dallanma aramasnn yan sra, rastgele-yol aramas da denenmi‡tir. Bu yakla‡m rastgele yollar semeyi ve al‡may bu yollara ynlendirmeyi dener. Bu yakla‡mn yazlm testinde en sk kullanlan rastgele-girdi aramasndan daha iyi al‡t§ iddia edilmi‡tir. Bu yakla‡m somut bir al‡ma seer ve bu al‡ma yolu zerindeki her dallanmay 12 olaslkla tersine evirir. Sonra da bu yeni yol kst iin girdi yaratmaya al‡r. Rastgele-dallanma yakla‡mnn kapsama bakmndan daha iyi al‡t§ gsterilmi‡tir [ 5 ]. Bir di§er ilgin yakla‡m ise hedef-ynelimli dallanma zorlamasdr (goal-directed branch enforcement). Bu yakla‡mda belirli bir hedef iin sembolik yol kstlar toplanr ve btn kst giderek artan ‡ekilde kritik dallanma ko‡ullarn zerek sa§lanr [ 11 ]. Bizim al‡mamzda ise, sz konusu yakla‡mn tm yollar deneyen metodlara genellenmesi sunulmaktadr. Konkolik testte kullanlan kst sa§lama problemi verilen kstlar ierisinde kalan bir rnek bulmak olarak tanmlanabilir. Konu hakknda daha fazla bilgi [ 12 ] kayna§ndan elde edilebilir. Yices, Z3 gibi standart kst zclerin yan sra nonlineer kstlar zmek [ 13 ] ve gerel saylarda yksek kesinlik [ 14 ] iin ayarlanm‡ kst zcler vardr. Kst zm 3-sa§lanabilirlik (3-satisability) probleminin bir genellemesi olup problemin byk rneklerini zen bir algoritma bulunmas beklenmemelidir. Bu makalede kulland§mz yntem derinlik ncelikli arama ile hedef-ynelimli konkolik test algoritmalarnn birle‡tirilmesiyle geli‡tirilmi‡tir. 3 3.1

Yntem

Konkolik Test

Konkolik (Concolic) test ingilizce concrete (somut) ve symb olic (sembolik) testlerin birle‡imi iin bir ksaltmadr. Bu yakla‡mda, test altndaki program sa§lanmas gereken dallanma ko‡ullarnn (branch condition) sembolik olarak toplanlmasn sa§layacak ‡ekle getirilir. Sonra toplanm‡ ko‡ullar kullanlarak yeni bir ko‡ul kmesi elde edilir. Bu yeni ko‡ullar incelenilerek yeni girdiler yaratlr ve programa girdi olarak sunulur.

Tanm 1 DALLANMA KOULU (Branch Condition, c) En az bir program parametresine (girdi) ba§l sadece do§ru veya yanl‡ olabilen ve her farkl sonucun program farkl bir al‡ma yoluna ynlendirdi§i ko‡ullardr.

Dallanma ko‡ullar a‡a§dakilerden herhangi biri olabilir: Boole cebri (boolean algebra) kullanlarak yazlm‡ bir ifade, Bir kar‡la‡trma veya Sadece do§ru veya yanl‡ dndren bir fonksiyon.

Genelde bir programdaki dallanma ko‡ullar birbirine ba§ldr, o yzden bir ko‡ulun sonucunu sabit tutmak di§erlerini etkiler. Rastgele bir al‡ma yolu zerindeki rastgele bir ko‡ulun, bu yol zerindeki di§er dallanmalarn ortalama i ile ba§l oldu§u gsterilmi‡tir ( N bu yol zerindeki toplam dallanma ko‡ulu says olarak alnm‡tr) [ 4 ].

N 8 Tanm 2 DALLANMA KOULU BALILII (Branch Condition Dependency) ki dallanma ko‡ulu sadece ve sadece a‡a§daki durumlarda birbirine ba§l kabul edilir: ki dallanma ko‡ulunun d gibi en az bir ortak de§i‡keni varsa veya ki ko‡ul da nc bir ko‡ulla ba§lysa.

Olas bir al‡ma yolunun gereklenebilmesi ancak o yol zerindeki btn dallanma ko‡ullarnn sa§lanmasyla olabilir. Tanm 3 TAM YOL KISITI (Full Path Constraint, ) Tam yol kst, bir al‡ma yolu zerindeki btn dallanma ko‡ullarnn mantksal Ve operatryle birle‡tirilmesi olarak tanmlanr: u andan itibaren kst zc ad verilecek olan ve varsa tam yol kstn sa§layan de§erler yaratabilen bir zcnn oldu§u varsaylacaktr. Bylece, gereklenebilir (feasible) btn al‡ma yollarna gtrecek olan gerekli girdiler yaratlp program bu girdilerle al‡trlabilir. rne§in, program bir hata ifadesine ynlendiren bir yol gereklenmeye al‡lyor ve buna kar‡lk gelen tam yol kst biliniyorsa ya bu ifadeye varacak girdiler yaratlabilir ya da bu al‡ma yolunun gereklenemez (olanaksz) oldu§u sonucuna varlr.

Konkolik testte, program nce rastgele girdilerle al‡trlr. Sonra, al‡ma srasnda sembolik al‡ma yolunun tam yol kst toplanr. Asl kst zerinden yeni bir tam yol kst elde etmek iin bir strateji izlenir. Genel bir strateji bu tam yol kst zerindeki son dallanma ko‡ulunu tersine evirmektir [ 4 ]. Sonra yeni yol kst kst zc ye verilir ve program iin yeni test girdileri elde edilir. 0 = :cN ^

N 1 ^ ci i=1 (1)

Bu stratejiye derinlik-ncelikli arama ad verilir. Uygulamalar genel olarak kst saysyla veya azami iterasyon saysyla [ 5 ] snrlandrlm‡tr. Byle bir algoritma Algoritma 1 zerinde aklanm‡tr. 3.2

Ksmi Yol Kstlar

Teoride, bir kst zcnn al‡ma sresi zcye verilen ifade (ko‡ul) saysyla ssel olarak byr [ 15 ]. Bu yzden, kst zcye byk kstlar vermek kt bir kirdir. Konkolik testte, leklendirilebilirli§in nndeki darbo§az yol patlamas, yksek dallanma says ve kst zcye verilen bu byk sorgulardr [ 16 ]. Bizim yakla‡mmzda, sorgu uzunluklar sorgu saysn artrmak pahasna d‡rlmeye al‡lm‡tr.

Tanm 4 KISM YOL KISITI (Partial Path Constraint, ) Tam yol kstnn her yukar yakla‡m (over-approximation) bir ksmi yol kst olarak adlandrlr. Tam yol kstn yol zerindeki dallanma ko‡ullarnn bir kmesi olarak d‡nrsek, ksmi yol kstn da tam yol kstnn herhangi bir alt kmesi olarak grebiliriz.

Tanma gre, mutlak do§ruluk (true) btn tam yol kstlarnn bir yukar yakla‡mdr. Ayrca, al‡ma yolu zerindeki her dallanma ko‡ulunun da bir ksmi yol kst oldu§u grlebilir.

! Algoritma 1 Derinlik ncelikli Aramal ve Azami terasyonlu Konkolik Test. Teorem 1 YOL KISITLARININ YUKARI YAKLAIMI (Over-approximation of Path Constraints) Bir tam yol kstn sa§layan btn rnekler ayrca bu yolun btn ksmi yol kstlarn da sa§lar.

E§er sadece ksmi yol kstn zersek, bu zmn her zaman tam yol kstn sa§lama ‡ans vardr. Bu al‡mada, tam yol kstlarnn kullanmndan kanabilmek amacyla ksmi yol kstlarnn yaratlmas zerine al‡lm‡tr. Burada asl hedef btnlk (completeness) ve geerlilikten (soundness) dn vermeden byk kstlarn yaratt§ yk azaltmaktr. 3.3

Ksmi Yol Kst Yaratma Stratejileri

Algoritma 2’da program zerinde tek bir al‡ma yolunu gerekleyecek girdi retilmektedir. Bunun iin sembolik olarak bu heden tam yol kst bilinmelidir. E§er 3. satrda ksmi yol kstn sa§layan girdiler bulunamyorsa, tam yol kst da sa§lanamyor demektir. E§er 8. satrda §renilen tam yol kst hedef ile aynysa istenilen girdi elde edilmi‡ demektir. E§er hibiri de§ilse, o zaman yolun sapmasna neden olan bir ko‡ul vardr. Bu sapma 15. satrda §renilmektedir.

Algoritma 3’te ise Algoritma 2 kullanlarak tm yollar gerekleyecek olan bir girdi listesi retilmektedir. Derinlik ncelikli arama kullanlm‡tr. 15. satrda grld§ gibi daha nce gereklenmi‡ al‡ma yollarndan yeni tam yol kstlar elde edilerek Algoritma 2’ye verilmektedir. Algoritma 2 Byyen Ksmi Yol Kstlar Kullanan Hedef-Ynelimli Konkolik Test Algoritma 3 Byyen Ksmi Yol Kstlarn Kullanan Tam Konkolik Test

Require: P : program under test

Ensure: inputs : Test Suite 1: inputs ; 2: = true. 3: girdi generateInput( ) 4: for j = 1 to max_iterations do 5: Execute P with input 6: Add input to inputs 7: collectedPathConstraint 8: for i = length( ) to 0 do 9: if !isVisited(branchOf( [i]) then 10: c [i] 11: break 12: end if 13: end for 14: if isDened( c) then 15: [i] :c 16: input Algortihm 2(P; ) 17: Add input to inputs 18: else 19: break 20: end if 21: end for Teorem 2 YOL SAPMASI (Path Divergence) Ksmi kst yi sa§layan ama tam yol kst ’yi sa§lamayan girdiler var ise bu girdiler iin ( ! c)^( 0 ! :c) ifadesini sa§layan ve yol sapmasna neden olan c vardr. Bu ifadede 0, yi sa§layan girdilerin kar‡lk geldi§i al‡ma yolunun tam yol kstn belirtmektedir.

Algoritma 3’n perfromansn arttrmak iin 15. satrda daha uzun ama kst zcye yklenmeyen bir ile ba‡lanabilir. Bu sefer yine son dallanma ko‡ulunun tersi :cN i ierir, ama bundan ba‡ka birbirinden ba§msz (Tanm 2) di§er btn dallanma ko‡ullarn da ierir. Byle bir yi zmek, kst zc iin = cN yi zmek kadar kolay olacaktr, nk kst zc byle bir durumda her dallanma ko‡ulunu ayr ayr zer [ 4 ] [ 17 ]. Bu durumda ksmi yol kstlar daha ok de§i‡ken ierdi§i iin al‡ma yolunu sa§lama ‡ans daha yksek olacaktr.

Sonraki φ ye geç (π → φ) evet evet Sonraki φ var mı? hayır φ ← φ ∧ cd evet π0 smaup?ıyor hayır πSoyneragkeçi

Sonraki π hayır var mı?

DUR ekil 1. Byyen Ksmi Yol Kstl Konkolik Test Ak‡ ˙izelgesi

Grsel kolaylk vermek iin ekil 1 te geli‡tiridi§imiz algoritmann ak‡ izelgesi vardr. Bir listesi oldu§unu ve de her iin btn yollar deneyen bir listesi oldu§unu varsaymaktadr. Genel olarak sonsuz yol olabilir ve azami iterasyon snr durma ko‡ulu olarak kullanlr. Ak‡ izelgesi ayrca cd de§i‡kenini kullanmaktadr. Bu de§i‡ken sapma sebebini belirtmek iin kullanlm‡tr. Hedef yol kst nin bir dallanma ko‡uludur.

Başlangıç, φ ← > φ için girdi yarat φ gerçeklenebilir mi?

evet Programı Girdilerle Çalıştır hayır

rnek

Bu blmde rnek olarak verilen saynn kkten by§e sral olup olmad§n kontrol eden bir program iin test kmesi yaratlacaktr. Test altndaki programn kontrol-ak‡ izelgesi ekil 2 zerinde gsterilmi‡tir.

a ≤ b a ≤ c

A B C

a > b a > c

HAY IR b > c b ≤ c

EV ET ekil 2. sralM(a,b,c) Metodunun Ak‡ ˙izelgesi

Klasik bir konkolik test ekil 3 zerinde grld§ gibi rastgele bir girdi ile ba‡lar. Test altndaki program bu girdiyle al‡trlr ve tam yol kst 1 hesaplanr. Bundan sonra yeni bir tam yol kst 2, 1 in son dallanma ko‡ulu tersine evrilerek olu‡turulur. Bu yeni al‡ma yolunu gerekleyebilmek iin tam yol kst kst zcye verilir. Bu tam yol kst 3 tane dallanma ko‡ulu ierdi§i iin bu operasyon 3 uzunlukta kst zm, ksaca K˙(3) olarak tanmlanm‡tr.

Test altndaki program test boyunca 4 kere al‡trlm‡tr ve kst zcye 3 kere sorgu gnderilmi‡tir. nemli nokta ise bu sorgularn ortalama uzunlu§unun (3 + 2 + 1)=3 = 2 olmasdr.

Geli‡tiridi§imiz konkolik test tekni§inde ekil 4 zerinde grlen testte bir girdiyle ba‡lanm‡ ve kar‡lk gelen tam yol kst §renilmi‡tir. Sonra 2 normal konkolik testteki gibi olu‡turulup hedef olarak belirlenmi‡tir. Tm ifadenin zlmesi yerine tam bu noktada tam yol kstnn yukar yakla‡mlar kullanlm‡tr. 21 alttaki kst zcnn program do§ru al‡ma yoluna ynlendiremeyen bir girdi yaratmasna neden olmu‡tur. Bu yzden algoritma sapmann nedenini (cd) bulur ve §renir ( ^ cd). Bu §renme bir ba‡ka yukar yakla‡m olan 2 ! 22 ! 21 ile sonulanr. Bu yukar yakla‡m rnekte program al‡masn hedefe ynlendirme asndan yeterli gelmi‡tir.

ki algoritmay kar‡la‡tracak olursak, bunda da yine test altndaki program 4 kere al‡trlm‡tr, ancak kst zcye ortalamada (1 + 2 + 1)=3 = 1:33 uzunlu§unda sorgular yaplm‡tr. [K˙(3)] [K˙(2)] [K˙(1)] [Tm Yollar Denendi ] ekil 3.

Klasik Konkolik Test Kullanlarak ˙zm

ekil 4.

Geli‡tiridi§imiz Ksmi Yol Kstlar ile ˙zm [ba‡langta ]

[K˙(1)] [P21 6= Pistenen ] [ ^ cd]

[K˙(2)] [P22 = Pistenen ]

[K˙(1)] [Tm Yollar Denendi ] i1 = [0; 0; 0] P1 = A ! B ! C ! EV ET 1 = (a b) ^ (a c) ^ (b 2 = (a b) ^ (a c) ^ :(b 21 = :(b c) i21 = [0; 0; 1] P21 = A ! B ! HAY IR 22 = (a c) ^ :(b c) i22 = [ 1; 0; 1] P22 = A ! B ! C ! HAY IR 3 = :(a b) 31 = :(a b) i31 = [0; 1; 1] P31 = A ! HAY IR

DUR c) c)

Deneyler

Tekni§imizi CREST adl C iin geli‡tirilmi‡, derinlik-ncelikli arama ve rastgeledallanma gibi bilinen stratejileri kullanan bir konkolik test uygulamas zerine ekledik [ 5 ]. CREST’i ksmi yol kstlarn ve girdi/kst nbelleklenmesi kullanacak ‡ekilde de§i‡tirdik. Ayrca verilen test kmelerinin verilen programlardaki dallanma kapsamn (branch coverage) len bir kod da yazdk.

A‡a§da be‡ farkl konkolik test uygulamas tanmlanm‡tr. Bunlardan KYK ve bKYK bizim geli‡tirid§imiz ksmi yol kstlar yakla‡mn kullanmaktayken di§er kar‡la‡trma amal olarak literatrde bulunana ve CREST’te gerekle‡tirlmi‡ yntemlerdir. 1. DA: Derinlik-ncelikli arama kullanan normal konkolik test algoritmasdr. 2. KA˙: Kontrol-ak‡ izelgesi ynlendirmeli konkolik test algoritmasdr. 3. Rastgele: Rastgele-dallanma yakla‡m kullanlan konkolik test algoritmasdr. 4. KYK: Ksmi yol kstlar yakla‡m kullanlan konkolik test algoritmasdr. 5. bKYK: Bellekli ksmi yol kstlar algoritmasdr. Bu algoritma da normal KYK’dan farkl olarak kst zcye daha nce yollanm‡ sorgular ve test altndaki programa gnderilmi‡ girdileri hatrlayan bir hafza vardr ve ayn sorgularla al‡malarn tekrarlanmasna engel olmak amacyla tasarlanm‡ olup yer kayglar yznden bu makalenin d‡nda braklm‡tr.

Be‡ yntem de iki farkl C programnda ( Drtgen ve gen ) ile al‡trlm‡tr. Bu programlar alar ve kenar uzunluklar verilen gen ve drtgenleri snandrmak amacyla yazlm‡tr. Test altndaki programn al‡trlma iin iterasyon limiti 100 olarak belirlenmi‡tir.

Tablo 1’de deney sonularmz verilmi‡tir. Tablodan KYK ve bKYK’nn DA ve KA˙’a gre daha ok sorgu yapt§ grlebilir. Ancak, ortalama sorgu uzunlu§u bunlara gre ok d‡ktr. Benzer ‡ekilde Rastgele’nin ortalama sorgu uzunlu§unn en ksa oldu§u ancak sorgu saysn ok fazla oldu§u ve dallanma kapsamnn d‡t§ grlmektedir. Bu sayede kst zcnn zm sresi kst uzunlu§uyla ssel olarak artt§ndan karma‡klk azaltlm‡tr. Tablo’dan bKYK ynteminin kst zc zerindeki yk en az tavizle en ok haeten yntem oldu§unu grlmektedir. nceki sorgular hatrlamann toplam sorgu says zerinde bir etkisi olmam‡tr, ancak gereksiz test girdilerinin karlmas ile test kmeleri KYK’ya gre kltm‡tr. Bu saptama gen programnn ihtiya duydu§u girdi saysnn 27’den 19’a d‡rlm‡ olmasyla aklanabilir. 6

Sonular

Bu n al‡mada byyen ksmi yol kstlarnn konkolik test iin kullanlabilecek bir yakla‡m oldu§u gsterilmi‡tir. Deneylerimizde ortalama sorgu uzunlu§unun yarya kadar d‡rlmesi ilerisi iin umut vaat edici bir geli‡medir. Bu geli‡melerin zellikle karma‡k yol kstlarna sahip programlarda konkolik testin gen 10 19 26 26 DA KA˙ KYK bKYK Rastgele 100

Sorgu Ort. Sorgu Girdi Dallanma

Sorgu Ort. Sorgu Girdi Dallanma

Yntem

Says

Uzunlu§u Says Kapsamas

Says

Uzunlu§u Says Kapsamas

Drtgen 100 10 18 17 17 daha hzl al‡masn sa§layaca§ beklenmektedir. Bu nal‡mann devam olarak leklenebilirli§i grmek asndan daha byk kodlar zerinde test etmeyi planlamaktayz. 7

Gelecek ˙al‡malar

Ksmi yol kstlar yakla‡m birka ‡ekilde geli‡tirilebilir. rne§in, kadar kk bir yukar yakla‡mla ba‡lamak ok iyi bir kir de§ildir. Onun yerine yol zerinde birbiriyle ba§msz bir dallanma ko‡ullar kmesiyle ba‡lanabilir. Sonra kst zc bu daha gl ksmi kstn ko‡ullarn birer birer zebilir. Bu yntem kst zcye yklenmeden sorgu ba‡na do§ru girdileri bulma ‡ansn artrr.

Ksmi yol kstlar grep ve vim gibi daha byk kodlar zerinde test edilmelidir. Zaman kstlarna uyulabilmesi iin bu testler henz gerekle‡tirilememi‡tir. iin bu

Kaynaklar

References

1. P. Godefroid , N. Klarlund , and K. Sen , Dart: Directed automated random testing, SIGPLAN Not. , vol. 40 , no. 6 , pp. 213223 , 2005 .

2. A. R. Bradley , Sat-based model checking without unrolling , in Verication, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011 , pp. 7087 , 2011 .

3. C. Cadar , D. Dunbar , and D. Engler , Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs , in Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation , OSDI' 08 , 2008 .

4. K. Sen , D. Marinov , and G. Agha, Cute: A concolic unit testing engine for c , SIGSOFT Softw. Eng. Notes , vol. 30 , no. 5 , pp. 263272 , 2005 .

5. J. Burnim and K. Sen , Heuristics for scalable dynamic test generation , in Proceedings of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, ASE '08 , 2008 .

6. N. Tillmann and J. De Halleux , Pex: White box test generation for .net , in Proceedings of the 2Nd International Conference on Tests and Proofs , TAP'08 , 2008 .

7. K. Sen and G. Agha, Cute and jcute: Concolic unit testing and explicit path modelchecking tools , in Proceedings of the 18th International Conference on Computer Aided Verication , CAV'06 , 2006 .

8. K. Khknen , R. Kindermann , K. Heljanko , and I. Niemel , Experimental comparison of concolic and random testing for java card applets , in Model Checking Software (J. van de Pol and M. Weber, eds.), vol. 6349 of Lecture Notes in Computer Science, pp. 2239 , Springer Berlin Heidelberg, 2010 .

9. X. Qu and B. Robinson , A case study of concolic testing tools and their limitations , in Proceedings of the 2011 International Symposium on Empirical Software Engineering and Measurement , ESEM '11 , 2011 .

10. H. Seo and S. Kim , How we get there: A context-guided search strategy in concolic testing , in Proceedings of the 22Nd ACM SIGSOFT International Symposium on Foundations of Software Engineering , FSE 2014 , 2014 .

11. S. Sidiroglou-Douskos , E. Lahtinen , N. Rittenhouse , P. Piselli , F. Long , D. Kim , and M. C. Rinard , Targeted automatic integer overow discovery using goaldirected conditional branch enforcement , in Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '15 , pp. 473486 , 2015 .

12. E. Tsang, Foundations of constraint satisfaction, 1993 .

13. P. Nuzzo , A. Puggelli , S. A. Seshia , and A. Sangiovanni-Vincentelli , Calcs: Smt solving for non-linear convex constraints , in Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design , FMCAD '10 , 2010 .

14. M. Souza , M. Borges , M. d'Amorim, and C. S. Pasareanu , Coral: Solving complex constraints for symbolic pathnder , in Proceedings of the Third International Conference on NASA Formal Methods , NFM'11 , 2011 .

15. J. Zhou , M. Yin , and C. Zhou , New worst-case upper bound for 2-sat and 3-sat with the number of clauses as the parameter , in Proceedings of the Twenty-Fourth AAAI Conference on Articial Intelligence , 2010 .

16. S. Anand , E. K. Burke , T. Y. Chen , J. Clark , M. B. Cohen , W. Grieskamp , M. Harman , M. J. Harrold , and P. Mcminn , An orchestrated survey of methodologies for automated software test case generation , J. Syst. Softw. , vol. 86 , pp. 19782001 , Aug . 2013 .

17. B. Dutertre , Yices 2 .2, in Computer Aided Verication ( A. Biere and R. Bloem, eds.), vol. 8559 of Lecture Notes in Computer Science , pp. 737744 , Springer International Publishing, 2014 .