Synthesis of past time signal temporal logic formulas using monotonicity properties

Sinyal Zamansal Mantık(Signal Temporal Logic - STL) verilmli algoritmaları ve anlatım gücü sayesinde çalışma zamanında doğrulama, formel kontrol ve zaman serisi verilerinin analizinde yaygın olarak kullanılmaktadır. Bir STL formülü tanımlayıp, sistemi simüle edip, test süreçlerindeki gibi beklenmeyen davranışları bu formüle göre işaretlemek görece kolayken, hataların altında yatan sebebi bulacak bir STL formülü bulmak karmaşık bir süreçtir. Bu tezin ana motivasyonu, bir sistemde meydana gelen hatalı davranışa sebep olan olayları otomatikleştirilmiş, verimli ve insan tarafından okunabilir şekilde açıklayacak bir yöntem bulmaktır. Bu çalışmada amaç sistemde hatalara yol açan durumları bulmak olduğundan, geçmiş olayları tanımlamakta kullanılan geçmiş zamanlı sinyal sayısal mantık (past time Signal Temporal Logic - ptSTL) kullanılmıştır. Bu tez bir veri kümesinden, beklenmeyen davranışlara sebep olan zamansal özellikleri bulacak yeni bir yöntem sunmaktadır. Belirtilen veri kümesi her zamanda etiketlenmiş sistem izlerinden oluşmaktadır. İlk olarak, ptSTL formüllerinin bu veri kümesi üzerindeki monotonluk özellikleri tanımlanmıştır. Ardından monotonluk özellikleri kullanılarak, ptSTL için verimli bir parametre sentezi yöntemi önerilmiştir. Son olarak, parametre sentezi yöntemi ile bulunan optimize formülleri birleştiren yinelemeli ve rehbersiz bir formül sentezleme yapısı geliştirilmiştir. Ek olarak, önerilen yaklaşımın her iz için tekil etiketi olan veri kümeleri için genişletilmesi sağlanmıştır. Bu kısımda, önceden tanımlanan monotonluk özelliklerinin korunduğu gösterilip, yapı uyarlanmıştır.