Memanfaatkan Observasi Tingkat Sistem untuk Menginformasikan Pembelajaran Bayesian Parameter Model bagi Verifikasi Kuantitatif

Verifikasi kuantitatif adalah teknik yang ampuh untuk menganalisis properti kuantitatif kunci dari sistem perangkat lunak, seperti keandalan dan waktu respons. Ketika dikombinasikan dengan pembelajaran Bayesian, teknik ini memungkinkan inferensi probabilistik atas parameter model. Namun, akurasi dan ketahanan hasil verifikasi sangat bergantung pada pengetahuan prior (PK) yang mendasari inferensi Bayesian. Pengetahuan ini mencerminkan keyakinan awal tentang probabilitas peristiwa dan biasanya bergantung pada keahlian domain. Penggunaan PK yang tidak akurat atau tidak informatif dapat berdampak negatif pada analisis kuantitatif, menghasilkan hasil verifikasi yang salah.

Pendekatan EPIK mengatasi tantangan penting ini dengan menggali dan menyematkan PK dalam verifikasi kuantitatif yang dilengkapi estimator Bayesian. Berbeda dari pendekatan yang ada yang memerlukan PK pada parameter transisi model formal, EPIK memanfaatkan properti tingkat sistem yang dapat diobservasi secara langsung dan terkait dengan semantik dunia nyata. EPIK merumuskan masalah optimisasi dua arah untuk menurunkan distribusi parameter transisi yang tidak diketahui, lalu menyematkan distribusi tersebut untuk memver

Efektivitas, fleksibilitas, dan keumuman EPIK dievaluasi melalui eksperimen terperinci menggunakan berbagai varian studi kasus dunia nyata dan beragam instansiasi EPIK. Studi kasus tersebut kemungkinan mencakup sistem perangkat lunak dari domain seperti komputasi awan, sistem otonom, atau jaringan komunikasi, tempat verifikasi kuantitatif sangat penting.

Temuan kunci dari evaluasi eksperimental meliputi:

- **Akurasi yang meningkat**: prior yang diturunkan EPIK menghasilkan hasil verifikasi yang lebih akurat dibandingkan penggunaan prior yang tidak informatif atau tidak akurat. Penurunan galat untuk properti yang sulit terukur cukup signifikan, menunjukkan nilai observasi tingkat sistem.
- **Ketahanan**: pendekatan ini menunjukkan ketahanan terhadap variasi kualitas dan kuantitas observasi tingkat sistem, mempertahankan hasil verifikasi yang andal bahkan dengan data yang terbatas.
- **Fleksibilitas**: EPIK diinstansiasi dengan berbagai teknik optimisasi dan estimator Bayesian, menunjukkan bahwa kerangka kerja ini dapat diadaptasi ke berbagai pengaturan tanpa kehilangan performa.
- **Keumuman**: metode ini diterapkan pada berbagai studi kasus dunia nyata, masing-masing dengan karak